Kenneth L. McMillan

Proceedings of the Formal Methods: Foundations and Applications - 16th Brazilian Symposium, 2013

On Solving Universally Quantified Horn Clauses.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Andrey Rybalchenko

Proceedings of the Static Analysis - 20th International Symposium, 2013

Inductive invariant generation via abductive inference.

[BibT_eX]

[DOI]

Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

Beautiful Interpolants.

[BibT_eX]

[DOI]

Aws Albarghouthi

Leonardo Mendonça de Moura

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

2012

Beyond First-Order Satisfaction: Fixed Points, Interpolants, Automata and Polynomials.

[BibT_eX]

[DOI]

Thomas Ball

Nikolaj S. Bjørner

Margus Veanes

Proceedings of the Model Checking Software - 19th International Workshop, 2012

Minimum Satisfying Assignments for SMT.

[BibT_eX]

[DOI]

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

Program Verification as Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Nikolaj S. Bjørner

Andrey Rybalchenko

Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011

Invisible Invariants and Abstract Interpretation.

[BibT_eX]

[DOI]

Lenore D. Zuck

Proceedings of the Static Analysis - 18th International Symposium, 2011

Widening and Interpolation.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 18th International Symposium, 2011

Interpolants from Z3 proofs.

[BibT_eX]

[DOI]

Proceedings of the International Conference on Formal Methods in Computer-Aided Design, 2011

2010

Lazy Annotation for Program Testing and Verification.

[BibT_eX]

[DOI]

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

2009

Abstract Counterexamples for Non-disjunctive Abstractions.

[BibT_eX]

[DOI]

Lenore D. Zuck

Proceedings of the Reachability Problems, 3rd International Workshop, 2009

What's in Common between Test, Model Checking, and Decision Procedures?

[BibT_eX]

[DOI]

Proceedings of the Formal Methods for Industrial Critical Systems, 2009

Generalizing DPLL to Richer Logics.

[BibT_eX]

[DOI]

Andreas Kuehlmann

Mooly Sagiv

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Automated assumption generation for compositional verification.

[BibT_eX]

[DOI]

Anubhav Gupta

Zhaohui Fu

Formal Methods Syst. Des., 2008

Quantified Invariant Generation Using an Interpolating Saturation Prover.

[BibT_eX]

[DOI]

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

Relevance heuristics for program analysis.

[BibT_eX]

[DOI]

Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008

Proofs, Interpolants, and Relevance Heuristics.

[BibT_eX]

[DOI]

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

2007

Interpolant-Based Transition Relation Approximation.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2007

Interpolants and Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2007

Combining Abstraction Refinement and SAT-Based Model Checking.

[BibT_eX]

[DOI]

Nina Amla

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

Array Abstractions from Proofs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

Toward Property-Driven Abstraction for Heap Manipulating Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2007

2006

A Practical and Complete Approach to Predicate Refinement.

[BibT_eX]

[DOI]

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

Liveness by Invisible Invariants.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006

Lazy Abstraction with Interpolants.

[BibT_eX]

[DOI]

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

2005

An interpolating theorem prover.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

Deciding Global Partial-Order Properties.

[BibT_eX]

[DOI]

Rajeev Alur

Doron A. Peled

Formal Methods Syst. Des., 2005

Applications of Craig Interpolants in Model Checking.

[BibT_eX]

[DOI]

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

An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

Applications of Craig Interpolation to Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Applications and Theory of Petri Nets 2005, 2005

2004

A Hybrid of Counterexample-Based and Proof-Based Abstraction.

[BibT_eX]

[DOI]

Nina Amla

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

2003

Automatic Abstraction without Counterexamples.

[BibT_eX]

[DOI]

Nina Amla

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

Experimental Analysis of Different Techniques for Bounded Model Checking.

[BibT_eX]

[DOI]

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

Craig Interpolation and Reachability Analysis.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis, 10th International Symposium, 2003

Methods for exploiting SAT solvers in unbounded model checking.

[BibT_eX]

[DOI]

Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

Interpolation and SAT-Based Model Checking.

[BibT_eX]

[DOI]

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

2002

Applying SAT Methods in Unbounded Symbolic Model Checking.

[BibT_eX]

[DOI]

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

2001

Theory of latency-insensitive design.

[BibT_eX]

[DOI]

