Stop the war!Остановите войну!
for scientists:
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
- 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]