17 citations · 28 across the 18 of their papers we have counts for
24 papers
Verifiable Checks for Business Rule Consistency
Joseph Tafese, Milad Hooshyar, Sam Bayless +2
Maintaining consistency between natural language documentation of business rules and their evolving internal implementations is a significant challenge in large-scale systems. We p…
Automatic Inference of Relational Object Invariants
Yusen Su, Jorge A. Navas, Arie Gurfinkel +1
Relational object invariants (or representation invariants) are relational properties held by the fields of a (memory) object throughout its lifetime. For example, the length of a…
Inductive Predicate Synthesis Modulo Programs (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the…
Btor2MLIR: A Format and Toolchain for Hardware Verification
Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel
Formats for representing and manipulating verification problems are extremely important for supporting the ecosystem of tools, developers, and practitioners. A good format allows r…
Speculative SAT Modulo SAT
Hari Govind V K, Isabel Garcia-Contreras, Sharon Shoham +1
State-of-the-art model-checking algorithms like IC3/PDR are based on uni-directional modular SAT solving for finding and/or blocking counterexamples. Modular SAT solvers divide a S…
Fast Approximations of Quantifier Elimination
Isabel Garcia-Contreras, Hari Govind V K, Sharon Shoham +1
Quantifier elimination (qelim) is used in many automated reasoning tasks including program synthesis, exist-forall solving, quantified SMT, Model Checking, and solving Constrained…
Towards Reliable Neural Specifications
Chuqin Geng, Nham Le, Xiaojie Xu +3
Having reliable specifications is an unavoidable challenge in achieving verifiable correctness, robustness, and interpretability of AI systems. Existing specifications for neural n…
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existin…
Logical Characterization of Coherent Uninterpreted Programs
Hari Govind V K, Sharon Shoham, Arie Gurfinkel
An uninterpreted program (UP) is a program whose semantics is defined over the theory of uninterpreted functions. This is a common abstraction used in equivalence checking, compile…
Verifying Verified Code
Siddharth Priya, Xiang Zhou, Yusen Su +3
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a follow up case study that explo…
Quantifiers on Demand
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Automated program verification is a difficult problem. It is undecidable even for transition systems over Linear Integer Arithmetic (LIA). Extending the transition system with theo…
Global Guidance for Local Generalization in Model Checking
Hari Govind V K, YuTing Chen, Sharon Shoham +1
SMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants…
Interpolating Strong Induction
Hari Govind V K, Yakir Vizel, Vijay Ganesh +1
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, propert…
Unification-based Pointer Analysis without Oversharing
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyse…
Property Directed Self Composition
Ron Shemer, Arie Gurfinkel, Sharon Shoham +1
We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self co…
Local Reasoning for Parameterized First Order Protocols
Rylo Ashmore, Arie Gurfinkel, Richard Trefler
First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed system…
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts
Andreas Katis, Grigory Fedyukovich, Huajun Guo +4
Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of re…
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability
Andreas Katis, Grigory Fedyukovich, Andrew Gacek +3
The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizabilit…
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel +1
We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely…
Synthesizing Modular Invariants for Synchronous Code
Pierre-Loic Garoche, Arie Gurfinkel, Temesghen Kahsai
In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characte…
SMT-based Model Checking for Recursive Programs
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other…
Automatic Abstraction in SMT-Based Unbounded Software Model Checking
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki +1
Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e. reachability) properties. They combine two key ideas -- (a) "con…
Interpolation Properties and SAT-based Model Checking
Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
Craig interpolation is a widespread method in verification, with important applications such as Predicate Abstraction, CounterExample Guided Abstraction Refinement and Lazy Abstrac…
Robust Vacuity for Branching Temporal Logic
Arie Gurfinkel, Marsha Chechik
There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventu…