Arie Gurfinkel

According to our database1, Arie Gurfinkel authored at least 108 papers between 2001 and 2020.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepage:

On csauthors.net:

Bibliography

2020
Global Guidance for Local Generalization in Model Checking.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Lazy but Effective Functional Synthesis.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

The Science, Art, and Magic of Constrained Horn Clauses.
Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2019

Simple and precise static analysis of untrusted Linux kernel extensions.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Local Reasoning for Parameterized First Order Protocols.
Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Unification-based Pointer Analysis without Oversharing.
Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

Property Directed Self Composition.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Interpolating Strong Induction.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018
BDD-Based Symbolic Model Checking.
Proceedings of the Handbook of Model Checking., 2018

Executable Counterexamples in Software Model Checking.
Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

<i>P</i>revent : A Predictive Run-Time Verification Framework Using Statistical Learning.
Proceedings of the Software Engineering and Formal Methods - 16th International Conference, 2018

Predictive Run-Time Verification of Discrete-Time Reachability Properties in Black-Box Systems Using Trace-Level Abstraction and Statistical Learning.
Proceedings of the Runtime Verification - 18th International Conference, 2018

Quantifiers on Demand.
Proceedings of the Automated Technology for Verification and Analysis, 2018

2017
IC3 - Flipping the E in ICE.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

A Context-Sensitive Memory Model for Verification of C/C++ Programs.
Proceedings of the Static Analysis - 24th International Symposium, 2017

Automated analysis of Stateflow models.
Proceedings of the LPAR-21, 2017

Designing parallel PDR.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

K-induction without unrolling.
Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016
SMT-based model checking for recursive programs.
Formal Methods Syst. Des., 2016

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability.
CoRR, 2016

Synthesizing Ranking Functions from Bits and Pieces.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

SMT-based verification of parameterized systems.
Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

CoCoSpec: A Mode-Aware Contract Language for Reactive Systems.
Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Maximal specification synthesis.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Property Directed Equivalence via Abstract Simulation.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015
Algorithmic logic-based verification.
ACM SIGLOG News, 2015

Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation).
Formal Methods Syst. Des., 2015

Property Directed Polyhedral Abstraction.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

SeaHorn: A Framework for Verifying C Programs (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Algorithmic Logic-Based Verification with SeaHorn.
Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2015

Automated Discovery of Simulation Between Programs.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Pushing to the Top.
Proceedings of the Formal Methods in Computer-Aided Design, 2015

Fast Interpolating BMC.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

The SeaHorn Verification Framework.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Horn Clause Solvers for Program Verification.
Proceedings of the Fields of Logic and Computation II, 2015

2014
Synthesizing Modular Invariants for Synchronous Code.
Proceedings of the Proceedings First Workshop on Horn Clauses for Verification and Synthesis, 2014

Synthesizing Safe Bit-Precise Invariants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Symbolic optimization with SMT solvers.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis.
Proceedings of the 3rd ACM SIGPLAN Program Protection and Reverse Engineering Workshop 2014, 2014

Incremental Verification of Compiler Optimizations.
Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Small inductive safe invariants.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

DRUPing for interpolates.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Efficient verification of periodic programs using sequential consistency and snapshots.
Proceedings of the Formal Methods in Computer-Aided Design, 2014

Interpolating Property Directed Reachability.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013
Beyond vacuity: towards the strongest passing formula.
Formal Methods Syst. Des., 2013

Compositional Sequentialization of Periodic Programs.
Proceedings of the Verification, 2013

UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Finding Errors in Python Programs Using Dynamic Symbolic Execution.
Proceedings of the Testing Software and Systems, 2013

Instantiations, Zippers and EPR Interpolation.
Proceedings of the LPAR 2013, 2013

Verifying periodic programs with priority inheritance locks.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Automatic Abstraction in SMT-Based Unbounded Software Model Checking.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Interpolation Properties and SAT-Based Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
Robust Vacuity for Branching Temporal Logic.
ACM Trans. Comput. Log., 2012

Reachability Problems in Piecewise FIFO Systems.
ACM Trans. Comput. Log., 2012

Propositional Interpolation Systems for Model Checking
CoRR, 2012

Regression Verification for Multi-threaded Programs.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Whale: An Interpolation-Based Algorithm for Inter-procedural Verification.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

From Under-Approximations to Over-Approximations and Back.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Craig Interpretation.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Binary Function Clustering Using Semantic Hashes.
Proceedings of the 11th International Conference on Machine Learning and Applications, 2012

Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Automated assume-guarantee reasoning for omega-regular systems and specifications.
ISSE, 2011

On the consistency, expressiveness, and precision of partial modeling formalisms.
Inf. Comput., 2011

CSSL: a logic for specifying conditional scenarios.
Proceedings of the SIGSOFT/FSE'11 19th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-19) and ESEC'11: 13th European Software Engineering Conference (ESEC-13), 2011

Efficient Predicate Abstraction of Program Summaries.
Proceedings of the NASA Formal Methods, 2011

Supervised learning for provenance-similarity of binaries.
Proceedings of the 17th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2011

Time-bounded analysis of real-time systems.
Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

2010
Exploiting resolution proofs to speed up LTL vacuity detection for BMC.
Int. J. Softw. Tools Technol. Transf., 2010

Combining predicate and numeric abstraction for software model checking.
Int. J. Softw. Tools Technol. Transf., 2010

Boxes: A Symbolic Abstract Domain of Boxes.
Proceedings of the Static Analysis - 17th International Symposium, 2010

Variants of LTL Query Checking.
Proceedings of the Hardware and Software: Verification and Testing, 2010

Using Architecturally Significant Requirements for Guiding System Evolution.
Proceedings of the 14th European Conference on Software Maintenance and Reengineering, 2010

Abstract Analysis of Symbolic Executions.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Mixed Transition Systems Revisited.
Proceedings of the Verification, 2009

Towards engineered architecture evolution.
Proceedings of the ICSE Workshop on Modeling in Software Engineering, 2009

Verification of Parameterized Systems with Combinations of Abstract Domains.
Proceedings of the Formal Techniques for Distributed Systems, 2009

Decision diagrams for linear arithmetic.
Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008
PtYasm: Software Model Checking with Proof Templates.
Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates.
Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

Model Checking Recursive Programs with Exact Predicate Abstraction.
Proceedings of the Automated Technology for Verification and Analysis, 2008

2007
A framework for counterexample generation and exploration.
Int. J. Softw. Tools Technol. Transf., 2007

Finding State Solutions to Temporal Logic Queries.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Algorithmic Analysis of Piecewise FIFO Systems.
Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Finding Environment Guarantees.
Proceedings of the Fundamental Approaches to Software Engineering, 2007

2006
Data structures for symbolic multi-valued model-checking.
Formal Methods Syst. Des., 2006

Systematic Construction of Abstractions for Model-Checking.
Proceedings of the Verification, 2006

Why Waste a Perfectly Good Abstraction?.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Yasm: A Software Model-Checker for Verification and Refutation.
Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005
A Practical Approach to Partial Functions in CVC Lite.
Electron. Notes Theor. Comput. Sci., 2005

Model-Checking Software Using Precise Abstractions.
Proceedings of the Verified Software: Theories, 2005

Stuttering Abstraction for Model Checkin.
Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Identification and Counter Abstraction for Full Virtual Symmetry.
Proceedings of the Correct Hardware Design and Verification Methods, 2005

How Thorough Is Thorough Enough?
Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004
How Vacuous Is Vacuous?
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Extending Extended Vacuity.
Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

2003
Temporal Logic Query Checking: A Tool for Model Exploration.
IEEE Trans. Software Eng., 2003

Multi-valued symbolic model-checking.
ACM Trans. Softw. Eng. Methodol., 2003

Proof-Like Counter-Examples.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

\chiChek: A Model Checker for Multi-Valued Reasoning.
Proceedings of the 25th International Conference on Software Engineering, 2003

Generating Counterexamples for Multi-valued Model-Checking.
Proceedings of the FME 2003: Formal Methods, 2003

Multi-Valued Model Checking via Classical Model Checking.
Proceedings of the CONCUR 2003, 2003

TLQSolver: A Temporal Logic Query Checker.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002
Model exploration with temporal logic query checking.
Proceedings of the Tenth ACM SIGSOFT Symposium on Foundations of Software Engineering 2002, 2002

chi-Chek: A Multi-valued Model-Checker.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN.
Proceedings of the Model Checking Software, 2001


  Loading...