Cyber & formal methods publications
-
Non-Linear Rewrite Closure and Weak Normalization
In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and…
-
Logic and Epistemology in Safety Cases
-
Safety Verification for Linear Systems
-
A Vocabulary of Topological and Containment Relations for a Practical Biological Ontology
-
Network Coding for Content-Based Intermittently Connected Emergency Networks
n this demo, we present a network architecture that exploits partial caches by utilizing network coding to deliver large files (e.g. images) to first responders. The architecture is based on…
-
Time-Aware Relational Abstractions for Hybrid Systems
We present a technique to compute a time-aware relational abstraction for verifying (timing-related) safety properties of cyber-physical systems.
-
Large-Scale Access Scheduling in Wireless Mesh Networks Using Social Centrality
We propose a set of efficient resource allocation algorithms and channel access scheduling protocols based on Latin squares and social centrality metrics for wireless mesh networks (WMNs) with multi-radio multi-channel…
-
On the Potential to Enhance the Spatial Resolution of the Day/Night Band (DNB) Channel of the Visible and Infrared Imaging Radiometer Suite (VIRRS) for the Second Joint Polar Satellite System (JPSS-2) and Beyond
This paper examines the feasibility and potential benefits of enhancing the spatial resolution of the VIIRS DNB channel for the JPSS-2 mission and beyond.
-
Application Patterns for Cyber-Physical Systems
Inspired by a new programming paradigm based on partially ordered knowledge sharing model for loosely coupled distributed computing and its implementation in our cyber-application framework, this paper studies how to…
-
Drill Evaluation for Training Procedural Skills
This paper describes an automated assessment and feedback capability that has been applied to training for a complex software system in widespread use throughout the U.S. Army.
-
JBernstein: A Validity Checker for Generalized Polynomial Constraints
Despite substantial advances in verification technology, complexity issues with classical decision procedures for nonlinear real arithmetic are still a major obstacle for formal verification of real-world applications.
-
Automated Reasoning, Fast and Slow
We present some tentative and preliminary speculation on the prospects for automated reasoning in the style of System 1, and the synergy with the more traditional System 2 strand of…