Cyber & formal methods publications

We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract…

A new US law allows warrantless wiretapping whenever one end of the communication is believed to be outside national borders. This creates serious security risks: danger of exploitation of the…

Tracing the history of exposing and elucidating the wide variety of system problems and associated social implications of uses and misuses of computing technology.

This paper presents a constraint-based technique for discovering a rich class of inductive invariants (boolean combinations of polynomial inequalities of bounded degree) for verification of hybrid systems.

To reduce the risk of successful cryptanalysis, new keys must be established (rekeying). We have designed a rekeying scheme that provides both backward and forward secrecy.

In this paper we investigate how to use the alerts from several audit sources to improve the accuracy of the intrusion detection system (IDS). Concentrating on web server attacks, we…

We present novel online index learning algorithms. When compared to other approaches, including one-versus-rest and top-down learning and classification using support vector machines, we find that indexing is highly advantageous…

This tutorial describes the use of PL to model signal transduction processes. It begins with a general discussion of Symbolic Systems Biology, followed by some background on rewriting logic and…

This paper discusses event-based semantics in the context of the emerging concept of Cyber Physical Systems and describes two related formal models concerning policy-based coordination and Interactive Agents.

We describe a general technique for building abstract interpreters over powerful universally quantified abstract domains that leverage existing quantifier-free domains.

Abstract PVS is now 15 years old, and has been extensively used in research, industry, and teaching. The system is very expressive, with unique features such as predicate subtypes, recursive…