Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN. - Marsha Chechik; Benet Devereux; Arie Gurfinkel (SPIN, 2001)

chi-Chek: A Multi-valued Model-Checker. - Marsha Chechik; Arie Gurfinkel; Benet Devereux (CAV, 2002)

Model exploration with temporal logic query checking. - Arie Gurfinkel; Benet Devereux; Marsha Chechik (SIGSOFT FSE, 2002)

TLQSolver: A Temporal Logic Query Checker. - Marsha Chechik; Arie Gurfinkel (CAV, 2003)

Multi-Valued Model Checking via Classical Model Checking. - Arie Gurfinkel; Marsha Chechik (CONCUR, 2003)

Generating Counterexamples for Multi-valued Model-Checking. - Arie Gurfinkel; Marsha Chechik (FME, 2003)

chiChek: A Model Checker for Multi-Valued Reasoning. - Steve M. Easterbrook; Marsha Chechik; Benet Devereux; Arie Gurfinkel; Albert Y. C. Lai; Victor Petrovykh; Anya Tafliovich; Christopher D. Thompson-Walsh (ICSE, 2003)

Proof-Like Counter-Examples. - Arie Gurfinkel; Marsha Chechik (TACAS, 2003)

Multi-valued symbolic model-checking. - Marsha Chechik; Benet Devereux; Steve M. Easterbrook; Arie Gurfinkel (ACM Trans. Softw. Eng. Methodol., 2003)

Temporal Logic Query Checking: A Tool for Model Exploration. - Arie Gurfinkel; Marsha Chechik; Benet Devereux (IEEE Trans. Software Eng., 2003)

Extending Extended Vacuity. - Arie Gurfinkel; Marsha Chechik (FMCAD, 2004)

How Vacuous Is Vacuous? - Arie Gurfinkel; Marsha Chechik (TACAS, 2004)

A Practical Approach to Partial Functions in CVC Lite. - Sergey Berezin; Clark W. Barrett; Igor Shikanian; Marsha Chechik; Arie Gurfinkel; David L. Dill (D/PDPAR@IJCAR, 2004)

How Thorough Is Thorough Enough? - Arie Gurfinkel; Marsha Chechik (CHARME, 2005)

Identification and Counter Abstraction for Full Virtual Symmetry. - Ou Wei; Arie Gurfinkel; Marsha Chechik (CHARME, 2005)

Stuttering Abstraction for Model Checkin. - Shiva Nejati 001; Arie Gurfinkel; Marsha Chechik (SEFM, 2005)

Model-Checking Software Using Precise Abstractions. - Marsha Chechik; Arie Gurfinkel (VSTTE, 2005)

Yasm: A Software Model-Checker for Verification and Refutation. - Arie Gurfinkel; Ou Wei; Marsha Chechik (CAV, 2006)

Why Waste a Perfectly Good Abstraction?. - Arie Gurfinkel; Marsha Chechik (TACAS, 2006)

Systematic Construction of Abstractions for Model-Checking. - Arie Gurfinkel; Ou Wei; Marsha Chechik (VMCAI, 2006)

Data structures for symbolic multi-valued model-checking. - Marsha Chechik; Arie Gurfinkel; Benet Devereux; Albert Y. C. Lai; Steve M. Easterbrook (Formal Methods Syst. Des., 2006)

Finding Environment Guarantees. - Marsha Chechik; Mihaela Gheorghiu; Arie Gurfinkel (FASE, 2007)

Algorithmic Analysis of Piecewise FIFO Systems. - Naghmeh Ghafari; Arie Gurfinkel; Nils Klarlund; Richard J. Trefler (FMCAD, 2007)

Finding State Solutions to Temporal Logic Queries. - Mihaela Gheorghiu; Arie Gurfinkel; Marsha Chechik (IFM, 2007)

A framework for counterexample generation and exploration. - Marsha Chechik; Arie Gurfinkel (Int. J. Softw. Tools Technol. Transf., 2007)

Model-checking with many values. - Arie Gurfinkel (2007)

Model Checking Recursive Programs with Exact Predicate Abstraction. - Arie Gurfinkel; Ou Wei; Marsha Chechik (ATVA, 2008)

Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates. - Thomas E. Hart; Kelvin Ku; Arie Gurfinkel; Marsha Chechik; David Lie (ASE, 2008)

PtYasm: Software Model Checking with Proof Templates. - Thomas E. Hart; Kelvin Ku; Arie Gurfinkel; Marsha Chechik; David Lie (ASE, 2008)

