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…
-
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.
-
Logic and Epistemology in Safety Cases
-
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…
-
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…
-
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.
-
Wernicke-Korsakoff Syndrome: A Nutritional Alcohol-Related Brain Disorder