17 citations · 28 across the 18 of their papers we have counts for
3 papers · 1 filter
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…