Decision diagrams for linear arithmetic. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2009)

Verification of Parameterized Systems with Combinations of Abstract Domains. - Naghmeh Ghafari; Arie Gurfinkel; Richard J. Trefler (FMOODS/FORTE, 2009)

Towards engineered architecture evolution. - Sagar Chaki; J. Andrés Díaz Pace; David Garlan; Arie Gurfinkel; Ipek Ozkaya (MiSE@ICSE, 2009)

Mixed Transition Systems Revisited. - Ou Wei; Arie Gurfinkel; Marsha Chechik (VMCAI, 2009)

Abstract Analysis of Symbolic Executions. - Aws Albarghouthi; Arie Gurfinkel; Ou Wei; Marsha Chechik (CAV, 2010)

Using Architecturally Significant Requirements for Guiding System Evolution. - Ipek Ozkaya; J. Andrés Díaz Pace; Arie Gurfinkel; Sagar Chaki (CSMR, 2010)

Variants of LTL Query Checking. - Hana Chockler; Arie Gurfinkel; Ofer Strichman (Haifa Verification Conference, 2010)

Boxes: A Symbolic Abstract Domain of Boxes. - Arie Gurfinkel; Sagar Chaki (SAS, 2010)

Combining predicate and numeric abstraction for software model checking. - Arie Gurfinkel; Sagar Chaki (Int. J. Softw. Tools Technol. Transf., 2010)

Exploiting resolution proofs to speed up LTL vacuity detection for BMC. - Jocelyn Simmonds; Jessica Davies 001; Arie Gurfinkel; Marsha Chechik (Int. J. Softw. Tools Technol. Transf., 2010)

Time-bounded analysis of real-time systems. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2011)

Supervised learning for provenance-similarity of binaries. - Sagar Chaki; Cory F. Cohen; Arie Gurfinkel (KDD, 2011)

Efficient Predicate Abstraction of Program Summaries. - Arie Gurfinkel; Sagar Chaki; Samir Sapra (NASA Formal Methods, 2011)

CSSL: a logic for specifying conditional scenarios. - Shoham Ben-David; Marsha Chechik; Arie Gurfinkel; Sebastián Uchitel (SIGSOFT FSE, 2011)

On the consistency, expressiveness, and precision of partial modeling formalisms. - Ou Wei; Arie Gurfinkel; Marsha Chechik (Inf. Comput., 2011)

Automated assume-guarantee reasoning for omega-regular systems and specifications. - Sagar Chaki; Arie Gurfinkel (Innov. Syst. Softw. Eng., 2011)

Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. - Aws Albarghouthi; Yi Li 008; Arie Gurfinkel; Marsha Chechik (CAV, 2012)

Binary Function Clustering Using Semantic Hashes. - Wesley Jin; Sagar Chaki; Cory F. Cohen; Arie Gurfinkel; Jeffrey Havrilla; Charles Hines; Priya Narasimhan (ICMLA (1), 2012)

Craig Interpretation. - Aws Albarghouthi; Arie Gurfinkel; Marsha Chechik (SAS, 2012)

From Under-Approximations to Over-Approximations and Back. - Aws Albarghouthi; Arie Gurfinkel; Marsha Chechik (TACAS, 2012)

Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. - Aws Albarghouthi; Arie Gurfinkel; Marsha Chechik (VMCAI, 2012)

Regression Verification for Multi-threaded Programs. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (VMCAI, 2012)

Propositional Interpolation Systems for Model Checking - Arie Gurfinkel; Simone Fulvio Rollini; Natasha Sharygina (CoRR, 2012)

Reachability Problems in Piecewise FIFO Systems. - Naghmeh Ghafari; Arie Gurfinkel; Nils Klarlund; Richard J. Trefler (ACM Trans. Comput. Log., 2012)

Robust Vacuity for Branching Temporal Logic. - Arie Gurfinkel; Marsha Chechik (ACM Trans. Comput. Log., 2012)

Interpolation Properties and SAT-Based Model Checking. - Arie Gurfinkel; Simone Fulvio Rollini; Natasha Sharygina (ATVA, 2013)

Automatic Abstraction in SMT-Based Unbounded Software Model Checking. - Anvesh Komuravelli; Arie Gurfinkel; Sagar Chaki; Edmund M. Clarke (CAV, 2013)

Verifying periodic programs with priority inheritance locks. - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (FMCAD, 2013)

