Arie Gurfinkel

178 papers A* 16A 13B 54C 2Misc 2Journal 44Unranked 38

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Learning SMT Algorithm Selection with High-Level Natural-Language Descriptions. FoIKS Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, Vijay Ganesh
2026	—	`conf`	Syntactically Convex Model-Based Projection for Linear Real Arithmetic. TACAS (1) Anna Becchi, Grigory Fedyukovich, Arie Gurfinkel, Lev Nachmanson
2025	J	`jnl`	A Flow-Sensitive Refinement Type System for Verifying eBPF Programs. Proc. ACM Program. Lang. Ameer Hamza, Lucas Zavalía, Arie Gurfinkel, Jorge A. Navas, Grigory Fedyukovich
2025	B	`conf`	A Tale of Two Case Studies: A Unified Exploration of Rust Verification with SEABMC. FMCAD Joseph Tafese, Siddharth Priya, Giuliano Losa, Arie Gurfinkel, Graydon Hoare
2025	—	`conf`	Automatic Inference of Relational Object Invariants. VMCAI (1) Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras
2025	—	`conf`	Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking. CAV (1) Zhengyang Lu, Po-Chun Chien, Nian-Ze Lee, Arie Gurfinkel, Vijay Ganesh
2025	A	`conf`	Relatively Complete and Efficient Partial Quantifier Elimination. CADE Estifanos Getachew, Arie Gurfinkel, Richard J. Trefler
2025	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part I TACAS (1) Arie Gurfinkel, Marijn Heule
2025	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part II TACAS (2) Arie Gurfinkel, Marijn Heule
2025	—	`ed.`	Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3-8, 2025, Proceedings, Part III TACAS (3) Arie Gurfinkel, Marijn Heule
2024	J	`jnl`	Automatic Inference of Relational Object Invariants. CoRR Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras
2024	—	`ed.`	Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I CAV (1) Arie Gurfinkel, Vijay Ganesh
2024	—	`ed.`	Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II CAV (2) Arie Gurfinkel, Vijay Ganesh
2024	—	`ed.`	Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III CAV (3) Arie Gurfinkel, Vijay Ganesh
2024	B	`conf`	Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). CONCUR Arie Gurfinkel
2024	B	`conf`	Efficient Simulation for Hardware Model Checking. LPAR Joseph Tafese, Arie Gurfinkel
2024	J	`jnl`	Global guidance for local generalization in model checking. Formal Methods Syst. Des. Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel
2024	J	`jnl`	Inductive Predicate Synthesis Modulo Programs (Extended). CoRR Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2024	A	`conf`	Inductive Predicate Synthesis Modulo Programs. ECOOP Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2024	B	`conf`	Ownership in Low-Level Intermediate Representation. FMCAD Siddharth Priya, Arie Gurfinkel
2024	J	`jnl`	Ownership in low-level intermediate representation. CoRR Siddharth Priya, Arie Gurfinkel
2024	—	`conf`	Speculative SAT Modulo SAT. TACAS (1) Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
2024	C	`conf`	Towards Robust Saliency Maps. ACML Nham Le, Arie Gurfinkel, Xujie Si, Chuqin Geng
2024	B	`conf`	Unlocking the Power of Environment Assumptions for Unit Proofs. SEFM Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel
2024	J	`jnl`	Unlocking the Power of Environment Assumptions for Unit Proofs. CoRR Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel
2023	B	`conf`	BTOR2MLIR: A Format and Toolchain for Hardware Verification. FMCAD Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel
2023	J	`jnl`	Btor2MLIR: A Format and Toolchain for Hardware Verification. CoRR Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel
2023	—	`conf`	Fast Approximations of Quantifier Elimination. CAV (2) Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2023	J	`jnl`	Fast Approximations of Quantifier Elimination. CoRR Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2023	J	`jnl`	Speculative SAT Modulo SAT. CoRR Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel
2023	J	`jnl`	Theoretical Advances and Emerging Applications in Abstract Interpretation (Dagstuhl Seminar 23281). Dagstuhl Reports Arie Gurfinkel, Isabella Mastroeni, Antoine Miné, Peter Müller, Anna Becchi
2023	A*	`conf`	Towards Reliable Neural Specifications. ICML Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si
2022	B	`conf`	Bounded Model Checking for LLVM. FMCAD Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel
2022	B	`conf`	Efficient Modular SMT-Based Model Checking of Pointer Programs. SAS Isabel Garcia-Contreras, Arie Gurfinkel, Jorge A. Navas
2022	—	`conf`	Program Verification with Constrained Horn Clauses (Invited Paper). CAV (1) Arie Gurfinkel
2022	J	`jnl`	Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2022	J	`jnl`	Toward Reliable Neural Specifications. CoRR Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si
2022	B	`conf`	Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. VMCAI Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2022	J	`jnl`	Verifying verified code. Innov. Syst. Softw. Eng. Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2021	—	`conf`	Abstract Interpretation of LLVM with a Region-Based Memory Model. VSTTE Arie Gurfinkel, Jorge A. Navas
2021	J	`jnl`	Compositional Verification of Smart Contracts Through Communication Abstraction (Extended). CoRR Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2021	B	`conf`	Compositional Verification of Smart Contracts Through Communication Abstraction. SAS Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel
2021	B	`conf`	Data-driven Optimization of Inductive Generalization. FMCAD Nham Le, Xujie Si, Arie Gurfinkel
2021	B	`conf`	IC3 with Internal Signals. FMCAD Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, Yakir Vizel
2021	B	`conf`	Logical Characterization of Coherent Uninterpreted Programs. FMCAD Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2021	J	`jnl`	Logical Characterization of Coherent Uninterpreted Programs. CoRR Hari Govind V. K., Sharon Shoham, Arie Gurfinkel
2021	J	`jnl`	Preface of the special issue on the conference on formal methods in computer aided design 2018. Formal Methods Syst. Des. Nikolaj S. Bjørner, Arie Gurfinkel
2021	J	`jnl`	Quantifiers on Demand. CoRR Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2021	B	`conf`	Verifying Verified Code. ATVA Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2021	J	`jnl`	Verifying Verified Code. CoRR Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel
2020	—	`conf`	Global Guidance for Local Generalization in Model Checking. CAV (2) Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel
2020	J	`jnl`	Global Guidance for Local Generalization in Model Checking. CoRR Hari Govind V. K., Yuting Chen, Sharon Shoham, Arie Gurfinkel
2020	A	`conf`	Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. ECAI Hongce Zhang, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, Nina Narodytska
2020	A	`conf`	Word Level Property Directed Reachability. ICCAD Hari Govind V. K., Grigory Fedyukovich, Arie Gurfinkel
2019	—	`conf`	Interpolating Strong Induction. CAV (2) Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
2019	J	`jnl`	Interpolating Strong Induction. CoRR Hari Govind V. K., Yakir Vizel, Vijay Ganesh, Arie Gurfinkel
2019	B	`conf`	Lazy but Effective Functional Synthesis. VMCAI Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta
2019	—	`conf`	Local Reasoning for Parameterized First Order Protocols. NFM Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler
2019	J	`jnl`	Local Reasoning for Parameterized First Order Protocols. CoRR Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler
2019	—	`conf`	Property Directed Self Composition. CAV (1) Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2019	J	`jnl`	Property Directed Self Composition. CoRR Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2019	A*	`conf`	Simple and precise static analysis of untrusted Linux kernel extensions. PLDI Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, Mooly Sagiv
2019	Misc	`conf`	The Science, Art, and Magic of Constrained Horn Clauses. SYNASC Arie Gurfinkel, Nikolaj S. Bjørner
2019	B	`conf`	Unification-based Pointer Analysis without Oversharing. FMCAD Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
2019	J	`jnl`	Unification-based Pointer Analysis without Oversharing. CoRR Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
2018	B	`ed.`	2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018 FMCAD Nikolaj S. Bjørner, Arie Gurfinkel
2018	—	`ch.`	BDD-Based Symbolic Model Checking. Handbook of Model Checking Sagar Chaki, Arie Gurfinkel
2018	—	`conf`	Executable Counterexamples in Software Model Checking. VSTTE Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz
2018	B	`conf`	Predictive Run-Time Verification of Discrete-Time Reachability Properties in Black-Box Systems Using Trace-Level Abstraction and Statistical Learning. RV Reza Babaee, Arie Gurfinkel, Sebastian Fischmeister
2018	B	`conf`	Quantifiers on Demand. ATVA Arie Gurfinkel, Sharon Shoham, Yakir Vizel
2018	—	`conf`	Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
2017	B	`conf`	A Context-Sensitive Memory Model for Verification of C/C++ Programs. SAS Arie Gurfinkel, Jorge A. Navas
2017	B	`conf`	Automated analysis of Stateflow models. LPAR Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux
2017	B	`conf`	Designing parallel PDR. FMCAD Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, Natasha Sharygina
2017	B	`conf`	IC3 - Flipping the E in ICE. VMCAI Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik
2017	B	`conf`	K-induction without unrolling. FMCAD Arie Gurfinkel, Alexander Ivrii
2017	J	`jnl`	Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. CoRR Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel, Michael W. Whalen
2016	B	`conf`	CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. SEFM Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli
2016	A*	`conf`	Maximal specification synthesis. POPL Aws Albarghouthi, Isil Dillig, Arie Gurfinkel
2016	—	`conf`	Property Directed Equivalence via Abstract Simulation. CAV (2) Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
2016	J	`jnl`	SMT-based model checking for recursive programs. Formal Methods Syst. Des. Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
2016	—	`conf`	SMT-based verification of parameterized systems. SIGSOFT FSE Arie Gurfinkel, Sharon Shoham, Yuri Meshman
2016	J	`jnl`	Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR Andreas Katis, Grigory Fedyukovich, Andrew Gacek, John D. Backes, Arie Gurfinkel, Michael W. Whalen
2016	A	`conf`	Synthesizing Ranking Functions from Bits and Pieces. TACAS Caterina Urban, Arie Gurfinkel, Temesghen Kahsai
2016	—	`ed.`	Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers VSTTE Arie Gurfinkel, Sanjit A. Seshia
2015	Misc	`conf`	Algorithmic Logic-Based Verification with SeaHorn. SYNASC Arie Gurfinkel
2015	J	`jnl`	Algorithmic logic-based verification. ACM SIGLOG News Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas
2015	B	`conf`	Automated Discovery of Simulation Between Programs. LPAR Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
2015	B	`conf`	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan
2015	J	`jnl`	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan
2015	—	`conf`	Fast Interpolating BMC. CAV (1) Yakir Vizel, Arie Gurfinkel, Sharad Malik
2015	—	`conf`	Horn Clause Solvers for Program Verification. Fields of Logic and Computation II Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko
2015	B	`conf`	Property Directed Polyhedral Abstraction. VMCAI Nikolaj S. Bjørner, Arie Gurfinkel
2015	B	`conf`	Pushing to the Top. FMCAD Arie Gurfinkel, Alexander Ivrii
2015	J	`jnl`	Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). Formal Methods Syst. Des. Sagar Chaki, Arie Gurfinkel, Ofer Strichman
2015	A	`conf`	SeaHorn: A Framework for Verifying C Programs (Competition Contribution). TACAS Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas
2015	—	`conf`	The SeaHorn Verification Framework. CAV (1) Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas
2014	B	`conf`	DRUPing for interpolates. FMCAD Arie Gurfinkel, Yakir Vizel
2014	B	`conf`	Efficient verification of periodic programs using sequential consistency and snapshots. FMCAD Sagar Chaki, Arie Gurfinkel, Nishant Sinha
2014	A	`conf`	FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). TACAS Arie Gurfinkel, Anton Belov
2014	—	`conf`	Incremental Verification of Compiler Optimizations. NASA Formal Methods Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina
2014	A*	`conf`	Interpolating Property Directed Reachability. CAV Yakir Vizel, Arie Gurfinkel
2014	—	`conf`	Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis. PPREW@POPL Wesley Jin, Cory F. Cohen, Jeffrey Gennari, Charles Hines, Sagar Chaki, Arie Gurfinkel, Jeffrey Havrilla, Priya Narasimhan
2014	A*	`conf`	SMT-Based Model Checking for Recursive Programs. CAV Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
2014	J	`jnl`	SMT-based Model Checking for Recursive Programs. CoRR Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki
2014	B	`conf`	Small inductive safe invariants. FMCAD Alexander Ivrii, Arie Gurfinkel, Anton Belov
2014	A*	`conf`	Symbolic optimization with SMT solvers. POPL Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik
2014	—	`conf`	Synthesizing Modular Invariants for Synchronous Code. HCVS Pierre-Loïc Garoche, Arie Gurfinkel, Temesghen Kahsai
2014	A	`conf`	Synthesizing Safe Bit-Precise Invariants. TACAS Arie Gurfinkel, Anton Belov, João Marques-Silva
2013	A*	`conf`	Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CAV Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
2013	J	`jnl`	Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CoRR Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke
2013	J	`jnl`	Beyond vacuity: towards the strongest passing formula. Formal Methods Syst. Des. Hana Chockler, Arie Gurfinkel, Ofer Strichman
2013	B	`conf`	Compositional Sequentialization of Periodic Programs. VMCAI Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman
2013	C	`conf`	Finding Errors in Python Programs Using Dynamic Symbolic Execution. ICTSS Samir Sapra, Marius Minea, Sagar Chaki, Arie Gurfinkel, Edmund M. Clarke
2013	—	`conf`	Instantiations, Zippers and EPR Interpolation. LPAR (short papers) Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
2013	B	`conf`	Interpolation Properties and SAT-Based Model Checking. ATVA Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
2013	A	`conf`	UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). TACAS Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik
2013	B	`conf`	Verifying periodic programs with priority inheritance locks. FMCAD Sagar Chaki, Arie Gurfinkel, Ofer Strichman
2012	—	`conf`	Binary Function Clustering Using Semantic Hashes. ICMLA (1) Wesley Jin, Sagar Chaki, Cory F. Cohen, Arie Gurfinkel, Jeffrey Havrilla, Charles Hines, Priya Narasimhan
2012	B	`conf`	Craig Interpretation. SAS Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik
2012	A	`conf`	From Under-Approximations to Over-Approximations and Back. TACAS Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik
2012	J	`jnl`	Propositional Interpolation Systems for Model Checking CoRR Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina
2012	J	`jnl`	Reachability Problems in Piecewise FIFO Systems. ACM Trans. Comput. Log. Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler
2012	B	`conf`	Regression Verification for Multi-threaded Programs. VMCAI Sagar Chaki, Arie Gurfinkel, Ofer Strichman
2012	J	`jnl`	Robust Vacuity for Branching Temporal Logic. ACM Trans. Comput. Log. Arie Gurfinkel, Marsha Chechik
2012	A*	`conf`	Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. CAV Aws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik
2012	B	`conf`	Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. VMCAI Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik
2011	J	`jnl`	Automated assume-guarantee reasoning for omega-regular systems and specifications. Innov. Syst. Softw. Eng. Sagar Chaki, Arie Gurfinkel
2011	—	`conf`	CSSL: a logic for specifying conditional scenarios. SIGSOFT FSE Shoham Ben-David, Marsha Chechik, Arie Gurfinkel, Sebastián Uchitel
2011	—	`conf`	Efficient Predicate Abstraction of Program Summaries. NASA Formal Methods Arie Gurfinkel, Sagar Chaki, Samir Sapra
2011	J	`jnl`	On the consistency, expressiveness, and precision of partial modeling formalisms. Inf. Comput. Ou Wei, Arie Gurfinkel, Marsha Chechik
2011	A*	`conf`	Supervised learning for provenance-similarity of binaries. KDD Sagar Chaki, Cory F. Cohen, Arie Gurfinkel
2011	B	`conf`	Time-bounded analysis of real-time systems. FMCAD Sagar Chaki, Arie Gurfinkel, Ofer Strichman
2010	A*	`conf`	Abstract Analysis of Symbolic Executions. CAV Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik
2010	—	`conf`	Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications. NASA Formal Methods Sagar Chaki, Arie Gurfinkel
2010	B	`conf`	Boxes: A Symbolic Abstract Domain of Boxes. SAS Arie Gurfinkel, Sagar Chaki
2010	J	`jnl`	Combining predicate and numeric abstraction for software model checking. Int. J. Softw. Tools Technol. Transf. Arie Gurfinkel, Sagar Chaki
2010	J	`jnl`	Exploiting resolution proofs to speed up LTL vacuity detection for BMC. Int. J. Softw. Tools Technol. Transf. Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik
2010	J	`jnl`	Robust Vacuity for Branching Temporal Logic CoRR Arie Gurfinkel, Marsha Chechik
2010	—	`conf`	Using Architecturally Significant Requirements for Guiding System Evolution. CSMR Ipek Ozkaya, J. Andrés Díaz Pace, Arie Gurfinkel, Sagar Chaki
2010	—	`conf`	Variants of LTL Query Checking. Haifa Verification Conference Hana Chockler, Arie Gurfinkel, Ofer Strichman
2009	B	`conf`	Decision diagrams for linear arithmetic. FMCAD Sagar Chaki, Arie Gurfinkel, Ofer Strichman
2009	B	`conf`	Mixed Transition Systems Revisited. VMCAI Ou Wei, Arie Gurfinkel, Marsha Chechik
2009	—	`conf`	Towards engineered architecture evolution. MiSE@ICSE Sagar Chaki, J. Andrés Díaz Pace, David Garlan, Arie Gurfinkel, Ipek Ozkaya
2009	—	`conf`	Verification of Parameterized Systems with Combinations of Abstract Domains. FMOODS/FORTE Naghmeh Ghafari, Arie Gurfinkel, Richard J. Trefler
2008	A*	`conf`	Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates. ASE Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie
2008	B	`conf`	Beyond Vacuity: Towards the Strongest Passing Formula. FMCAD Hana Chockler, Arie Gurfinkel, Ofer Strichman
2008	B	`conf`	Combining Predicate and Numeric Abstraction for Software Model Checking. FMCAD Arie Gurfinkel, Sagar Chaki
2008	B	`conf`	Model Checking Recursive Programs with Exact Predicate Abstraction. ATVA Arie Gurfinkel, Ou Wei, Marsha Chechik
2008	A*	`conf`	PtYasm: Software Model Checking with Proof Templates. ASE Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie
2007	J	`jnl`	A framework for counterexample generation and exploration. Int. J. Softw. Tools Technol. Transf. Marsha Chechik, Arie Gurfinkel
2007	B	`conf`	Algorithmic Analysis of Piecewise FIFO Systems. FMCAD Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler
2007	B	`conf`	Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. FMCAD Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik
2007	B	`conf`	Finding Environment Guarantees. FASE Marsha Chechik, Mihaela Gheorghiu, Arie Gurfinkel
2007	B	`conf`	Finding State Solutions to Temporal Logic Queries. IFM Mihaela Gheorghiu, Arie Gurfinkel, Marsha Chechik
2007	—	`—`	Model-checking with many values. Arie Gurfinkel
2006	J	`jnl`	Data structures for symbolic multi-valued model-checking. Formal Methods Syst. Des. Marsha Chechik, Arie Gurfinkel, Benet Devereux, Albert Y. C. Lai, Steve M. Easterbrook
2006	B	`conf`	Systematic Construction of Abstractions for Model-Checking. VMCAI Arie Gurfinkel, Ou Wei, Marsha Chechik
2006	A	`conf`	Why Waste a Perfectly Good Abstraction?. TACAS Arie Gurfinkel, Marsha Chechik
2006	A*	`conf`	Yasm: A Software Model-Checker for Verification and Refutation. CAV Arie Gurfinkel, Ou Wei, Marsha Chechik
2005	B	`conf`	A Framework for Counterexample Generation and Exploration. FASE Marsha Chechik, Arie Gurfinkel
2005	—	`conf`	How Thorough Is Thorough Enough? CHARME Arie Gurfinkel, Marsha Chechik
2005	—	`conf`	Identification and Counter Abstraction for Full Virtual Symmetry. CHARME Ou Wei, Arie Gurfinkel, Marsha Chechik
2005	—	`conf`	Model-Checking Software Using Precise Abstractions. VSTTE Marsha Chechik, Arie Gurfinkel
2005	B	`conf`	Stuttering Abstraction for Model Checkin. SEFM Shiva Nejati, Arie Gurfinkel, Marsha Chechik
2004	—	`conf`	A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill
2004	B	`conf`	Extending Extended Vacuity. FMCAD Arie Gurfinkel, Marsha Chechik
2004	A	`conf`	How Vacuous Is Vacuous? TACAS Arie Gurfinkel, Marsha Chechik
2003	—	`conf`	Generating Counterexamples for Multi-valued Model-Checking. FME Arie Gurfinkel, Marsha Chechik
2003	B	`conf`	Multi-Valued Model Checking via Classical Model Checking. CONCUR Arie Gurfinkel, Marsha Chechik
2003	J	`jnl`	Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. Marsha Chechik, Benet Devereux, Steve M. Easterbrook, Arie Gurfinkel
2003	A	`conf`	Proof-Like Counter-Examples. TACAS Arie Gurfinkel, Marsha Chechik
2003	A*	`conf`	TLQSolver: A Temporal Logic Query Checker. CAV Marsha Chechik, Arie Gurfinkel
2003	J	`jnl`	Temporal Logic Query Checking: A Tool for Model Exploration. IEEE Trans. Software Eng. Arie Gurfinkel, Marsha Chechik, Benet Devereux
2003	A*	`conf`	\chiChek: A Model Checker for Multi-Valued Reasoning. ICSE Steve M. Easterbrook, Marsha Chechik, Benet Devereux, Arie Gurfinkel, Albert Y. C. Lai, Victor Petrovykh, Anya Tafliovich, Christopher D. Thompson-Walsh
2002	—	`conf`	Model exploration with temporal logic query checking. SIGSOFT FSE Arie Gurfinkel, Benet Devereux, Marsha Chechik
2002	A*	`conf`	chi-Chek: A Multi-valued Model-Checker. CAV Marsha Chechik, Arie Gurfinkel, Benet Devereux
2001	—	`conf`	Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN. SPIN Marsha Chechik, Benet Devereux, Arie Gurfinkel