Cyber & formal methods publications

Details of the Advanced Riometer Components (ARCOM) component-based software architecture are presented.

This article is a retrospective of concepts and people who have contributed significantly to the IEEE Symposium on Security and Privacy over the past 30 years.

A formalism for expressing the operational semantics of proof languages used in procedural theorem provers is proposed.

In this paper we analyze the special case of context unification where the use of at most one context variable is allowed and show that it is in NP.

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 use a mechanically checked proof of the Knaster–Tarski theorem to illustrate several features of the Prototype Verification System (PVS).

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.