Cyber & formal methods publications

In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and…

Efficient and effective means are needed that exploit structure inherent in one layer of architecture to provide key properties to enable reliable execution at other levels.

We focus on coordinating actors and roles through message manipulations based on event-based timing constraints. In addition, different types of timing constraints are generalized into a semiring-based constraint structure; and…

Higher-Order and Symbolic Computation is an international journal that presents a broad-spectrum forum for discussion of results and ideas on programming with higher-order and symbolic facilities: first-class functions and continuations,…

A systematic approach to digital forensic engineering acknowledges the close, intertwine relationship between digital forensics and information security.

In this paper, we argue that analysis tools based on recent advances in formal methods (SMT solvers, infinite bounded model checkers, and k-induction) can provide suitable modeling notations, effective analysis,…

We formalize the problem of defending honeynets from systematic mapping (a serious threat to their viability) as a simple two-person game.

Abstract This talk discusses some of the challenges of building a usable theorem prover. These include the chasm between theory and code, conflicting requirements, feature interaction, and competitive performance. The…

Here we demonstrate additional applications that enjoy strong security properties and a high level of efficiency.

Our approach involves a multilayer security architecture for monitoring process control systems to achieve accurate and effective situational awareness.

We present a unifying framework that extends the CP formalism in both model and solutions, to tackle ill-defined combinatorial problems with incomplete or erroneous data.