Instantiations, Zippers and EPR Interpolation. - Nikolaj S. Bjørner; Arie Gurfinkel; Konstantin Korovin; Ori Lahav 001 (LPAR (short papers), 2013)

Finding Errors in Python Programs Using Dynamic Symbolic Execution. - Samir Sapra; Marius Minea; Sagar Chaki; Arie Gurfinkel; Edmund M. Clarke (ICTSS, 2013)

UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). - Aws Albarghouthi; Arie Gurfinkel; Yi Li 008; Sagar Chaki; Marsha Chechik (TACAS, 2013)

Compositional Sequentialization of Periodic Programs. - Sagar Chaki; Arie Gurfinkel; Soonho Kong; Ofer Strichman (VMCAI, 2013)

Beyond vacuity: towards the strongest passing formula. - Hana Chockler; Arie Gurfinkel; Ofer Strichman (Formal Methods Syst. Des., 2013)

Interpolating Property Directed Reachability. - Yakir Vizel; Arie Gurfinkel (CAV, 2014)

Efficient verification of periodic programs using sequential consistency and snapshots. - Sagar Chaki; Arie Gurfinkel; Nishant Sinha 001 (FMCAD, 2014)

DRUPing for interpolates. - Arie Gurfinkel; Yakir Vizel (FMCAD, 2014)

Small inductive safe invariants. - Alexander Ivrii; Arie Gurfinkel; Anton Belov (FMCAD, 2014)

Incremental Verification of Compiler Optimizations. - Grigory Fedyukovich; Arie Gurfinkel; Natasha Sharygina (NASA Formal Methods, 2014)

Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis. - Wesley Jin; Cory F. Cohen; Jeffrey Gennari; Charles Hines; Sagar Chaki; Arie Gurfinkel; Jeffrey Havrilla; Priya Narasimhan (PPREW@POPL, 2014)

Symbolic optimization with SMT solvers. - Yi Li 008; Aws Albarghouthi; Zachary Kincaid; Arie Gurfinkel; Marsha Chechik (POPL, 2014)

FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). - Arie Gurfinkel; Anton Belov (TACAS, 2014)

Synthesizing Safe Bit-Precise Invariants. - Arie Gurfinkel; Anton Belov; João Marques-Silva 001 (TACAS, 2014)

Synthesizing Modular Invariants for Synchronous Code. - Pierre-Loïc Garoche; Arie Gurfinkel; Temesghen Kahsai (HCVS, 2014)

Horn Clause Solvers for Program Verification. - Nikolaj S. Bjørner; Arie Gurfinkel; Kenneth L. McMillan; Andrey Rybalchenko (Fields of Logic and Computation II, 2015)

The SeaHorn Verification Framework. - Arie Gurfinkel; Temesghen Kahsai; Anvesh Komuravelli; Jorge A. Navas (CAV (1), 2015)

Fast Interpolating BMC. - Yakir Vizel; Arie Gurfinkel; Sharad Malik (CAV (1), 2015)

Pushing to the Top. - Arie Gurfinkel; Alexander Ivrii (FMCAD, 2015)

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. - Anvesh Komuravelli; Nikolaj S. Bjørner; Arie Gurfinkel; Kenneth L. McMillan (FMCAD, 2015)

Automated Discovery of Simulation Between Programs. - Grigory Fedyukovich; Arie Gurfinkel; Natasha Sharygina (LPAR, 2015)

Algorithmic Logic-Based Verification with SeaHorn. - Arie Gurfinkel (SYNASC, 2015)

SeaHorn: A Framework for Verifying C Programs (Competition Contribution). - Arie Gurfinkel; Temesghen Kahsai; Jorge A. Navas (TACAS, 2015)

Property Directed Polyhedral Abstraction. - Nikolaj S. Bjørner; Arie Gurfinkel (VMCAI, 2015)

Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). - Sagar Chaki; Arie Gurfinkel; Ofer Strichman (Formal Methods Syst. Des., 2015)

Algorithmic logic-based verification. - Arie Gurfinkel; Temesghen Kahsai; Jorge A. Navas (ACM SIGLOG News, 2015)

Property Directed Equivalence via Abstract Simulation. - Grigory Fedyukovich; Arie Gurfinkel; Natasha Sharygina (CAV (2), 2016)

Maximal specification synthesis. - Aws Albarghouthi; Isil Dillig; Arie Gurfinkel (POPL, 2016)

CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. - Adrien Champion; Arie Gurfinkel; Temesghen Kahsai; Cesare Tinelli (SEFM, 2016)

