1 citations · 2 across the 5 of their papers we have counts for
7 papers
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…
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…
VeriFly: On-the-fly Assertion Checking via Incrementality
Miguel A. Sanchez-Ordaz, Isabel Garcia-Contreras, Victor Perez-Carrasco +3
Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers this…
Multivariant Assertion-based Guidance in Abstract Interpretation
Isabel Garcia-Contreras, Jose F. Morales, Manuel V. Hermenegildo
Approximations during program analysis are a necessary evil, as they ensure essential properties, such as soundness and termination of the analysis, but they also imply not always…