-
Chapter and Conference Paper
An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning
We contribute a new dataset composed of more than 41K MetiTarski challenges that can be used to investigate applications of machine learning (ML) in determining efficient variable orderings in Cylindrical Alge...
-
Chapter and Conference Paper
CoProver: A Recommender System for Proof Construction
Interactive Theorem Provers (ITPs) are an indispensable tool in the arsenal of formal method experts as a platform for construction and (formal) verification of proofs. The complexity of the proofs in conjunct...
-
Article
Open AccessConflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs
Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. Conflict-driven procedures perform non...
-
Chapter and Conference Paper
Requirements-Driven Model Checking and Test Generation for Comprehensive Verification
In this paper, we present a novel approach that seamlessly integrates requirements-based testing and model checking. Given a set of functional requirements and properties, both generic attributes and application ...
-
Article
Opposition-based equilibrium optimizer algorithm for identification of equivalent circuit parameters of various photovoltaic models
The simulation, assessment, and harvesting of maximum energy of the solar photovoltaic (PV) system require accurate and fast parameter estimation for solar cell/module models. No complete information on the PV...
-
Article
2018 CAV award
-
Article
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness
Many applications depend on solving the satisfiability of formulæ involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory. This article presents a new method for...
-
Chapter and Conference Paper
The Correctness of a Code Generator for a Functional Language
Code generation is gaining popularity as a technique to bridge the gap between high-level models and executable code. We describe the theory underlying the PVS2C code generator that translates functional progr...
-
Chapter and Conference Paper
Model-Centered Assurance for Autonomous Systems
The functions of an autonomous system can generally be partitioned into those concerned with perception and those concerned with action. Perception builds and maintains an internal model of the world (i.e., th...
-
Article
TeLEx: learning signal temporal logic from positive examples using tightness metric
We propose a novel passive learning approach, TeLex, to infer signal temporal logic (STL) formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. First, we p...
-
Chapter
A Refinement Proof for a Garbage Collector
We describe how the PVS theorem prover has been used to verify a safety property of a widely studied garbage collection algorithm. The safety property asserts that “nothing but garbage is ever collected”. The gar...
-
Chapter and Conference Paper
Formalizing Hoare Logic in PVS
We formalize a Hoare logic for the partial correctness of while programs in PVS and prove its soundness and relative completeness. We use the PVS higher-order logic to define the syntax and semantics of a small i...
-
Chapter
Combining Model Checking and Deduction
There are two basic approaches to automated verification. In model checking, the system is viewed as a graph representing possible execution steps. Properties are established by exploring or traversing the gra...
-
Chapter and Conference Paper
Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems
We propose an automatic synthesis technique to generate provably correct controllers of stochastic linear dynamical systems for Signal Temporal Logic (STL) specifications. While formal synthesis problems can b...
-
Chapter and Conference Paper
TeLEx: Passive STL Learning Using Only Positive Examples
We propose a novel passive learning approach, TeLEx, to infer signal temporal logic formulas that characterize the behavior of a dynamical system using only observed signal traces of the system. The approach requ...
-
Chapter and Conference Paper
Satisfiability Modulo Theories and Assignments
The CDCL procedure for SAT is the archetype of conflict-driven procedures for satisfiability of quantifier-free problems in a single theory. In this paper we lift CDCL to CDSAT (Conflict-Driven Satisfiability), a...
-
Chapter and Conference Paper
Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems
Avionic systems involve complex time-dependent behaviors across interacting components. This paper presents a contract-based approach for formally verifying these behaviors in a compositional manner. A unique ...
-
Chapter and Conference Paper
ARSENAL: Automatic Requirements Specification Extraction from Natural Language
Requirements are informal and semi-formal descriptions of the expected behavior of a complex system from the viewpoints of its stakeholders (customers, users, operators, designers, and engineers). However, for...
-
Chapter and Conference Paper
Code Generation Using a Formal Model of Reference Counting
Reference counting is a popular technique for memory management. It tracks the number of active references to a data object during the execution of a program. Reference counting allows the memory used by a dat...
-
Chapter and Conference Paper
The Gradual Verifier
Static verification traditionally produces yes/no answers. It either provides a proof that a piece of code meets a property, or a counterexample showing that the property can be violated. Hence, the progress o...
