Arie Gurfinkel
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
105
Venues
27
Active years
2002–2026
Best venue rank
A*
Where they publish
- BFMCAD23 papers
- A*CAV18 papers
- ATACAS12 papers
- BVMCAI10 papers
- BSAS5 papers
- BLPAR4 papers
- BSEFM4 papers
- BATVA4 papers
- A*POPL3 papers
- BCONCUR2 papers
- NationalSYNASC2 papers
- A*ICSE2 papers
- BFASE2 papers
- ACP1 paper
- ACADE1 paper
- CACML1 paper
- AECOOP1 paper
- A*ICML1 paper
- AECAI1 paper
- AICCAD1 paper
- A*PLDI1 paper
- BRV1 paper
- CICMLA1 paper
- A*KDD1 paper
- CFORTE1 paper
- BIFM1 paper
- BFM1 paper
Papers
105 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | CAV | Show Me The Money: An Exercise in Proof-Driven Software Understanding. | Joseph Tafese, Karthik Nukala, Hassen Sadi, Natarajan Shankar, Arie Gurfinkel, Giuliano Losa |
| 2026 | CP | Learning Unified Graph and Language Representations for SMT Algorithm Selection. | Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, Vijay Ganesh |
| 2026 | TACAS | Syntactically Convex Model-Based Projection for Linear Real Arithmetic. | Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel, Lev Nachmanson |
| 2025 | CADE | Relatively Complete and Efficient Partial Quantifier Elimination. | Estifanos Getachew, Arie Gurfinkel, Richard J. Trefler |
| 2025 | CAV | Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking. | Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, Arie Gurfinkel, Vijay Ganesh |
| 2025 | FMCAD | A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SEABMC. | Joseph Tafese, Siddharth Priya, Giuliano Losa, Arie Gurfinkel, Graydon Hoare |
| 2025 | VMCAI | Automatic Inference of Relational Object Invariants. | Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras |
| 2024 | ACML | Towards Robust Saliency Maps. | Nham Le, Arie Gurfinkel, Xujie Si, Chuqin Geng |
| 2024 | CONCUR | Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). | Arie Gurfinkel |
| 2024 | ECOOP | Inductive Predicate Synthesis Modulo Programs. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2024 | FMCAD | Ownership in Low-Level Intermediate Representation. | Siddharth Priya, Arie Gurfinkel |
| 2024 | LPAR | Efficient Simulation for Hardware Model Checking. | Joseph Tafese, Arie Gurfinkel |
| 2024 | SEFM | Unlocking the Power of Environment Assumptions for Unit Proofs. | Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel |
| 2024 | TACAS | Speculative SAT Modulo SAT. | Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel |
| 2023 | CAV | Fast Approximations of Quantifier Elimination. | Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel |
| 2023 | FMCAD | BTOR2MLIR: A Format and Toolchain for Hardware Verification. | Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel |
| 2023 | ICML | Towards Reliable Neural Specifications. | Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si |
| 2022 | CAV | Program Verification with Constrained Horn Clauses (Invited Paper). | Arie Gurfinkel |
| 2022 | FMCAD | Bounded Model Checking for LLVM. | Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel |
| 2022 | SAS | Efficient Modular SMT-Based Model Checking of Pointer Programs. | Isabel Garcia-Contreras, Arie Gurfinkel, Jorge A. Navas |
| 2022 | VMCAI | Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2021 | ATVA | Verifying Verified Code. | Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel |
| 2021 | FMCAD | IC3 with Internal Signals. | Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, Yakir Vizel |
| 2021 | FMCAD | Logical Characterization of Coherent Uninterpreted Programs. | Hari Govind V. K., Sharon Shoham, Arie Gurfinkel |
| 2021 | FMCAD | Data-driven Optimization of Inductive Generalization. | Nham Le, Xujie Si, Arie Gurfinkel |
| 2021 | SAS | Compositional Verification of Smart Contracts Through Communication Abstraction. | Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wstholz, Arie Gurfinkel |
| 2020 | CAV | Global Guidance for Local Generalization in Model Checking. | Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel |
| 2020 | ECAI | Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. | Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, Nina Narodytska |
| 2020 | ICCAD | Word Level Property Directed Reachability. | Hari Govind V. K., Grigory Fedyukovich, Arie Gurfinkel |
| 2019 | CAV | Interpolating Strong Induction. | Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel |
| 2019 | CAV | Property Directed Self Composition. | Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel |
| 2019 | FMCAD | Unification-based Pointer Analysis without Oversharing. | Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel |
| 2019 | PLDI | 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 |
| 2019 | SYNASC | The Science, Art, and Magic of Constrained Horn Clauses. | Arie Gurfinkel, Nikolaj S. Bjrner |
| 2019 | VMCAI | Lazy but Effective Functional Synthesis. | Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta |
| 2018 | ATVA | Quantifiers on Demand. | Arie Gurfinkel, Sharon Shoham, Yakir Vizel |
| 2018 | RV | 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 |
| 2018 | SEFM | Untitled record | Reza Babaee, Arie Gurfinkel, Sebastian Fischmeister |
| 2018 | TACAS | 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 |
| 2017 | FMCAD | K-induction without unrolling. | Arie Gurfinkel, Alexander Ivrii |
| 2017 | FMCAD | Designing parallel PDR. | Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvrinen, Natasha Sharygina |
| 2017 | LPAR | Automated analysis of Stateflow models. | Hamza Bourbouh, Pierre-Loc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux |
| 2017 | SAS | A Context-Sensitive Memory Model for Verification of C/C++ Programs. | Arie Gurfinkel, Jorge A. Navas |
| 2017 | VMCAI | IC3 - Flipping the E in ICE. | Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik |
| 2016 | CAV | Property Directed Equivalence via Abstract Simulation. | Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina |
| 2016 | POPL | Maximal specification synthesis. | Aws Albarghouthi, Isil Dillig, Arie Gurfinkel |
| 2016 | SEFM | CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. | Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli |
| 2016 | TACAS | Synthesizing Ranking Functions from Bits and Pieces. | Caterina Urban, Arie Gurfinkel, Temesghen Kahsai |
| 2015 | CAV | The SeaHorn Verification Framework. | Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas |
| 2015 | CAV | Fast Interpolating BMC. | Yakir Vizel, Arie Gurfinkel, Sharad Malik |
| 2015 | FMCAD | Pushing to the Top. | Arie Gurfinkel, Alexander Ivrii |
| 2015 | FMCAD | Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. | Anvesh Komuravelli, Nikolaj S. Bjrner, Arie Gurfinkel, Kenneth L. McMillan |
| 2015 | LPAR | Automated Discovery of Simulation Between Programs. | Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina |
| 2015 | SYNASC | Algorithmic Logic-Based Verification with SeaHorn. | Arie Gurfinkel |
| 2015 | TACAS | SeaHorn: A Framework for Verifying C Programs (Competition Contribution). | Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas |
| 2015 | VMCAI | Property Directed Polyhedral Abstraction. | Nikolaj S. Bjrner, Arie Gurfinkel |
| 2014 | CAV | SMT-Based Model Checking for Recursive Programs. | Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki |
| 2014 | CAV | Interpolating Property Directed Reachability. | Yakir Vizel, Arie Gurfinkel |
| 2014 | FMCAD | Efficient verification of periodic programs using sequential consistency and snapshots. | Sagar Chaki, Arie Gurfinkel, Nishant Sinha |
| 2014 | FMCAD | DRUPing for interpolates. | Arie Gurfinkel, Yakir Vizel |
| 2014 | FMCAD | Small inductive safe invariants. | Alexander Ivrii, Arie Gurfinkel, Anton Belov |
| 2014 | POPL | 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 |
| 2014 | POPL | Symbolic optimization with SMT solvers. | Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik |
| 2014 | TACAS | FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). | Arie Gurfinkel, Anton Belov |
| 2014 | TACAS | Synthesizing Safe Bit-Precise Invariants. | Arie Gurfinkel, Anton Belov, Joo Marques-Silva |
| 2013 | ATVA | Interpolation Properties and SAT-Based Model Checking. | Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina |
| 2013 | CAV | Automatic Abstraction in SMT-Based Unbounded Software Model Checking. | Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke |
| 2013 | FMCAD | Verifying periodic programs with priority inheritance locks. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2013 | LPAR | Instantiations, Zippers and EPR Interpolation. | Nikolaj S. Bjrner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav |
| 2013 | TACAS | UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). | Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik |
| 2013 | VMCAI | Compositional Sequentialization of Periodic Programs. | Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman |
| 2012 | CAV | Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. | Aws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik |
| 2012 | ICMLA | Binary Function Clustering Using Semantic Hashes. | Wesley Jin, Sagar Chaki, Cory F. Cohen, Arie Gurfinkel, Jeffrey Havrilla, Charles Hines, Priya Narasimhan |
| 2012 | SAS | Craig Interpretation. | Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik |
| 2012 | TACAS | From Under-Approximations to Over-Approximations and Back. | Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik |
| 2012 | VMCAI | Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. | Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik |
| 2012 | VMCAI | Regression Verification for Multi-threaded Programs. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2011 | FMCAD | Time-bounded analysis of real-time systems. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2011 | KDD | Supervised learning for provenance-similarity of binaries. | Sagar Chaki, Cory F. Cohen, Arie Gurfinkel |
| 2010 | CAV | Abstract Analysis of Symbolic Executions. | Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2010 | SAS | Boxes: A Symbolic Abstract Domain of Boxes. | Arie Gurfinkel, Sagar Chaki |
| 2009 | FMCAD | Decision diagrams for linear arithmetic. | Sagar Chaki, Arie Gurfinkel, Ofer Strichman |
| 2009 | FORTE | Verification of Parameterized Systems with Combinations of Abstract Domains. | Naghmeh Ghafari, Arie Gurfinkel, Richard J. Trefler |
| 2009 | ICSE | Towards engineered architecture evolution. | Sagar Chaki, J. Andrs Daz Pace, David Garlan, Arie Gurfinkel, Ipek Ozkaya |
| 2009 | VMCAI | Mixed Transition Systems Revisited. | Ou Wei, Arie Gurfinkel, Marsha Chechik |
| 2008 | ATVA | Model Checking Recursive Programs with Exact Predicate Abstraction. | Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2008 | FMCAD | Beyond Vacuity: Towards the Strongest Passing Formula. | Hana Chockler, Arie Gurfinkel, Ofer Strichman |
| 2008 | FMCAD | Combining Predicate and Numeric Abstraction for Software Model Checking. | Arie Gurfinkel, Sagar Chaki |
| 2007 | FASE | Finding Environment Guarantees. | Marsha Chechik, Mihaela Gheorghiu, Arie Gurfinkel |
| 2007 | FMCAD | Algorithmic Analysis of Piecewise FIFO Systems. | Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler |
| 2007 | FMCAD | Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. | Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik |
| 2007 | IFM | Finding State Solutions to Temporal Logic Queries. | Mihaela Gheorghiu, Arie Gurfinkel, Marsha Chechik |
| 2006 | CAV | Yasm: A Software Model-Checker for Verification and Refutation. | Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2006 | TACAS | Why Waste a Perfectly Good Abstraction?. | Arie Gurfinkel, Marsha Chechik |
| 2006 | VMCAI | Systematic Construction of Abstractions for Model-Checking. | Arie Gurfinkel, Ou Wei, Marsha Chechik |
| 2005 | FASE | A Framework for Counterexample Generation and Exploration. | Marsha Chechik, Arie Gurfinkel |
| 2005 | SEFM | Stuttering Abstraction for Model Checkin. | Shiva Nejati, Arie Gurfinkel, Marsha Chechik |
| 2004 | FMCAD | Extending Extended Vacuity. | Arie Gurfinkel, Marsha Chechik |
| 2004 | TACAS | How Vacuous Is Vacuous? | Arie Gurfinkel, Marsha Chechik |
| 2003 | CAV | TLQSolver: A Temporal Logic Query Checker. | Marsha Chechik, Arie Gurfinkel |
| 2003 | CONCUR | Multi-Valued Model Checking via Classical Model Checking. | Arie Gurfinkel, Marsha Chechik |
| 2003 | FM | Generating Counterexamples for Multi-valued Model-Checking. | Arie Gurfinkel, Marsha Chechik |
| 2003 | ICSE | \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 |
| 2003 | TACAS | Proof-Like Counter-Examples. | Arie Gurfinkel, Marsha Chechik |
| 2002 | CAV | chi-Chek: A Multi-valued Model-Checker. | Marsha Chechik, Arie Gurfinkel, Benet Devereux |