Luca P. Carloni

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2001

Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2001

Microarchitecture Verification by Compositional Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000

Sibling-substitution-based BDD minimization using don't cares.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000

A methodology for hardware verification using compositional model checking.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2000

Model-Checking of Correctness Conditions for Concurrent Objects.

[BibT_eX]

[DOI]

Rajeev Alur

Doron A. Peled

Inf. Comput., 2000

Some Strategies for Proving Theorems with a Model Checker.

[BibT_eX]

[DOI]

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Induction in Compositional Model Checking.

[BibT_eX]

[DOI]

Shaz Qadeer

James B. Saxe

Proceedings of the Computer Aided Verification, 12th International Conference, 2000

1999

Probabilistic state space search.

[BibT_eX]

[DOI]

Andreas Kuehlmann

Robert K. Brayton

Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

A methodology for correct-by-construction latency insensitive design.

[BibT_eX]

[DOI]

Luca P. Carloni

Alexander Saldanha

Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Circular Compositional Reasoning about Liveness.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1999

Verification of Infinite State Systems by Compositional Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1999

Latency Insensitive Protocols.

[BibT_eX]

[DOI]

Luca P. Carloni

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998

Proof Rules for Model Checking Systems with Data.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1998

Minimalist Proof Assistants: Interactions of Technology and Methodology in Formal System Level Verification (abstract).

[BibT_eX]

[DOI]

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

Approximation and Decomposition of Binary Decision Diagrams.

[BibT_eX]

[DOI]

Proceedings of the 35th Conference on Design Automation, 1998

Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1997

Safe BDD Minimization Using Don't Cares.

[BibT_eX]

[DOI]

Proceedings of the 34st Conference on Design Automation, 1997

A Compositional Rule for Hardware Design Refinement.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

1996

Engineering Change in a Non-Deterministic FSM Setting.

[BibT_eX]

[DOI]

Proceedings of the 33st Conference on Design Automation, 1996

A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Symbolic Model Checking.

[BibT_eX]

[DOI]

Edmund M. Clarke

Sérgio Vale Aguiar Campos

Vasiliki Hartonas-Garmhausen

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995

A Structural Induction Theorem for Processes

[BibT_eX]

[DOI]

Robert P. Kurshan

Inf. Comput., February, 1995

A Technique of State Space Search Based on Unfolding.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1995

Verification of the Futurebus+ Cache Coherence Protocol.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1995

Fast discrete function evaluation using decision diagrams.

[BibT_eX]

[DOI]

Patrick C. McGeer

Alexander Saldanha

Patrick Scaglia

Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 32st Conference on Design Automation, 1995

Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 1995

Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study.

[BibT_eX]

[DOI]

Ásgeir Th. Eiríksson

Proceedings of the Computer Aided Verification, 1995

1994

Symbolic model checking for sequential circuit verification.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994

Fitting Formal Methods into the Design Cycle.

[BibT_eX]

[DOI]

Proceedings of the 31st Conference on Design Automation, 1994

Panel: Complex System Verification: The Challenge Ahead.

[BibT_eX]

[DOI]

Johan Van Ginderdeuren

Stephen Ricca

Steve Sapiro

Naeem Zafar

Proceedings of the 31st Conference on Design Automation, 1994

Hierarchical Representations of Discrete Functions, with Application to Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 6th International Conference, 1994

1993

Symbolic model checking.

[BibT_eX]

[DOI]

Kluwer, ISBN: 978-1-4615-3190-6, 1993

1992

Symbolic Model Checking: 10^20 States and Beyond

[BibT_eX]

[DOI]

Inf. Comput., June, 1992

Algorithms for Interface Timing Verification.

[BibT_eX]

[DOI]

David L. Dill

Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1991

Analysis of digital circuits through symbolic reduction.

[BibT_eX]

[DOI]

Robert P. Kurshan

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1991

A language for compositional specification and verification of finite state hardware controllers.

[BibT_eX]

[DOI]

Edmund M. Clarke

David E. Long

Proc. IEEE, 1991

Synthesizing Converters Between Finite State Protocols.

[BibT_eX]

[DOI]

Janaki Akella

Proceedings of the Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1991

1990

Sequential Circuit Verification Using Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990

1989

Compositional Model Checking

[BibT_eX]

[DOI]

Edmund M. Clarke

David E. Long