38 citations · 63 across the 23 of their papers we have counts for
29 papers
Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Eden Frenkel, Tej Chajed, Oded Padon +1
This paper lays a practical foundation for using abstract interpretation with an abstract domain that consists of sets of quantified first-order logic formulas. This abstract domai…
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Neta Elad, Oded Padon, Sharon Shoham
First-order logic, and quantifiers in particular, are widely used in deductive verification. Quantifiers are essential for describing systems with unbounded domains, but prove diff…
State Merging with Quantifiers in Symbolic Execution
David Trabish, Noam Rinetzky, Sharon Shoham +1
We address the problem of constraint encoding explosion which hinders the applicability of state merging in symbolic execution. Specifically, our goal is to reduce the number of di…
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…
Hyperproperty Verification as CHC Satisfiability
Shachar Itzhaky, Sharon Shoham, Yakir Vizel
Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, su…
Invariant Inference With Provable Complexity From the Monotone Theory
Yotam M. Y. Feldman, Sharon Shoham
Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, b…
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
Jason R. Koenig, Oded Padon, Sharon Shoham +1
We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified in…
Property-Directed Reachability as Abstract Interpretation in the Monotone Theory
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham +1
Inferring inductive invariants is one of the main challenges of formal verification. The theory of abstract interpretation provides a rich framework to devise invariant inference a…
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…
Some Complexity Results for Stateful Network Verification
Kalev Alpernas, Aurojit Panda, Alexander Rabinovich +4
In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour dep…
Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan +3
Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imp…
Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction
Oren Ish Shalom, Shachar Itzhaky, Noam Rinetzky +1
Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of in ductive quantified loop invariants which, in some cas…
Modular Verification of Concurrent Programs via Sequential Model Checking
Dan Rasin, Orna Grumberg, Sharon Shoham
This work utilizes the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We reduce the verification of a concurrent program…
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…
Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea +4
Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any sy…
A Thread-Local Semantics and Efficient Static Analyses for Race Free Programs
Suvam Mukherjee, Oded Padon, Sharon Shoham +2
Data race free (DRF) programs constitute an important class of concurrent programs. In this paper we provide a framework for designing and proving the correctness of data flow anal…
Learning the Boundary of Inductive Invariants
Yotam M. Y. Feldman, Mooly Sagiv, Sharon Shoham +1
We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, wh…
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…
Complexity and Information in Invariant Inference
Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv +1
This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of po…
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…
Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics
Idan Berkovits, Marijana Lazic, Giuliano Losa +2
Verification of fault-tolerant distributed protocols is an immensely difficult task. Often, in these protocols, thresholds on set cardinalities are used both in the process code an…
Inferring Inductive Invariants from Phase Structures
Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham +1
Infinite-state systems such as distributed protocols are challenging to verify using interactive theorem provers or automatic verification tools. Of these techniques, deductive ver…
Undecidability of Inferring Linear Integer Invariants
Sharon Shoham
We show that the problem of determining the existence of an inductive invariant in the language of quantifier free linear integer arithmetic (QFLIA) is undecidable, even for transi…