Cyber & formal methods publications
-
A Flexible Streaming Software Architecture for Scientific Instruments
Details of the Advanced Riometer Components (ARCOM) component-based software architecture are presented.
-
Reflections on the 30th Anniversary of the IEEE Symposium on Security and Privacy
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.
-
The Proof Monad
A formalism for expressing the operational semantics of proof languages used in procedural theorem provers is proposed.
-
Context Unification with One Context Variable
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.
-
Fixpoints and Search in PVS
We use a mechanically checked proof of the Knaster–Tarski theorem to illustrate several features of the Prototype Verification System (PVS).
-
Toward Distributed Declarative Control of Networked Cyber-Physical Systems
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.
-
SMT-Based Formal Verification of a TTEthernet Synchronization Function
In this paper, we present the formal verification of the compression function which is a core element of the clock synchronization service of TTEthernet.
-
Understanding Signalling Networks as Collections of Signal Transduction Pathways
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.
-
Efficient Querying of Distributed Provenance Stores
We are developing a completely decentralized system with each computer maintaining the authoritative repository of the provenance gathered on it.
-
Unraveling a Card Trick
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…
-
Performance and Extension of User Space File Systems
In this paper, we discuss the evolution of user space file systems with an emphasis on FUSE, and measure its performance using a variety of test cases.
-
Mendel: Efficiently Verifying the Lineage of Data Modified in Multiple Trust Domains
We describe Mendel, a protocol with a three-pronged strategy that combines eager signature verification, lazy trust establishment, and cryptographic ordering witnesses to yield fast lineage verification in distributed multi-domain environments.