1 citations · 1 across the 4 of their papers we have counts for
4 papers
Proving Cutoff Bounds for Safety Properties in First-Order Logic
Raz Lotan, Eden Frenkel, Sharon Shoham
First-order logic has been established as an important tool for modeling and verifying intricate systems such as distributed protocols and concurrent systems. These systems are par…
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…
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…