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.
-
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.
-
Rewriting, Inference, and Proof
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?
-
Bayesian Minimax Estimation of the Normal Model with Incomplete Prior Covariance Matrix Specification
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…
-
Middleware for Managing Provenance Metadata
We describe middleware for managing distributed provenance metadata, where each host maintains an authoritative local repository of the provenance metadata gathered on it.
-
Discovery of Numerous Specific Topics Via Term Co-Occurrence Analysis
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.
-
Theory of Reals for Verification and Synthesis of Hybrid Dynamical Systems
Formal verification and synthesis are both indispensable components of any methodology for designing and efficiently developing safe cyber-physical systems.
-
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.