Arie Gurfinkel

ORCID

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 62

Top Venues

Publications

Arie Gurfinkel
Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). CONCUR (2024)
Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
Speculative SAT Modulo SAT. TACAS (1) (2024)
Joseph Tafese, Arie Gurfinkel
Efficient Simulation for Hardware Model Checking. LPAR (2024)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Inductive Predicate Synthesis Modulo Programs (Extended). CoRR (2024)
Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, Anna Becchi
Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). Dagstuhl Reports 13 (7) (2023)
Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si
Towards Reliable Neural Specifications. ICML (2023)
Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel
Btor2MLIR: A Format and Toolchain for Hardware Verification. CoRR (2023)
Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
Speculative SAT Modulo SAT. CoRR (2023)
Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Fast Approximations of Quantifier Elimination. CAV (2) (2023)
Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel
BTOR2MLIR: A Format and Toolchain for Hardware Verification. FMCAD (2023)
Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Fast Approximations of Quantifier Elimination. CoRR (2023)
Arie Gurfinkel
Program Verification with Constrained Horn Clauses (Invited Paper). CAV (1) (2022)
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6 (POPL) (2022)
Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel
Bounded Model Checking for LLVM. FMCAD (2022)
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
Verifying verified code. Innov. Syst. Softw. Eng. 18 (3) (2022)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. VMCAI (2022)
Isabel Garcia-Contreras, Arie Gurfinkel, Jorge A. Navas
Efficient Modular SMT-Based Model Checking of Pointer Programs. SAS (2022)
Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si
Toward Reliable Neural Specifications. CoRR (2022)
Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, Yakir Vizel
IC3 with Internal Signals. FMCAD (2021)
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Logical Characterization of Coherent Uninterpreted Programs. FMCAD (2021)
Nikolaj Bjørner, Arie Gurfinkel
Preface of the special issue on the conference on formal methods in computer aided design 2018. Formal Methods Syst. Des. 57 (2) (2021)
Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
Logical Characterization of Coherent Uninterpreted Programs. CoRR (2021)
Nham Le, Xujie Si, Arie Gurfinkel
Data-driven Optimization of Inductive Generalization. FMCAD (2021)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Compositional Verification of Smart Contracts Through Communication Abstraction. SAS (2021)
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
Verifying Verified Code. ATVA (2021)
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Quantifiers on Demand. CoRR (2021)
Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
Verifying Verified Code. CoRR (2021)
Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended). CoRR (2021)
Arie Gurfinkel, Jorge A. Navas
Abstract Interpretation of LLVM with a Region-Based Memory Model. VSTTE (2021)
Hari Govind V. K., Grigory Fedyukovich, Arie Gurfinkel
Word Level Property Directed Reachability. ICCAD (2020)
Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel
Global Guidance for Local Generalization in Model Checking. CAV (2) (2020)
Hari Govind V. K., Yuting Chen, Sharon Shoham, Arie Gurfinkel
Global Guidance for Local Generalization in Model Checking. CoRR (2020)
Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, Nina Narodytska
Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. ECAI (2020)
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Unification-based Pointer Analysis without Oversharing. CoRR (2019)
Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler
Local Reasoning for Parameterized First Order Protocols. NFM (2019)
Arie Gurfinkel, Nikolaj Bjørner
The Science, Art, and Magic of Constrained Horn Clauses. SYNASC (2019)
Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
Lazy but Effective Functional Synthesis. VMCAI (2019)
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Unification-based Pointer Analysis without Oversharing. FMCAD (2019)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Property Directed Self Composition. CAV (1) (2019)
Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Property Directed Self Composition. CoRR (2019)
Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler
Local Reasoning for Parameterized First Order Protocols. CoRR (2019)
Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv
Simple and precise static analysis of untrusted Linux kernel extensions. PLDI (2019)
Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
Interpolating Strong Induction. CAV (2) (2019)
Hari Govind V. K., Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
Interpolating Strong Induction. CoRR (2019)
Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz
Executable Counterexamples in Software Model Checking. VSTTE (2018)
Arie Gurfinkel, Sharon Shoham, Yakir Vizel
Quantifiers on Demand. ATVA (2018)
Reza Babaee, Arie Gurfinkel, Sebastian Fischmeister
Predictive Run-Time Verification of Discrete-Time Reachability Properties in Black-Box Systems Using Trace-Level Abstraction and Statistical Learning. RV (2018)
Reza Babaee, Arie Gurfinkel, Sebastian Fischmeister
revent : A Predictive Run-Time Verification Framework Using Statistical Learning. SEFM (2018)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) (2018)
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. CoRR (2017)
Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, Natasha Sharygina
Designing parallel PDR. FMCAD (2017)
Arie Gurfinkel, Alexander Ivrii
K-induction without unrolling. FMCAD (2017)
Arie Gurfinkel, Jorge A. Navas
A Context-Sensitive Memory Model for Verification of C/C++ Programs. SAS (2017)
Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik
IC3 - Flipping the E in ICE. VMCAI (2017)
Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux
Automated analysis of Stateflow models. LPAR (2017)
Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli
CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. SEFM (2016)
Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, Michael W. Whalen
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR (2016)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Property Directed Equivalence via Abstract Simulation. CAV (2) (2016)
Caterina Urban, Arie Gurfinkel, Temesghen Kahsai
Synthesizing Ranking Functions from Bits and Pieces. TACAS (2016)
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48 (3) (2016)
Aws Albarghouthi, Isil Dillig, Arie Gurfinkel
Maximal specification synthesis. POPL (2016)
Arie Gurfinkel, Sharon Shoham, Yuri Meshman
SMT-based verification of parameterized systems. SIGSOFT FSE (2016)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). Formal Methods Syst. Des. 47 (3) (2015)
Nikolaj Bjørner, Arie Gurfinkel
Property Directed Polyhedral Abstraction. VMCAI (2015)
Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR (2015)
Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas
Algorithmic logic-based verification. ACM SIGLOG News 2 (2) (2015)
Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas
SeaHorn: A Framework for Verifying C Programs (Competition Contribution). TACAS (2015)
Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II (2015)
Arie Gurfinkel, Alexander Ivrii
Pushing to the Top. FMCAD (2015)
Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD (2015)
Yakir Vizel, Arie Gurfinkel, Sharad Malik
Fast Interpolating BMC. CAV (1) (2015)
Arie Gurfinkel
Algorithmic Logic-Based Verification with SeaHorn. SYNASC (2015)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Automated Discovery of Simulation Between Programs. LPAR (2015)
Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas
The SeaHorn Verification Framework. CAV (1) (2015)
Wesley Jin, Cory F. Cohen, Jeffrey Gennari, Charles Hines, Sagar Chaki, Arie Gurfinkel, Jeffrey Havrilla, Priya Narasimhan
Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis. PPREW@POPL (2014)
Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
Incremental Verification of Compiler Optimizations. NASA Formal Methods (2014)
Alexander Ivrii, Arie Gurfinkel, Anton Belov
Small inductive safe invariants. FMCAD (2014)
Arie Gurfinkel, Anton Belov, João Marques-Silva
Synthesizing Safe Bit-Precise Invariants. TACAS (2014)
Arie Gurfinkel, Yakir Vizel
DRUPing for interpolates. FMCAD (2014)
Arie Gurfinkel, Anton Belov
FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). TACAS (2014)
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
SMT-based Model Checking for Recursive Programs. CoRR (2014)
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
SMT-Based Model Checking for Recursive Programs. CAV (2014)
Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik
Symbolic optimization with SMT solvers. POPL (2014)
Pierre-Loïc Garoche, Arie Gurfinkel, Temesghen Kahsai
Synthesizing Modular Invariants for Synchronous Code. HCVS (2014)
Sagar Chaki, Arie Gurfinkel, Nishant Sinha
Efficient verification of periodic programs using sequential consistency and snapshots. FMCAD (2014)
Yakir Vizel, Arie Gurfinkel
Interpolating Property Directed Reachability. CAV (2014)
Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik
UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). TACAS (2013)
Hana Chockler, Arie Gurfinkel, Ofer Strichman
Beyond vacuity: towards the strongest passing formula. Formal Methods Syst. Des. 43 (3) (2013)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Verifying periodic programs with priority inheritance locks. FMCAD (2013)
Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
Interpolation Properties and SAT-Based Model Checking. ATVA (2013)
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CoRR (2013)
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CAV (2013)
Samir Sapra, Marius Minea, Sagar Chaki, Arie Gurfinkel, Edmund M. Clarke
Finding Errors in Python Programs Using Dynamic Symbolic Execution. ICTSS (2013)
Nikolaj Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) (2013)
Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman
Compositional Sequentialization of Periodic Programs. VMCAI (2013)
Aws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. CAV (2012)
Arie Gurfinkel, Marsha Chechik
Robust Vacuity for Branching Temporal Logic. ACM Trans. Comput. Log. 13 (1) (2012)
Wesley Jin, Sagar Chaki, Cory F. Cohen, Arie Gurfinkel, Jeffrey Havrilla, Charles Hines, Priya Narasimhan
Binary Function Clustering Using Semantic Hashes. ICMLA (1) (2012)
Sagar Chaki, Arie Gurfinkel, Ofer Strichman
Regression Verification for Multi-threaded Programs. VMCAI (2012)
Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
Propositional Interpolation Systems for Model Checking CoRR (2012)

Arie Gurfinkel.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Arie Gurfinkel