Arie Gurfinkel

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Lazy but Effective Functional Synthesis.

[BibT_eX]

[DOI]

Aarti Gupta

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2019

The Science, Art, and Magic of Constrained Horn Clauses.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

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.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Local Reasoning for Parameterized First Order Protocols.

[BibT_eX]

[DOI]

Rylo Ashmore

Richard J. Trefler

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Unification-based Pointer Analysis without Oversharing.

[BibT_eX]

[DOI]

Jakub Kuderski

Hari Govind Vediramana Krishnan

Proceedings of the 2019 Formal Methods in Computer Aided Design, 2019

Property Directed Self Composition.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Interpolating Strong Induction.

[BibT_eX]

[DOI]

Vijay Ganesh

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2018

BDD-Based Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Model Checking., 2018

Executable Counterexamples in Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2018

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Reza Babaee

Sebastian Fischmeister

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.

[BibT_eX]

[DOI]

Reza Babaee

Sebastian Fischmeister

Proceedings of the Runtime Verification - 18th International Conference, 2018

Quantifiers on Demand.

[BibT_eX]

[DOI]

Sharon Shoham

Proceedings of the Automated Technology for Verification and Analysis, 2018

2017

IC3 - Flipping the E in ICE.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2017

A Context-Sensitive Memory Model for Verification of C/C++ Programs.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 24th International Symposium, 2017

Automated analysis of Stateflow models.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

Designing parallel PDR.

[BibT_eX]

[DOI]

Matteo Marescotti

Antti Eero Johannes Hyvärinen

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

K-induction without unrolling.

[BibT_eX]

[DOI]

Alexander Ivrii

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

2016

SMT-based model checking for recursive programs.

[BibT_eX]

[DOI]

Anvesh Komuravelli

Formal Methods Syst. Des., 2016

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

[BibT_eX]

[DOI]

CoRR, 2016

Synthesizing Ranking Functions from Bits and Pieces.

[BibT_eX]

[DOI]

Caterina Urban

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

SMT-based verification of parameterized systems.

[BibT_eX]

[DOI]

Sharon Shoham

Yuri Meshman

Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

CoCoSpec: A Mode-Aware Contract Language for Reactive Systems.

[BibT_eX]

[DOI]

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Maximal specification synthesis.

[BibT_eX]

[DOI]

Isil Dillig

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

Property Directed Equivalence via Abstract Simulation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

Algorithmic logic-based verification.

[BibT_eX]

[DOI]

ACM SIGLOG News, 2015

Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation).

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2015

Property Directed Polyhedral Abstraction.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2015

SeaHorn: A Framework for Verifying C Programs (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Algorithmic Logic-Based Verification with SeaHorn.

[BibT_eX]

[DOI]

Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2015

Automated Discovery of Simulation Between Programs.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Pushing to the Top.

[BibT_eX]

[DOI]

Alexander Ivrii

Proceedings of the Formal Methods in Computer-Aided Design, 2015

Fast Interpolating BMC.

[BibT_eX]

[DOI]

Sharad Malik

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

The SeaHorn Verification Framework.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Horn Clause Solvers for Program Verification.

[BibT_eX]

[DOI]

Proceedings of the Fields of Logic and Computation II, 2015

2014

Synthesizing Modular Invariants for Synchronous Code.

[BibT_eX]

[DOI]

Pierre-Loïc Garoche

Proceedings of the Proceedings First Workshop on Horn Clauses for Verification and Synthesis, 2014

Synthesizing Safe Bit-Precise Invariants.

[BibT_eX]

[DOI]

Anton Belov

João Marques-Silva

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

FrankenBit: Bit-Precise Verification with Many Bits - (Competition Contribution).

[BibT_eX]

[DOI]

Anton Belov

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

Symbolic optimization with SMT solvers.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the 3rd ACM SIGPLAN Program Protection and Reverse Engineering Workshop 2014, 2014

Incremental Verification of Compiler Optimizations.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

Small inductive safe invariants.

[BibT_eX]

[DOI]

Alexander Ivrii

Anton Belov

Proceedings of the Formal Methods in Computer-Aided Design, 2014

DRUPing for interpolates.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Efficient verification of periodic programs using sequential consistency and snapshots.

[BibT_eX]

[DOI]

Nishant Sinha

Proceedings of the Formal Methods in Computer-Aided Design, 2014

Interpolating Property Directed Reachability.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Beyond vacuity: towards the strongest passing formula.

[BibT_eX]

[DOI]

Hana Chockler

Formal Methods Syst. Des., 2013

Compositional Sequentialization of Periodic Programs.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

UFO: Verification with Interpolants and Abstract Interpretation - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Finding Errors in Python Programs Using Dynamic Symbolic Execution.

[BibT_eX]

[DOI]

Proceedings of the Testing Software and Systems, 2013

Instantiations, Zippers and EPR Interpolation.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2013, 2013

Verifying periodic programs with priority inheritance locks.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2013

Automatic Abstraction in SMT-Based Unbounded Software Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Interpolation Properties and SAT-Based Model Checking.

[BibT_eX]

[DOI]

Simone Fulvio Rollini

Proceedings of the Automated Technology for Verification and Analysis, 2013

2012

Robust Vacuity for Branching Temporal Logic.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2012

Reachability Problems in Piecewise FIFO Systems.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2012

Propositional Interpolation Systems for Model Checking

[BibT_eX]

[DOI]

Simone Fulvio Rollini

CoRR, 2012

Regression Verification for Multi-threaded Programs.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

Whale: An Interpolation-Based Algorithm for Inter-procedural Verification.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012

From Under-Approximations to Over-Approximations and Back.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

Craig Interpretation.

[BibT_eX]

[DOI]

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

Binary Function Clustering Using Semantic Hashes.

[BibT_eX]

[DOI]

Proceedings of the 11th International Conference on Machine Learning and Applications, 2012

Ufo: A Framework for Abstraction- and Interpolation-Based Software Verification.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

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

[BibT_eX]

[DOI]

Innov. Syst. Softw. Eng., 2011

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

[BibT_eX]

[DOI]

Inf. Comput., 2011

CSSL: a logic for specifying conditional scenarios.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Samir Sapra

Proceedings of the NASA Formal Methods, 2011

Supervised learning for provenance-similarity of binaries.

[BibT_eX]

[DOI]

Cory F. Cohen

Proceedings of the 17th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, 2011

Time-bounded analysis of real-time systems.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2010

Combining predicate and numeric abstraction for software model checking.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2010

Boxes: A Symbolic Abstract Domain of Boxes.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 17th International Symposium, 2010

Variants of LTL Query Checking.

[BibT_eX]

[DOI]

Hana Chockler

Proceedings of the Hardware and Software: Verification and Testing, 2010

Using Architecturally Significant Requirements for Guiding System Evolution.

[BibT_eX]

[DOI]

Proceedings of the 14th European Conference on Software Maintenance and Reengineering, 2010

Abstract Analysis of Symbolic Executions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009

Mixed Transition Systems Revisited.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2009

Towards engineered architecture evolution.

[BibT_eX]

[DOI]

Proceedings of the ICSE Workshop on Modeling in Software Engineering, 2009

Verification of Parameterized Systems with Combinations of Abstract Domains.

[BibT_eX]

[DOI]

Naghmeh Ghafari

Richard J. Trefler

Proceedings of the Formal Techniques for Distributed Systems, 2009

Decision diagrams for linear arithmetic.

[BibT_eX]

[DOI]

Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, 2009

2008

PtYasm: Software Model Checking with Proof Templates.

[BibT_eX]

[DOI]

Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates.

[BibT_eX]

[DOI]

Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

Model Checking Recursive Programs with Exact Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

Model-checking with many values.

[BibT_eX]

[DOI]

PhD thesis, 2007

A framework for counterexample generation and exploration.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2007

Finding State Solutions to Temporal Logic Queries.

[BibT_eX]

[DOI]

Mihaela Gheorghiu

Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Algorithmic Analysis of Piecewise FIFO Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 7th International Conference, 2007

Finding Environment Guarantees.

[BibT_eX]

[DOI]

Mihaela Gheorghiu

Proceedings of the Fundamental Approaches to Software Engineering, 2007

2006

Data structures for symbolic multi-valued model-checking.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2006

Systematic Construction of Abstractions for Model-Checking.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2006

Why Waste a Perfectly Good Abstraction?.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Yasm: A Software Model-Checker for Verification and Refutation.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Model-Checking Software Using Precise Abstractions.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, 2005

Stuttering Abstraction for Model Checkin.

[BibT_eX]

[DOI]

Shiva Nejati

Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Identification and Counter Abstraction for Full Virtual Symmetry.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

How Thorough Is Thorough Enough?

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

A Practical Approach to Partial Functions in CVC Lite.

[BibT_eX]

[DOI]

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

How Vacuous Is Vacuous?

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Extending Extended Vacuity.

[BibT_eX]

[DOI]

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

2003

Temporal Logic Query Checking: A Tool for Model Exploration.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2003

Multi-valued symbolic model-checking.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2003

Proof-Like Counter-Examples.

[BibT_eX]

[DOI]

Christopher D. Thompson-Walsh

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

\chiChek: A Model Checker for Multi-Valued Reasoning.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Software Engineering, 2003

Generating Counterexamples for Multi-valued Model-Checking.

[BibT_eX]

[DOI]

Proceedings of the FME 2003: Formal Methods, 2003

Multi-Valued Model Checking via Classical Model Checking.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2003, 2003

TLQSolver: A Temporal Logic Query Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

Model exploration with temporal logic query checking.

[BibT_eX]

[DOI]

Proceedings of the Tenth ACM SIGSOFT Symposium on Foundations of Software Engineering 2002, 2002

chi-Chek: A Multi-valued Model-Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001

Model-Checking Infinite State-Space Systems with Fine-Grained Abstractions Using SPIN.

[BibT_eX]

[DOI]