Cyber & formal methods publications

We discuss a range of issues at the intersection of rewriting and inference. How can other inference procedures be combined with rewriting? Can rewriting be used to describe inference procedures?

This work addresses the issue of Bayesian robustness in the multivariate normal model when the prior covariance matrix is not completely specified, but rather is described in terms of positive…

We describe middleware for managing distributed provenance metadata, where each host maintains an authoritative local repository of the provenance metadata gathered on it.

We describe efficient techniques for construction of large term co-occurrence graphs, and investigate an application to the discovery of numerous fine-grained (specific) topics.

Formal verification and synthesis are both indispensable components of any methodology for designing and efficiently developing safe cyber-physical systems.

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

This paper presents a graphical user interface (GUI) for the Maude-NPA, a crypto protocol analysis tool that takes into account algebraic properties of cryptosystems not supported by other tools, such…

In this paper, we examine what real vendors do to ensure that their products are reasonably secure. Our conclusion is that software vendors put significant energy into software security, but…

This paper reflects on many risks in the development and use of computer-related systems. It considers past and future alternatives, suggests some remedial approaches, and offers a few broad conclusions.

We review this idea and show how it provides a bridge between correctness, which is the goal of software verification (and especially formal verification), and the probabilistic properties such as…

We introduce some of the basic deduction techniques used in software and hardware verification and outline the theoretical and engineering issues in building deductive verification tools.

We propose an ambitious and long-term research program toward the construction of error-free software systems.