SMT-based verification of parameterized systems. - Arie Gurfinkel; Sharon Shoham; Yuri Meshman (SIGSOFT FSE, 2016)

Synthesizing Ranking Functions from Bits and Pieces. - Caterina Urban; Arie Gurfinkel; Temesghen Kahsai (TACAS, 2016)

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. - Andreas Katis; Grigory Fedyukovich; Andrew Gacek; John D. Backes; Arie Gurfinkel; Michael W. Whalen (CoRR, 2016)

SMT-based model checking for recursive programs. - Anvesh Komuravelli; Arie Gurfinkel; Sagar Chaki (Formal Methods Syst. Des., 2016)

K-induction without unrolling. - Arie Gurfinkel; Alexander Ivrii (FMCAD, 2017)

Designing parallel PDR. - Matteo Marescotti; Arie Gurfinkel; Antti Eero Johannes Hyvärinen; Natasha Sharygina (FMCAD, 2017)

Automated analysis of Stateflow models. - Hamza Bourbouh; Pierre-Loïc Garoche; Christophe Garion; Arie Gurfinkel; Temesghen Kahsai; Xavier Thirioux (LPAR, 2017)

A Context-Sensitive Memory Model for Verification of C/C++ Programs. - Arie Gurfinkel; Jorge A. Navas (SAS, 2017)

IC3 - Flipping the E in ICE. - Yakir Vizel; Arie Gurfinkel; Sharon Shoham; Sharad Malik (VMCAI, 2017)

Quantifiers on Demand. - Arie Gurfinkel; Sharon Shoham; Yakir Vizel (ATVA, 2018)

Predictive Run-Time Verification of Discrete-Time Reachability Properties in Black-Box Systems Using Trace-Level Abstraction and Statistical Learning. - Reza Babaee; Arie Gurfinkel; Sebastian Fischmeister (RV, 2018)

Prevent : A Predictive Run-Time Verification Framework Using Statistical Learning. - Reza Babaee; Arie Gurfinkel; Sebastian Fischmeister (SEFM, 2018)

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. - Andreas Katis; Grigory Fedyukovich; Huajun Guo; Andrew Gacek; John Backes; Arie Gurfinkel; Michael W. Whalen (TACAS (2), 2018)

Executable Counterexamples in Software Model Checking. - Jeffrey Gennari; Arie Gurfinkel; Temesghen Kahsai; Jorge A. Navas; Edward J. Schwartz (VSTTE, 2018)

BDD-Based Symbolic Model Checking. - Sagar Chaki; Arie Gurfinkel (Handbook of Model Checking, 2018)

Interpolating Strong Induction. - Hari Govind Vediramana Krishnan; Yakir Vizel; Vijay Ganesh 001; Arie Gurfinkel (CAV (2), 2019)

Property Directed Self Composition. - Ron Shemer; Arie Gurfinkel; Sharon Shoham; Yakir Vizel (CAV (1), 2019)

Unification-based Pointer Analysis without Oversharing. - Jakub Kuderski; Jorge A. Navas; Arie Gurfinkel (FMCAD, 2019)

Local Reasoning for Parameterized First Order Protocols. - Rylo Ashmore; Arie Gurfinkel; Richard J. Trefler (NFM, 2019)

Simple and precise static analysis of untrusted Linux kernel extensions. - Elazar Gershuni; Nadav Amit; Arie Gurfinkel; Nina Narodytska; Jorge A. Navas; Noam Rinetzky; Leonid Ryzhyk; Mooly Sagiv (PLDI, 2019)

The Science, Art, and Magic of Constrained Horn Clauses. - Arie Gurfinkel; Nikolaj S. Bjørner (SYNASC, 2019)

Lazy but Effective Functional Synthesis. - Grigory Fedyukovich; Arie Gurfinkel; Aarti Gupta (VMCAI, 2019)

Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. - Hongce Zhang; Maxwell Shinn; Aarti Gupta; Arie Gurfinkel; Nham Le; Nina Narodytska (ECAI, 2020)

Word Level Property Directed Reachability. - Hari Govind V. K.; Grigory Fedyukovich; Arie Gurfinkel (ICCAD, 2020)

IC3 with Internal Signals. - Rohit Dureja; Arie Gurfinkel; Alexander Ivrii; Yakir Vizel (FMCAD, 2021)

Logical Characterization of Coherent Uninterpreted Programs. - Hari Govind V. K.; Sharon Shoham; Arie Gurfinkel (FMCAD, 2021)

