default search action
Arie 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
- 2024
- [j18]Hari Govind Vediramana Krishnan
, YuTing Chen
Global guidance for local generalization in model checking. Formal Methods Syst. Des. 63(1): 81-109 (2024) - [c117]Arie Gurfinkel:
Constrained Horn Clauses for Program Verification and Synthesis (Invited Talk). CONCUR 2024: 1:1-1:1 - [c116]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 - [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.
Speculative SAT Modulo SAT. TACAS (1) 2024: 43-60 - [e5]Arie Gurfinkel
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
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
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] - [i24]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) - [i23]Siddharth Priya, Arie Gurfinkel:
Ownership in low-level intermediate representation. CoRR abs/2408.04043 (2024) - [i22]Siddharth Priya, Temesghen Kahsai, Arie Gurfinkel:
Unlocking the Power of Environment Assumptions for Unit Proofs. CoRR abs/2409.12269 (2024) - 2023
- [c112]Isabel Garcia-Contreras
Fast Approximations of Quantifier Elimination. CAV (2) 2023: 64-86 - [c111]Joseph Tafese
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
Verifying verified code. Innov. Syst. Softw. Eng. 18(3): 335-346 (2022) - [j16]Hari Govind V. K.
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
Bounded Model Checking for LLVM. FMCAD 2022: 214-224 - [c107]Isabel Garcia-Contreras
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
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.
Logical Characterization of Coherent Uninterpreted Programs. CoRR abs/2107.12902 (2021) - 2020
- [c99]Hari Govind Vediramana Krishnan
Global Guidance for Local Generalization in Model Checking. CAV (2) 2020: 101-125 - [c98]Hongce Zhang
Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis. ECAI 2020: 1690-1697 - [c97]Hari Govind V. K.
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
Property Directed Self Composition. CAV (1) 2019: 161-179 - [c95]Hari Govind Vediramana Krishnan
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
Local Reasoning for Parameterized First Order Protocols. NFM 2019: 36-53 - [c92]Elazar Gershuni, Nadav Amit
Simple and precise static analysis of untrusted Linux kernel extensions. PLDI 2019: 1069-1084 - [c91]Arie Gurfinkel
The Science, Art, and Magic of Constrained Horn Clauses. SYNASC 2019: 6-10 - [c90]Grigory Fedyukovich
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
Quantifiers on Demand. ATVA 2018: 248-266 - [c88]Reza Babaee
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
Prevent : A Predictive Run-Time Verification Framework Using Statistical Learning. SEFM 2018: 205-220 - [c86]Andreas Katis
Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts. TACAS (2) 2018: 176-193 - [c85]Jeffrey Gennari, Arie Gurfinkel
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
K-induction without unrolling. FMCAD 2017: 148-155 - [c83]Matteo Marescotti, Arie Gurfinkel
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
A Context-Sensitive Memory Model for Verification of C/C++ Programs. SAS 2017: 148-168 - [c80]Yakir Vizel, Arie Gurfinkel
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
SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3): 175-205 (2016) - [c79]Grigory Fedyukovich
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
CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. SEFM 2016: 347-366 - [c76]Arie Gurfinkel
SMT-based verification of parameterized systems. SIGSOFT FSE 2016: 338-348 - [c75]Caterina Urban, Arie Gurfinkel
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
Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability. CoRR abs/1610.05867 (2016) - 2015
- [j13]Sagar Chaki, Arie Gurfinkel
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
Horn Clause Solvers for Program Verification. Fields of Logic and Computation II 2015: 24-51 - [c73]Arie Gurfinkel
The SeaHorn Verification Framework. CAV (1) 2015: 343-361 - [c72]Yakir Vizel, Arie Gurfinkel
Fast Interpolating BMC. CAV (1) 2015: 641-657 - [c71]Arie Gurfinkel
Pushing to the Top. FMCAD 2015: 65-72 - [c70]Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96 - [c69]Grigory Fedyukovich
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
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
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
Efficient verification of periodic programs using sequential consistency and snapshots. FMCAD 2014: 51-58 - [c62]Arie Gurfinkel
DRUPing for interpolates. FMCAD 2014: 99-106 - [c61]Alexander Ivrii, Arie Gurfinkel
Small inductive safe invariants. FMCAD 2014: 115-122 - [c60]Grigory Fedyukovich
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
Symbolic optimization with SMT solvers. POPL 2014: 607-618 - [c57]Arie Gurfinkel
Synthesizing Safe Bit-Precise Invariants. TACAS 2014: 93-108 - [c56]Arie Gurfinkel
FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution). TACAS 2014: 408-411 - [c55]Pierre-Loïc Garoche, Arie Gurfinkel
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
Beyond vacuity: towards the strongest passing formula. Formal Methods Syst. Des. 43(3): 552-571 (2013) - [c54]Arie Gurfinkel
Interpolation Properties and SAT-Based Model Checking. ATVA 2013: 255-271 - [c53]Anvesh Komuravelli, Arie Gurfinkel
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
Finding Errors in Python Programs Using Dynamic Symbolic Execution. ICTSS 2013: 283-289 - [c49]Aws Albarghouthi, Arie Gurfinkel
UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution). TACAS 2013: 637-640 - [c48]Sagar Chaki, Arie Gurfinkel
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
Robust Vacuity for Branching Temporal Logic. ACM Trans. Comput. Log. 13(1): 1:1-1:32 (2012) - [j9]Naghmeh Ghafari, Arie Gurfinkel
Reachability Problems in Piecewise FIFO Systems. ACM Trans. Comput. Log. 13(1): 7:1-7:33 (2012) - [c47]Aws Albarghouthi, Yi Li
Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification. CAV 2012: 672-678 - [c46]Wesley Jin, Sagar Chaki, Cory F. Cohen, Arie Gurfinkel
Binary Function Clustering Using Semantic Hashes. ICMLA (1) 2012: 386-391 - [c45]Aws Albarghouthi, Arie Gurfinkel
Craig Interpretation. SAS 2012: 300-316 - [c44]Aws Albarghouthi, Arie Gurfinkel
From Under-Approximations to Over-Approximations and Back. TACAS 2012: 157-172 - [c43]Aws Albarghouthi, Arie Gurfinkel
Whale: An Interpolation-Based Algorithm for Inter-procedural Verification. VMCAI 2012: 39-55 - [c42]Sagar Chaki, Arie Gurfinkel
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
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
Efficient Predicate Abstraction of Program Summaries. NASA Formal Methods 2011: 131-145 - [c38]Shoham Ben-David, Marsha Chechik, Arie Gurfinkel
CSSL: a logic for specifying conditional scenarios. SIGSOFT FSE 2011: 37-47 - 2010
- [j6]Jocelyn Simmonds
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
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
Abstract Analysis of Symbolic Executions. CAV 2010: 495-510 - [c36]Ipek Ozkaya
Using Architecturally Significant Requirements for Guiding System Evolution. CSMR 2010: 127-136 - [c35]Hana Chockler
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
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
Decision diagrams for linear arithmetic. FMCAD 2009: 53-60 - [c31]Naghmeh Ghafari, Arie Gurfinkel
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
Towards engineered architecture evolution. MiSE@ICSE 2009: 1-6 - [c29]Ou Wei, Arie Gurfinkel
Mixed Transition Systems Revisited. VMCAI 2009: 349-365 - 2008
- [c28]Arie Gurfinkel
Model Checking Recursive Programs with Exact Predicate Abstraction. ATVA 2008: 95-110 - [c27]Hana Chockler
Beyond Vacuity: Towards the Strongest Passing Formula. FMCAD 2008: 1-8 - [c26]Arie Gurfinkel
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
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
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. FMCAD 2007: 3-12 - [c21]Naghmeh Ghafari, Arie Gurfinkel
Algorithmic Analysis of Piecewise FIFO Systems. FMCAD 2007: 45-52 - [c20]Mihaela Gheorghiu, Arie Gurfinkel
Finding State Solutions to Temporal Logic Queries. IFM 2007: 273-292 - 2006
- [j3]Marsha Chechik, Arie Gurfinkel
Data structures for symbolic multi-valued model-checking. Formal Methods Syst. Des. 29(3): 295-344 (2006) - [c19]Arie Gurfinkel
Yasm: A Software Model-Checker for Verification and Refutation. CAV 2006: 170-174 - [c18]Arie Gurfinkel
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
How Thorough Is Thorough Enough? CHARME 2005: 65-80 - [c15]Ou Wei, Arie Gurfinkel
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
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
Extending Extended Vacuity. FMCAD 2004: 306-321 - [c10]Arie Gurfinkel
How Vacuous Is Vacuous? TACAS 2004: 451-466 - [c9]Sergey Berezin, Clark W. Barrett
A Practical Approach to Partial Functions in CVC Lite. D/PDPAR@IJCAR 2004: 13-23 - 2003
- [j2]Marsha Chechik, Benet Devereux, Steve M. Easterbrook
Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4): 371-408 (2003) - [j1]Arie Gurfinkel
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
Multi-Valued Model Checking via Classical Model Checking. CONCUR 2003: 263-277 - [c6]Arie Gurfinkel
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
Proof-Like Counter-Examples. TACAS 2003: 160-175 - 2002
- [c3]Marsha Chechik, Arie Gurfinkel
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 2024-12-13 20:07 CET 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: