Cyber & formal methods publications

We design and implement a "what-if" analysis methodology using formal methods. Our methodology analyzes the impact of failures and changes in heterogeneous networks on QoS of flows.

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

We describe a complementary approach that uses Web Ontology Language and Semantic Web Rule Language to capture information about the roles and capabilities required to complete a task, and the…

(video)

We present a novel proof of the Stressing algorithm and its verification using the Prototype Verification System (PVS) theorem prover.

We use an architecture where aggregation, fusion, and composition policies define how provenance records can be automatically merged to facilitate the analysis and reproducibility of experiments.

We provide a contract-based type system of Simulink with annotations and dimensions/units associated with ports and links.

We describe in this paper a simple alternative, the least-squares (LS) configuration, which employs an intuitive post-compensator, and retains the easy-to-tune decoupling control feature.

We present experimental results that show that our tool Brahma can efficiently synthesize highly nontrivial 10-20 line loop-free bit vector programs.

In this paper, we propose using a special variant of low-density parity codes (LDPCs) - Euclidean Geometry LDPC (EG-LDPC) codes - to enable dynamic changes in the level of fault…

We use the Prototype Verification System (PVS) to verify a satisfiability procedure based on the Davis–Putnam–Logemann–Loveland (DPLL) scheme.