research
∙
08/23/2023
State Merging with Quantifiers in Symbolic Execution
We address the problem of constraint encoding explosion which hinders th...
share
research
∙
06/30/2023
Speculative SAT Modulo SAT
State-of-the-art model-checking algorithms like IC3/PDR are based on uni...
research
∙
06/16/2023
Fast Approximations of Quantifier Elimination
Quantifier elimination (qelim) is used in many automated reasoning tasks...
research
∙
04/25/2023
Hyperproperty Verification as CHC Satisfiability
Hyperproperties govern the behavior of a system or systems across multip...
research
∙
08/15/2022
Invariant Inference With Provable Complexity From the Monotone Theory
Invariant inference algorithms such as interpolation-based inference and...
research
∙
12/10/2021
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
We present a PDR/IC3 algorithm for finding inductive invariants with qua...
research
∙
10/30/2021
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Inferring inductive invariants is one of the main challenges of formal v...
research
∙
07/26/2021
Logical Characterization of Coherent Uninterpreted Programs
An uninterpreted program (UP) is a program whose semantics is defined ov...
research
∙
06/02/2021
Some Complexity Results for Stateful Network Verification
In modern networks, forwarding of packets often depends on the history o...
research
∙
06/02/2021
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Various verification techniques for temporal properties transform tempor...
research
∙
06/02/2021
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
Automatic verification of array manipulating programs is a challenging p...
research
∙
06/01/2021
Modular Verification of Concurrent Programs via Sequential Model Checking
This work utilizes the plethora of work on verification of sequential pr...
research
∙
06/01/2021
Quantifiers on Demand
Automated program verification is a difficult problem. It is undecidable...
research
∙
10/02/2020
Proving Highly-Concurrent Traversals Correct
Modern highly-concurrent search data structures, such as search trees, o...
research
∙
09/06/2020
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs
Data race free (DRF) programs constitute an important class of concurren...
research
∙
08/22/2020
Learning the Boundary of Inductive Invariants
We study the complexity of invariant inference and its connections to ex...
research
∙
05/27/2020
Global Guidance for Local Generalization in Model Checking
SMT-based model checkers, especially IC3-style ones, are currently the m...
research
∙
10/27/2019
Complexity and Information in Invariant Inference
This paper addresses the complexity of SAT-based invariant inference, a ...
research
∙
05/19/2019
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
Verification of fault-tolerant distributed protocols is an immensely dif...
research
∙
05/19/2019
Inferring Inductive Invariants from Phase Structures
Infinite-state systems such as distributed protocols are challenging to ...
research
∙
05/19/2019
Property Directed Self Composition
We address the problem of verifying k-safety properties: properties that...
research
∙
12/03/2018
Undecidability of Inferring Linear Integer Invariants
We show that the problem of determining the existence of an inductive in...
research
∙
05/10/2018
Order out of Chaos: Proving Linearizability Using Local Views
Proving the linearizability of highly concurrent data structures, such a...
research
∙
10/24/2017
Bounded Quantifier Instantiation for Checking Inductive Invariants
We consider the problem of checking whether a proposed invariant ϕ expre...
research
∙
10/19/2017
Paxos Made EPR: Decidable Reasoning about Distributed Protocols
Distributed protocols such as Paxos play an important role in many compu...
research
∙
10/03/2017
Programming Not Only by Example
In recent years, there has been tremendous progress in automated synthes...
research
∙
08/19/2017
Abstractions for Verifying Isolation Properties in Stateful Networks
Modern networks achieve robustness and scalability by maintaining states...
research
∙
08/19/2017