Data-driven Optimization of Inductive Generalization. - Nham Le; Xujie Si; Arie Gurfinkel (FMCAD, 2021)

Compositional Verification of Smart Contracts Through Communication Abstraction. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (SAS, 2021)

Abstract Interpretation of LLVM with a Region-Based Memory Model. - Arie Gurfinkel; Jorge A. Navas (VSTTE, 2021)

Compositional Verification of Smart Contracts Through Communication Abstraction (Extended). - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (CoRR, 2021)

Preface of the special issue on the conference on formal methods in computer aided design 2018. - Nikolaj S. Bjørner; Arie Gurfinkel (Formal Methods Syst. Des., 2021)

Program Verification with Constrained Horn Clauses (Invited Paper). - Arie Gurfinkel (CAV (1), 2022)

Bounded Model Checking for LLVM. - Siddharth Priya; Yusen Su; Yuyan Bao; Xiang Zhou; Yakir Vizel; Arie Gurfinkel (FMCAD, 2022)

Efficient Modular SMT-Based Model Checking of Pointer Programs. - Isabel Garcia-Contreras; Arie Gurfinkel; Jorge A. Navas (SAS, 2022)

Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (VMCAI, 2022)

Toward Reliable Neural Specifications. - Chuqin Geng; Nham Le; Xiaojie Xu; Zhaoyue Wang; Arie Gurfinkel; Xujie Si (CoRR, 2022)

Verifying verified code. - Siddharth Priya; Xiang Zhou; Yusen Su; Yakir Vizel; Yuyan Bao; Arie Gurfinkel (Innov. Syst. Softw. Eng., 2022)

Solving constrained Horn clauses modulo algebraic data types and recursive functions. - Hari Govind V. K.; Sharon Shoham; Arie Gurfinkel (Proc. ACM Program. Lang., 2022)

Fast Approximations of Quantifier Elimination. - Isabel Garcia-Contreras; Hari Govind V. K.; Sharon Shoham; Arie Gurfinkel (CAV (2), 2023)

BTOR2MLIR: A Format and Toolchain for Hardware Verification. - Joseph Tafese; Isabel Garcia-Contreras; Arie Gurfinkel (FMCAD, 2023)

Towards Reliable Neural Specifications. - Chuqin Geng; Nham Le; Xiaojie Xu; Zhaoyue Wang; Arie Gurfinkel; Xujie Si (ICML, 2023)

Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). - Arie Gurfinkel; Isabella Mastroeni; Antoine Miné; Peter Müller 001; Anna Becchi (Dagstuhl Reports, 2023)

Towards Robust Saliency Maps. - Nham Le; Arie Gurfinkel; Xujie Si; Chuqin Geng (ACML, 2024)

Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). - Arie Gurfinkel (CONCUR, 2024)

Inductive Predicate Synthesis Modulo Programs. - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (ECOOP, 2024)

Ownership in Low-Level Intermediate Representation. - Siddharth Priya; Arie Gurfinkel (FMCAD, 2024)

Efficient Simulation for Hardware Model Checking. - Joseph Tafese; Arie Gurfinkel (LPAR, 2024)

Unlocking the Power of Environment Assumptions for Unit Proofs. - Siddharth Priya; Temesghen Kahsai; Arie Gurfinkel (SEFM, 2024)

Speculative SAT Modulo SAT. - Hari Govind V. K.; Isabel Garcia-Contreras; Sharon Shoham; Arie Gurfinkel (TACAS (1), 2024)

Inductive Predicate Synthesis Modulo Programs (Extended). - Scott Wesley; Maria Christakis; Jorge A. Navas; Richard J. Trefler; Valentin Wüstholz; Arie Gurfinkel (CoRR, 2024)

Global guidance for local generalization in model checking. - Hari Govind Vediramana Krishnan; Yuting Chen; Sharon Shoham; Arie Gurfinkel (Formal Methods Syst. Des., 2024)

Relatively Complete and Efficient Partial Quantifier Elimination. - Estifanos Getachew; Arie Gurfinkel; Richard J. Trefler (CADE, 2025)

Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking. - Zhengyang Lu 002; Po-Chun Chien; Nian-Ze Lee; Arie Gurfinkel; Vijay Ganesh 001 (CAV (1), 2025)

Automatic Inference of Relational Object Invariants. - Yusen Su; Jorge A. Navas; Arie Gurfinkel; Isabel Garcia-Contreras (VMCAI (1), 2025)