| Publication | Date of Publication | Type |
|---|
| Compositional reasoning in model checking | 2025-03-19 | Paper |
| Analytica -- an experiment in combining theorem proving and symbolic computation | 2024-06-21 | Paper |
Combining symbolic computation and theorem proving: Some problems of Ramanujan
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
| scientific article; zbMATH DE number 7088727 (Why is no real title available?) | 2019-08-05 | Paper |
Introduction to model checking
Handbook of Model Checking | 2018-07-20 | Paper |
From non-preemptive to preemptive scheduling using synchronization synthesis
Computer Aided Verification | 2018-03-01 | Paper |
SMT-based analysis of virtually synchronous distributed hybrid systems
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control | 2017-05-19 | Paper |
Rare-event verification for stochastic hybrid systems
Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control | 2017-05-16 | Paper |
Learning probabilistic systems from tree samples
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
-decidability over the reals
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
From non-preemptive to preemptive scheduling using synchronization synthesis
Formal Methods in System Design | 2017-05-15 | Paper |
Bayesian statistical model checking with application to Simulink/Stateflow verification
Proceedings of the 13th ACM international conference on Hybrid systems: computation and control | 2017-05-10 | Paper |
Solving QBF with counterexample guided refinement
Artificial Intelligence | 2016-03-08 | Paper |
\(2^{5}\) years of model checking
Lecture Notes in Computer Science | 2015-12-03 | Paper |
Counterexample-guided abstraction refinement for symbolic model checking
Journal of the ACM | 2015-11-12 | Paper |
Bayesian statistical model checking with application to Stateflow/Simulink verification
Formal Methods in System Design | 2014-06-30 | Paper |
| Automated compositional abstraction refinement for concurrent C programs: a two-level approach | 2013-08-30 | Paper |
Solving QBF with counterexample guided refinement
Theory and Applications of Satisfiability Testing – SAT 2012 | 2013-08-12 | Paper |
dReal: an SMT solver for nonlinear theories over the reals
Automated Deduction – CADE-24 | 2013-06-14 | Paper |
-complete decision procedures for satisfiability over the reals
Automated Reasoning | 2012-09-05 | Paper |
-complete decision procedures for satisfiability over the reals
Automated Reasoning | 2012-09-05 | Paper |
Computational modeling and verification of signaling pathways in cancer
Algebraic and Numeric Biology | 2012-06-08 | Paper |
Statistical model checking for cyber-physical systems
Automated Technology for Verification and Analysis | 2011-10-07 | Paper |
Quantifier elimination over finite fields using Gröbner bases
Algebraic Informatics | 2011-07-08 | Paper |
Statistical verification of probabilistic properties with unbounded until
Lecture Notes in Computer Science | 2011-05-12 | Paper |
A non-prenex, non-clausal QBF solver with game-state learning
Theory and Applications of Satisfiability Testing – SAT 2010 | 2010-09-29 | Paper |
On simulation-based probabilistic model checking of mixed-analog circuits
Formal Methods in System Design | 2010-09-16 | Paper |
An abstraction technique for real-time verification
Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems | 2010-06-02 | Paper |
Making predicate abstraction efficient: how to eliminate redundant predicates
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Counterexamples revisited: principles, algorithms, applications
Lecture Notes in Computer Science | 2010-03-23 | Paper |
Predicate abstraction with minimum predicates
Lecture Notes in Computer Science | 2010-02-05 | Paper |
Computing differential invariants of hybrid systems as fixed points
Formal Methods in System Design | 2009-11-23 | Paper |
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
Formal Methods in System Design | 2009-11-23 | Paper |
Theory and Applications of Satisfiability Testing
Lecture Notes in Computer Science | 2009-07-24 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2009-05-15 | Paper |
Integrated Formal Methods
Lecture Notes in Computer Science | 2009-05-07 | Paper |
Learning Minimal Separating DFA’s for Compositional Verification
Tools and Algorithms for the Construction and Analysis of Systems | 2009-03-31 | Paper |
The Image Computation Problem in Hybrid Systems Model Checking
Hybrid Systems: Computation and Control | 2009-03-11 | Paper |
Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction
Hybrid Systems: Computation and Control | 2009-03-11 | Paper |
Arithmetic Strengthening for Shape Analysis
Static Analysis | 2009-03-03 | Paper |
Model Checking – My 27-Year Quest to Overcome the State Explosion Problem
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Verification of Supervisory Control Software Using State Proximity and Merging
Hybrid Systems: Computation and Control | 2008-09-02 | Paper |
Verification of evolving software via component substitutability analysis
Formal Methods in System Design | 2008-07-30 | Paper |
The Birth of Model Checking
25 Years of Model Checking | 2008-07-15 | Paper |
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
Computer Aided Verification | 2008-07-15 | Paper |
Computing Differential Invariants of Hybrid Systems as Fixedpoints
Computer Aided Verification | 2008-07-15 | Paper |
DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC
25 Years of Model Checking | 2008-07-15 | Paper |
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems
Tools and Algorithms for the Construction and Analysis of Systems | 2008-04-11 | Paper |
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
Tools and Algorithms for the Construction and Analysis of Systems | 2008-04-11 | Paper |
SAT-Based Compositional Verification Using Lazy Learning
Computer Aided Verification | 2007-11-29 | Paper |
State/Event Software Verification for Branching-Time Specifications
Lecture Notes in Computer Science | 2007-11-29 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-09-28 | Paper |
Program Compatibility Approaches
Formal Methods for Components and Objects | 2007-09-11 | Paper |
Satisfiability Checking of Non-clausal Formulas Using General Matings
Lecture Notes in Computer Science | 2007-09-04 | Paper |
Verification of SpecC using predicate abstraction
Formal Methods in System Design | 2007-06-21 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2007-05-02 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Concurrent software verification with states, events, and deadlocks
Formal Aspects of Computing | 2006-10-25 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | Paper |
FM 2005: Formal Methods
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Hybrid Systems: Computation and Control
Lecture Notes in Computer Science | 2005-11-11 | Paper |
Tools and Algorithms for the Construction and Analysis of Systems
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
International Journal of Foundations of Computer Science | 2005-10-19 | Paper |
An Iterative Framework for Simulation Conformance
Journal Of Logic And Computation | 2005-10-18 | Paper |
CONCUR 2004 - Concurrency Theory
Lecture Notes in Computer Science | 2005-08-23 | Paper |
Predicate abstraction of ANSI-C programs using SAT
Formal Methods in System Design | 2004-11-22 | Paper |
Efficient verification of sequential and concurrent C programs
Formal Methods in System Design | 2004-11-22 | Paper |
| scientific article; zbMATH DE number 2102731 (Why is no real title available?) | 2004-09-24 | Paper |
| scientific article; zbMATH DE number 2102695 (Why is no real title available?) | 2004-09-24 | Paper |
| scientific article; zbMATH DE number 2087616 (Why is no real title available?) | 2004-08-11 | Paper |
| scientific article; zbMATH DE number 1979542 (Why is no real title available?) | 2003-09-14 | Paper |
| scientific article; zbMATH DE number 1956581 (Why is no real title available?) | 2003-07-30 | Paper |
| scientific article; zbMATH DE number 1903365 (Why is no real title available?) | 2003-05-01 | Paper |
| scientific article; zbMATH DE number 1903358 (Why is no real title available?) | 2003-05-01 | Paper |
| scientific article; zbMATH DE number 1852165 (Why is no real title available?) | 2003-01-09 | Paper |
Verification of out-of-order processor designs using model Checking and a light-weight completion function
Formal Methods in System Design | 2002-07-08 | Paper |
Bounded model checking using satisfiability solving
Formal Methods in System Design | 2002-05-21 | Paper |
| scientific article; zbMATH DE number 1670775 (Why is no real title available?) | 2001-11-11 | Paper |
| scientific article; zbMATH DE number 1670773 (Why is no real title available?) | 2001-11-11 | Paper |
| scientific article; zbMATH DE number 1538051 (Why is no real title available?) | 2001-08-05 | Paper |
| Model checking. | 2001-01-01 | Paper |
The Verus language: Representing time efficiently with BDDs
Theoretical Computer Science | 2000-12-12 | Paper |
| scientific article; zbMATH DE number 1487864 (Why is no real title available?) | 2000-12-11 | Paper |
NuSMV: A new symbolic model checker
International Journal on Software Tools for Technology Transfer. STTT | 2000-01-01 | Paper |
| scientific article; zbMATH DE number 1324666 (Why is no real title available?) | 1999-08-17 | Paper |
| scientific article; zbMATH DE number 1324652 (Why is no real title available?) | 1999-08-17 | Paper |
| scientific article; zbMATH DE number 1324663 (Why is no real title available?) | 1999-08-17 | Paper |
Analytica --- an experiment in combining theorem proving and symbolic computation
Journal of Automated Reasoning | 1999-06-29 | Paper |
A unified approach for showing language inclusion and equivalence between various types of -automata
Information Processing Letters | 1999-02-25 | Paper |
State space reduction using partial order techniques
International Journal on Software Tools for Technology Transfer. STTT | 1999-01-01 | Paper |
Analysis and verification of real-time systems using quantitative symbolic algorithms
International Journal on Software Tools for Technology Transfer. STTT | 1999-01-01 | Paper |
| scientific article; zbMATH DE number 910726 (Why is no real title available?) | 1997-02-17 | Paper |
A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems
Journal Of Logic And Computation | 1993-06-29 | Paper |
| scientific article; zbMATH DE number 177234 (Why is no real title available?) | 1993-05-18 | Paper |
| scientific article; zbMATH DE number 125884 (Why is no real title available?) | 1993-02-21 | Paper |
PARTHENON: A parallel theorem prover for non-horn clauses
Journal of Automated Reasoning | 1992-09-27 | Paper |
Symbolic model checking: \(10^{20}\) states and beyond
Information and Computation | 1992-09-27 | Paper |
| scientific article; zbMATH DE number 4180829 (Why is no real title available?) | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 4180789 (Why is no real title available?) | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 4119616 (Why is no real title available?) | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 4128366 (Why is no real title available?) | 1989-01-01 | Paper |
Reasoning about networks with many identical finite state processes
Information and Computation | 1989-01-01 | Paper |
Reasoning about procedures as parameters in the language L4
Information and Computation | 1989-01-01 | Paper |
Characterizing finite Kripke structures in propositional temporal logic
Theoretical Computer Science | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 4016870 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 3976939 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 3993457 (Why is no real title available?) | 1986-01-01 | Paper |
Automatic verification of finite-state concurrent systems using temporal logic specifications
ACM Transactions on Programming Languages and Systems | 1986-01-01 | Paper |
Automatic Verification of Sequential Circuits Using Temporal Logic
IEEE Transactions on Computers | 1986-01-01 | Paper |
| scientific article; zbMATH DE number 3932379 (Why is no real title available?) | 1985-01-01 | Paper |
The complexity of propositional linear temporal logics
Journal of the ACM | 1985-01-01 | Paper |
Hierarchical verification of asynchronous circuits using temporal logic
Theoretical Computer Science | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3858385 (Why is no real title available?) | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3861073 (Why is no real title available?) | 1984-01-01 | Paper |
Can message buffers be axiomatized in linear temporal logic?
Information and Control | 1984-01-01 | Paper |
The characterization problem for Hoare logics
Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences | 1984-01-01 | Paper |
Effective Axiomatizations of Hoare Logics
Journal of the ACM | 1983-01-01 | Paper |
| scientific article; zbMATH DE number 3870578 (Why is no real title available?) | 1982-01-01 | Paper |
Using branching time temporal logic to synthesize synchronization skeletons
Science of Computer Programming | 1982-01-01 | Paper |
Task management in Ada—A critical evaluation for real-time multiprocessors
Software: Practice and Experience | 1981-01-01 | Paper |
| scientific article; zbMATH DE number 3714896 (Why is no real title available?) | 1980-01-01 | Paper |
Synthesis of Resource Invariants for Concurrent Programs
ACM Transactions on Programming Languages and Systems | 1980-01-01 | Paper |
Proving correctness of coroutines without history variables
Acta Informatica | 1980-01-01 | Paper |
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
Journal of the ACM | 1979-01-01 | Paper |
Program invariants as fixedpoints
Computing | 1979-01-01 | Paper |
