Cyber & formal methods publications

We pursue a declarative approach to provide an abstraction from the high complexity of NCPS and avoid error-prone and time-consuming low-level programming.

In this paper, we present the formal verification of the compression function which is a core element of the clock synchronization service of TTEthernet.

In this paper we introduce a method to compute all pathways in a signalling network that satisfy a simple property constraining initial, final and intermediate states.

We are developing a completely decentralized system with each computer maintaining the authoritative repository of the provenance gathered on it.

The principle underlying the card trick can be proved in a number of ways. We present the argument as a series of transformations that demystify the trick and describe its…

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 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…

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 propose an ambitious and long-term research program toward the construction of error-free software systems.

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.