38 citations · 63 across the 23 of their papers we have counts for
8 papers · 1 filter
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…