default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDArie Gurfinkel
Person information
- affiliation: University of Waterloo, Waterloo, ON, Canada
- affiliation (former): Carnegie Mellon University, Pittsburgh, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2025
[c120]Yusen Su, Jorge A. Navas
, Arie Gurfinkel, Isabel Garcia-Contreras:
Automatic Inference of Relational Object Invariants. VMCAI (1) 2025: 214-236- [e8]Arie Gurfinkel, Marijn Heule:
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. Lecture Notes in Computer Science 15696, Springer 2025, ISBN 978-3-031-90642-8 [contents] - [e7]Arie Gurfinkel, Marijn Heule:
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. Lecture Notes in Computer Science 15697, Springer 2025, ISBN 978-3-031-90652-7 [contents] - [e6]Arie Gurfinkel, Marijn Heule:
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. Lecture Notes in Computer Science 15698, Springer 2025, ISBN 978-3-031-90659-6 [contents] - 2024
- [j18]Hari Govind Vediramana Krishnan, YuTing Chen, Sharon Shoham, Arie Gurfinkel:
Global guidance for local generalization in model checking. Formal Methods Syst. Des. 63(1): 81-109 (2024) - [c119]Nham Le, Arie Gurfinkel, Xujie Si, Chuqin Geng:
Towards Robust Saliency Maps. ACML 2024: 351-366 - [c118]Arie Gurfinkel:
Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). CONCUR 2024: 1:1-1:1 - [c117]Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel:
Inductive Predicate Synthesis Modulo Programs. ECOOP 2024: 43:1-43:30 - [c116]Siddharth Priya, Arie Gurfinkel:
Ownership in Low-Level Intermediate Representation. FMCAD 2024: 292-300 - [c115]Joseph Tafese, Arie Gurfinkel:
Efficient Simulation for Hardware Model Checking. LPAR 2024: 136-146 - [c114]Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel:
Unlocking the Power of Environment Assumptions for Unit Proofs. SEFM 2024: 366-384 - [c113]Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel:
Speculative SAT Modulo SAT. TACAS (1) 2024: 43-60 - [e5]Arie Gurfinkel, Vijay Ganesh:
Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science 14681, Springer 2024, ISBN 978-3-031-65626-2 [contents] - [e4]Arie Gurfinkel, Vijay Ganesh:
Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part II. Lecture Notes in Computer Science 14682, Springer 2024, ISBN 978-3-031-65629-3 [contents] - [e3]Arie Gurfinkel, Vijay Ganesh:
Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. Lecture Notes in Computer Science 14683, Springer 2024, ISBN 978-3-031-65632-3 [contents] - [i25]Scott Wesley, Maria Christakis, Jorge A. Navas, Richard J. Trefler, Valentin Wüstholz, Arie Gurfinkel:
Inductive Predicate Synthesis Modulo Programs (Extended). CoRR abs/2407.08455 (2024) - [i24]Siddharth Priya, Arie Gurfinkel:
Ownership in low-level intermediate representation. CoRR abs/2408.04043 (2024) - [i23]Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel:
Unlocking the Power of Environment Assumptions for Unit Proofs. CoRR abs/2409.12269 (2024) - [i22]Yusen Su, Jorge A. Navas, Arie Gurfinkel, Isabel Garcia-Contreras:
Automatic Inference of Relational Object Invariants. CoRR abs/2411.14735 (2024) - 2023
- [c112]Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Fast Approximations of Quantifier Elimination. CAV (2) 2023: 64-86 - [c111]Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel:
BTOR2MLIR: A Format and Toolchain for Hardware Verification. FMCAD 2023: 55-63 - [c110]Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si:
Towards Reliable Neural Specifications. ICML 2023: 11196-11212 - [i21]Isabel Garcia-Contreras, Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Fast Approximations of Quantifier Elimination. CoRR abs/2306.10009 (2023) - [i20]Hari Govind V. K., Isabel Garcia-Contreras, Sharon Shoham, Arie Gurfinkel:
Speculative SAT Modulo SAT. CoRR abs/2306.17765 (2023) - [i19]Joseph Tafese, Isabel Garcia-Contreras, Arie Gurfinkel:
Btor2MLIR: A Format and Toolchain for Hardware Verification. CoRR abs/2309.09100 (2023) - [i18]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): 66-95 (2023) - 2022
- [j17]Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel:
Verifying verified code. Innov. Syst. Softw. Eng. 18(3): 335-346 (2022) - [j16]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): 1-29 (2022) - [c109]Arie Gurfinkel:
Program Verification with Constrained Horn Clauses (Invited Paper). CAV (1) 2022: 19-29 - [c108]Siddharth Priya, Yusen Su, Yuyan Bao, Xiang Zhou, Yakir Vizel, Arie Gurfinkel:
Bounded Model Checking for LLVM. FMCAD 2022: 214-224 - [c107]Isabel Garcia-Contreras, Arie Gurfinkel, Jorge A. Navas:
Efficient Modular SMT-Based Model Checking of Pointer Programs. SAS 2022: 227-246 - [c106]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: 425-449 - [i17]Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, Xujie Si:
Toward Reliable Neural Specifications. CoRR abs/2210.16114 (2022) - 2021
- [j15]Nikolaj S. 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): 119-120 (2021) - [c105]Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel:
Verifying Verified Code. ATVA 2021: 187-202 - [c104]Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, Yakir Vizel:
IC3 with Internal Signals. FMCAD 2021: 63-71 - [c103]Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Logical Characterization of Coherent Uninterpreted Programs. FMCAD 2021: 77-85 - [c102]Nham Le, Xujie Si, Arie Gurfinkel:
Data-driven Optimization of Inductive Generalization. FMCAD 2021: 86-95 - [c101]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: 429-452 - [c100]Arie Gurfinkel, Jorge A. Navas:
Abstract Interpretation of LLVM with a Region-Based Memory Model. VSTTE 2021: 122-144 - [i16]Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Quantifiers on Demand. CoRR abs/2106.00664 (2021) - [i15]Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao, Arie Gurfinkel:
Verifying Verified Code. CoRR abs/2107.00723 (2021) - [i14]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 abs/2107.08583 (2021) - [i13]Hari Govind V. K., Sharon Shoham, Arie Gurfinkel:
Logical Characterization of Coherent Uninterpreted Programs. CoRR abs/2107.12902 (2021) - 2020
- [c99]Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, Arie Gurfinkel:
Global Guidance for Local Generalization in Model Checking. CAV (2) 2020: 101-125 - [c98]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: 1690-1697 - [c97]Hari Govind V. K., Grigory Fedyukovich, Arie Gurfinkel:
Word Level Property Directed Reachability. ICCAD 2020: 107:1-107:9 - [i12]Hari Govind V. K., Yuting Chen, Sharon Shoham, Arie Gurfinkel:
Global Guidance for Local Generalization in Model Checking. CoRR abs/2005.13301 (2020)
2010 – 2019
- 2019
- [c96]Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Property Directed Self Composition. CAV (1) 2019: 161-179 - [c95]Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel:
Interpolating Strong Induction. CAV (2) 2019: 367-385 - [c94]Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel:
Unification-based Pointer Analysis without Oversharing. FMCAD 2019: 37-45 - [c93]Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler:
Local Reasoning for Parameterized First Order Protocols. NFM 2019: 36-53 - [c92]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: 1069-1084 - [c91]Arie Gurfinkel, Nikolaj S. Bjørner:
The Science, Art, and Magic of Constrained Horn Clauses. SYNASC 2019: 6-10 - [c90]Grigory Fedyukovich, Arie Gurfinkel, Aarti Gupta:
Lazy but Effective Functional Synthesis. VMCAI 2019: 92-113 - [i11]Rylo Ashmore, Arie Gurfinkel, Richard J. Trefler:
Local Reasoning for Parameterized First Order Protocols. CoRR abs/1903.03218 (2019) - [i10]Ron Shemer, Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Property Directed Self Composition. CoRR abs/1905.07705 (2019) - [i9]Hari Govind V. K., Yakir Vizel, Vijay Ganesh, Arie Gurfinkel:
Interpolating Strong Induction. CoRR abs/1906.01583 (2019) - [i8]Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel:
Unification-based Pointer Analysis without Oversharing. CoRR abs/1906.01706 (2019) - 2018
- [c89]Arie Gurfinkel, Sharon Shoham, Yakir Vizel:
Quantifiers on Demand. ATVA 2018: 248-266 - [c88]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: 187-204 - [c87]Reza Babaee, Arie Gurfinkel, Sebastian Fischmeister:
Prevent : A Predictive Run-Time Verification Framework Using Statistical Learning. SEFM 2018: 205-220 - [c86]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: 176-193 - [c85]Jeffrey Gennari, Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas, Edward J. Schwartz:
Executable Counterexamples in Software Model Checking. VSTTE 2018: 17-37 - [p1]Sagar Chaki, Arie Gurfinkel:
BDD-Based Symbolic Model Checking. Handbook of Model Checking 2018: 219-245 - [e2]Nikolaj S. Bjørner, Arie Gurfinkel:
2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018. IEEE 2018, ISBN 978-0-9835678-8-2 [contents] - 2017
- [c84]Arie Gurfinkel, Alexander Ivrii:
K-induction without unrolling. FMCAD 2017: 148-155 - [c83]Matteo Marescotti, Arie Gurfinkel, Antti Eero Johannes Hyvärinen, Natasha Sharygina:
Designing parallel PDR. FMCAD 2017: 156-163 - [c82]Hamza Bourbouh, Pierre-Loïc Garoche, Christophe Garion, Arie Gurfinkel, Temesghen Kahsai, Xavier Thirioux:
Automated analysis of Stateflow models. LPAR 2017: 144-161 - [c81]Arie Gurfinkel, Jorge A. Navas:
A Context-Sensitive Memory Model for Verification of C/C++ Programs. SAS 2017: 148-168 - [c80]Yakir Vizel, Arie Gurfinkel, Sharon Shoham, Sharad Malik:
IC3 - Flipping the E in ICE. VMCAI 2017: 521-538 - [i7]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 abs/1709.04986 (2017) - 2016
- [j14]Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3): 175-205 (2016) - [c79]Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina:
Property Directed Equivalence via Abstract Simulation. CAV (2) 2016: 433-453 - [c78]Aws Albarghouthi, Isil Dillig, Arie Gurfinkel:
Maximal specification synthesis. POPL 2016: 789-801 - [c77]Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli:
CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. SEFM 2016: 347-366 - [c76]Arie Gurfinkel, Sharon Shoham, Yuri Meshman:
SMT-based verification of parameterized systems. SIGSOFT FSE 2016: 338-348 - [c75]Caterina Urban, Arie Gurfinkel, Temesghen Kahsai:
Synthesizing Ranking Functions from Bits and Pieces. TACAS 2016: 54-70 - [e1]Arie Gurfinkel, Sanjit A. Seshia:
Verified Software: Theories, Tools, and Experiments - 7th International Conference, VSTTE 2015, San Francisco, CA, USA, July 18-19, 2015. Revised Selected Papers. Lecture Notes in Computer Science 9593, Springer 2016, ISBN 978-3-319-29612-8 [contents] - [i6]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 abs/1610.05867 (2016) - 2015
- [j13]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): 287-301 (2015) - [j12]Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas:
Algorithmic logic-based verification. ACM SIGLOG News 2(2): 29-38 (2015) - [c74]Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan, Andrey Rybalchenko:
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II 2015: 24-51 - [c73]Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, Jorge A. Navas:
The SeaHorn Verification Framework. CAV (1) 2015: 343-361 - [c72]Yakir Vizel, Arie Gurfinkel, Sharad Malik:
Fast Interpolating BMC. CAV (1) 2015: 641-657 - [c71]Arie Gurfinkel, Alexander Ivrii:
Pushing to the Top. FMCAD 2015: 65-72 - [c70]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96 - [c69]Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina:
Automated Discovery of Simulation Between Programs. LPAR 2015: 606-621 - [c68]Arie Gurfinkel:
Algorithmic Logic-Based Verification with SeaHorn. SYNASC 2015: 12-15 - [c67]Arie Gurfinkel, Temesghen Kahsai, Jorge A. Navas:
SeaHorn: A Framework for Verifying C Programs (Competition Contribution). TACAS 2015: 447-450 - [c66]Nikolaj S. Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281 - [i5]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. CoRR abs/1508.01288 (2015) - 2014
- [c65]Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-Based Model Checking for Recursive Programs. CAV 2014: 17-34 - [c64]Yakir Vizel, Arie Gurfinkel:
Interpolating Property Directed Reachability. CAV 2014: 260-276 - [c63]Sagar Chaki, Arie Gurfinkel, Nishant Sinha:
Efficient verification of periodic programs using sequential consistency and snapshots. FMCAD 2014: 51-58 - [c62]Arie Gurfinkel, Yakir Vizel:
DRUPing for interpolates. FMCAD 2014: 99-106 - [c61]Alexander Ivrii, Arie Gurfinkel, Anton Belov:
Small inductive safe invariants. FMCAD 2014: 115-122 - [c60]Grigory Fedyukovich, Arie Gurfinkel, Natasha Sharygina:
Incremental Verification of Compiler Optimizations. NASA Formal Methods 2014: 300-306 - [c59]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: 1:1-1:11 - [c58]Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik:
Symbolic optimization with SMT solvers. POPL 2014: 607-618 - [c57]Arie Gurfinkel, Anton Belov, João Marques-Silva:
Synthesizing Safe Bit-Precise Invariants. TACAS 2014: 93-108 - [c56]Arie Gurfinkel, Anton Belov:
FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). TACAS 2014: 408-411 - [c55]Pierre-Loïc Garoche, Arie Gurfinkel, Temesghen Kahsai:
Synthesizing Modular Invariants for Synchronous Code. HCVS 2014: 19-30 - [i4]Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-based Model Checking for Recursive Programs. CoRR abs/1405.4028 (2014) - 2013
- [j11]Hana Chockler, Arie Gurfinkel, Ofer Strichman:
Beyond vacuity: towards the strongest passing formula. Formal Methods Syst. Des. 43(3): 552-571 (2013) - [c54]Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina:
Interpolation Properties and SAT-Based Model Checking. ATVA 2013: 255-271 - [c53]Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke:
Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CAV 2013: 846-862 - [c52]Sagar Chaki, Arie Gurfinkel, Ofer Strichman:
Verifying periodic programs with priority inheritance locks. FMCAD 2013: 137-144 - [c51]Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav:
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) 2013: 35-41 - [c50]Samir Sapra, Marius Minea, Sagar Chaki, Arie Gurfinkel, Edmund M. Clarke:
Finding Errors in Python Programs Using Dynamic Symbolic Execution. ICTSS 2013: 283-289 - [c49]Aws Albarghouthi, Arie Gurfinkel, Yi Li, Sagar Chaki, Marsha Chechik:
UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). TACAS 2013: 637-640 - [c48]Sagar Chaki, Arie Gurfinkel, Soonho Kong, Ofer Strichman:
Compositional Sequentialization of Periodic Programs. VMCAI 2013: 536-554 - [i3]Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke:
Automatic Abstraction in SMT-Based Unbounded Software Model Checking. CoRR abs/1306.1945 (2013) - 2012
- [j10]Arie Gurfinkel, Marsha Chechik:
Robust Vacuity for Branching Temporal Logic. ACM Trans. Comput. Log. 13(1): 1:1-1:32 (2012) - [j9]Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler:
Reachability Problems in Piecewise FIFO Systems. ACM Trans. Comput. Log. 13(1): 7:1-7:33 (2012) - [c47]Aws Albarghouthi, Yi Li, Arie Gurfinkel, Marsha Chechik:
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. CAV 2012: 672-678 - [c46]Wesley Jin, Sagar Chaki, Cory F. Cohen, Arie Gurfinkel, Jeffrey Havrilla, Charles Hines, Priya Narasimhan:
Binary Function Clustering Using Semantic Hashes. ICMLA (1) 2012: 386-391 - [c45]Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik:
Craig Interpretation. SAS 2012: 300-316 - [c44]Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik:
From Under-Approximations to Over-Approximations and Back. TACAS 2012: 157-172 - [c43]Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik:
Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. VMCAI 2012: 39-55 - [c42]Sagar Chaki, Arie Gurfinkel, Ofer Strichman:
Regression Verification for Multi-threaded Programs. VMCAI 2012: 119-135 - [i2]Arie Gurfinkel, Simone Fulvio Rollini, Natasha Sharygina:
Propositional Interpolation Systems for Model Checking. CoRR abs/1212.4650 (2012) - 2011
- [j8]Ou Wei, Arie Gurfinkel, Marsha Chechik:
On the consistency, expressiveness, and precision of partial modeling formalisms. Inf. Comput. 209(1): 20-47 (2011) - [j7]Sagar Chaki, Arie Gurfinkel:
Automated assume-guarantee reasoning for omega-regular systems and specifications. Innov. Syst. Softw. Eng. 7(2): 131-139 (2011) - [c41]Sagar Chaki, Arie Gurfinkel, Ofer Strichman:
Time-bounded analysis of real-time systems. FMCAD 2011: 72-80 - [c40]Sagar Chaki, Cory F. Cohen, Arie Gurfinkel:
Supervised learning for provenance-similarity of binaries. KDD 2011: 15-23 - [c39]Arie Gurfinkel, Sagar Chaki, Samir Sapra:
Efficient Predicate Abstraction of Program Summaries. NASA Formal Methods 2011: 131-145 - [c38]Shoham Ben-David, Marsha Chechik, Arie Gurfinkel, Sebastián Uchitel:
CSSL: a logic for specifying conditional scenarios. SIGSOFT FSE 2011: 37-47 - 2010
- [j6]Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik:
Exploiting resolution proofs to speed up LTL vacuity detection for BMC. Int. J. Softw. Tools Technol. Transf. 12(5): 319-335 (2010) - [j5]Arie Gurfinkel, Sagar Chaki:
Combining predicate and numeric abstraction for software model checking. Int. J. Softw. Tools Technol. Transf. 12(6): 409-427 (2010) - [c37]Aws Albarghouthi, Arie Gurfinkel, Ou Wei, Marsha Chechik:
Abstract Analysis of Symbolic Executions. CAV 2010: 495-510 - [c36]Ipek Ozkaya, J. Andrés Díaz Pace, Arie Gurfinkel, Sagar Chaki:
Using Architecturally Significant Requirements for Guiding System Evolution. CSMR 2010: 127-136 - [c35]Hana Chockler, Arie Gurfinkel, Ofer Strichman:
Variants of LTL Query Checking. Haifa Verification Conference 2010: 76-92 - [c34]Sagar Chaki, Arie Gurfinkel:
Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications. NASA Formal Methods 2010: 57-66 - [c33]Arie Gurfinkel, Sagar Chaki:
Boxes: A Symbolic Abstract Domain of Boxes. SAS 2010: 287-303 - [i1]Arie Gurfinkel, Marsha Chechik:
Robust Vacuity for Branching Temporal Logic. CoRR abs/1002.4616 (2010)
2000 – 2009
- 2009
- [c32]Sagar Chaki, Arie Gurfinkel, Ofer Strichman:
Decision diagrams for linear arithmetic. FMCAD 2009: 53-60 - [c31]Naghmeh Ghafari, Arie Gurfinkel, Richard J. Trefler:
Verification of Parameterized Systems with Combinations of Abstract Domains. FMOODS/FORTE 2009: 57-72 - [c30]Sagar Chaki, J. Andrés Díaz Pace, David Garlan, Arie Gurfinkel, Ipek Ozkaya:
Towards engineered architecture evolution. MiSE@ICSE 2009: 1-6 - [c29]Ou Wei, Arie Gurfinkel, Marsha Chechik:
Mixed Transition Systems Revisited. VMCAI 2009: 349-365 - 2008
- [c28]Arie Gurfinkel, Ou Wei, Marsha Chechik:
Model Checking Recursive Programs with Exact Predicate Abstraction. ATVA 2008: 95-110 - [c27]Hana Chockler, Arie Gurfinkel, Ofer Strichman:
Beyond Vacuity: Towards the Strongest Passing Formula. FMCAD 2008: 1-8 - [c26]Arie Gurfinkel, Sagar Chaki:
Combining Predicate and Numeric Abstraction for Software Model Checking. FMCAD 2008: 1-9 - [c25]Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie:
Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates. ASE 2008: 387-390 - [c24]Thomas E. Hart, Kelvin Ku, Arie Gurfinkel, Marsha Chechik, David Lie:
PtYasm: Software Model Checking with Proof Templates. ASE 2008: 479-480 - 2007
- [b1]Arie Gurfinkel:
Model-checking with many values. University of Toronto, Canada, 2007 - [j4]Marsha Chechik, Arie Gurfinkel:
A framework for counterexample generation and exploration. Int. J. Softw. Tools Technol. Transf. 9(5-6): 429-445 (2007) - [c23]Marsha Chechik, Mihaela Gheorghiu, Arie Gurfinkel:
Finding Environment Guarantees. FASE 2007: 352-367 - [c22]Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, Marsha Chechik:
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. FMCAD 2007: 3-12 - [c21]Naghmeh Ghafari, Arie Gurfinkel, Nils Klarlund, Richard J. Trefler:
Algorithmic Analysis of Piecewise FIFO Systems. FMCAD 2007: 45-52 - [c20]Mihaela Gheorghiu, Arie Gurfinkel, Marsha Chechik:
Finding State Solutions to Temporal Logic Queries. IFM 2007: 273-292 - 2006
- [j3]Marsha Chechik, Arie Gurfinkel, Benet Devereux, Albert Y. C. Lai, Steve M. Easterbrook:
Data structures for symbolic multi-valued model-checking. Formal Methods Syst. Des. 29(3): 295-344 (2006) - [c19]Arie Gurfinkel, Ou Wei, Marsha Chechik:
Yasm: A Software Model-Checker for Verification and Refutation. CAV 2006: 170-174 - [c18]Arie Gurfinkel, Marsha Chechik:
Why Waste a Perfectly Good Abstraction?. TACAS 2006: 212-226 - [c17]Arie Gurfinkel, Ou Wei, Marsha Chechik:
Systematic Construction of Abstractions for Model-Checking. VMCAI 2006: 381-397 - 2005
- [c16]Arie Gurfinkel, Marsha Chechik:
How Thorough Is Thorough Enough? CHARME 2005: 65-80 - [c15]Ou Wei, Arie Gurfinkel, Marsha Chechik:
Identification and Counter Abstraction for Full Virtual Symmetry. CHARME 2005: 285-300 - [c14]Marsha Chechik, Arie Gurfinkel:
A Framework for Counterexample Generation and Exploration. FASE 2005: 220-236 - [c13]Shiva Nejati, Arie Gurfinkel, Marsha Chechik:
Stuttering Abstraction for Model Checkin. SEFM 2005: 311-320 - [c12]Marsha Chechik, Arie Gurfinkel:
Model-Checking Software Using Precise Abstractions. VSTTE 2005: 347-353 - 2004
- [c11]Arie Gurfinkel, Marsha Chechik:
Extending Extended Vacuity. FMCAD 2004: 306-321 - [c10]Arie Gurfinkel, Marsha Chechik:
How Vacuous Is Vacuous? TACAS 2004: 451-466 - [c9]Sergey Berezin, Clark W. Barrett, Igor Shikanian, Marsha Chechik, Arie Gurfinkel, David L. Dill:
A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR 2004: 13-23 - 2003
- [j2]Marsha Chechik, Benet Devereux, Steve M. Easterbrook, Arie Gurfinkel:
Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4): 371-408 (2003) - [j1]Arie Gurfinkel, Marsha Chechik, Benet Devereux:
Temporal Logic Query Checking: A Tool for Model Exploration. IEEE Trans. Software Eng. 29(10): 898-914 (2003) - [c8]Marsha Chechik, Arie Gurfinkel:
TLQSolver: A Temporal Logic Query Checker. CAV 2003: 210-214 - [c7]Arie Gurfinkel, Marsha Chechik:
Multi-Valued Model Checking via Classical Model Checking. CONCUR 2003: 263-277 - [c6]Arie Gurfinkel, Marsha Chechik:
Generating Counterexamples for Multi-valued Model-Checking. FME 2003: 503-521 - [c5]Steve M. Easterbrook, Marsha Chechik, Benet Devereux, Arie Gurfinkel, Albert Y. C. Lai, Victor Petrovykh, Anya Tafliovich, Christopher D. Thompson-Walsh:
\chiChek: A Model Checker for Multi-Valued Reasoning. ICSE 2003: 804-805 - [c4]Arie Gurfinkel, Marsha Chechik:
Proof-Like Counter-Examples. TACAS 2003: 160-175 - 2002
- [c3]Marsha Chechik, Arie Gurfinkel, Benet Devereux:
chi-Chek: A Multi-valued Model-Checker. CAV 2002: 505-509 - [c2]Arie Gurfinkel, Benet Devereux, Marsha Chechik:
Model exploration with temporal logic query checking. SIGSOFT FSE 2002: 139-148 - 2001
- [c1]Marsha Chechik, Benet Devereux, Arie Gurfinkel:
Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN. SPIN 2001: 16-36
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-05-22 01:53 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
