Cyber & formal methods publications

This volume contains the proceedings of the second working conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2008, held in Toronto, Canada, in October 2008.

We argue that trust need not be achieved at the expense of automation, and outline a lightweight approach where the results of untrusted verifiers are checked by a trusted offline…

We show that there is no black-box construction of IBE from Trapdoor Permutations (TDP) or even from Chosen Ciphertext Secure Public Key Encryption (CCA-PKE).

To detect exposures to the various pathogens more rapidly, especially during these early stages, we evaluated a suite of host responses to biological threat agents using global gene expression profiling…

We present the basis of the modeling method and discuss two related verification approaches for analyzing complex, real-time distributed systems.

This paper proposes a formal framework and architecture for specification and analysis of interactive agents. The framework can be used to explore the design space, study features of different points…

We construct such a scheme for predicates corresponding to the evaluation of inner products over (for some large integer N).

Three models of coordination—Reo, Actors-Roles-Coordinators (ARC), and Reflective Russian Dolls (RRD)—are compared and contrasted according to a set of coordination features.

We present a novel approach to developing cross-layer optimization for resource limited real-time distributed systems, based on a constraint refinement technique combined with formal specification and feedback from system implementation.

This report describes the monitoring, intrusion detection, and reporting infrastructure of the resulting system highlighting the design principles and lessons learned that are generally applicable to survivable information systems.