| Publication | Date of Publication | Type |
|---|
| Analytica -- an experiment in combining theorem proving and symbolic computation | 2024-06-21 | Paper |
| Combining symbolic computation and theorem proving: Some problems of Ramanujan | 2020-01-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5227061 | 2019-08-05 | Paper |
| Introduction to Model Checking | 2018-07-20 | Paper |
| From non-preemptive to preemptive scheduling using synchronization synthesis | 2018-03-01 | Paper |
| SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems | 2017-05-19 | Paper |
| Delta-Decidability over the Reals | 2017-05-16 | Paper |
| Rare-event verification for stochastic hybrid systems | 2017-05-16 | Paper |
| Learning Probabilistic Systems from Tree Samples | 2017-05-16 | Paper |
| From non-preemptive to preemptive scheduling using synchronization synthesis | 2017-05-15 | Paper |
| Bayesian statistical model checking with application to Simulink/Stateflow verification | 2017-05-10 | Paper |
| Solving QBF with counterexample guided refinement | 2016-03-08 | Paper |
| $$2^5$$ Years of Model Checking | 2015-12-03 | Paper |
| Counterexample-guided abstraction refinement for symbolic model checking | 2015-11-12 | Paper |
| Bayesian statistical model checking with application to Stateflow/Simulink verification | 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 | 2013-08-12 | Paper |
| dReal: An SMT Solver for Nonlinear Theories over the Reals | 2013-06-14 | Paper |
| δ-Complete Decision Procedures for Satisfiability over the Reals | 2012-09-05 | Paper |
| Computational Modeling and Verification of Signaling Pathways in Cancer | 2012-06-08 | Paper |
| Statistical Model Checking for Cyber-Physical Systems | 2011-10-07 | Paper |
| Quantifier Elimination over Finite Fields Using Gröbner Bases | 2011-07-08 | Paper |
| Statistical Verification of Probabilistic Properties with Unbounded Until | 2011-05-12 | Paper |
| A Non-prenex, Non-clausal QBF Solver with Game-State Learning | 2010-09-29 | Paper |
| On simulation-based probabilistic model checking of mixed-analog circuits | 2010-09-16 | Paper |
| An Abstraction Technique for Real-Time Verification | 2010-06-02 | Paper |
| Computer Aided Verification | 2010-04-20 | Paper |
| Verification: Theory and Practice | 2010-03-23 | Paper |
| Correct Hardware Design and Verification Methods | 2010-02-05 | Paper |
| Computing differential invariants of hybrid systems as fixed points | 2009-11-23 | Paper |
| Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations | 2009-11-23 | Paper |
| Theory and Applications of Satisfiability Testing | 2009-07-24 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2009-05-15 | Paper |
| Integrated Formal Methods | 2009-05-07 | Paper |
| Learning Minimal Separating DFA’s for Compositional Verification | 2009-03-31 | Paper |
| The Image Computation Problem in Hybrid Systems Model Checking | 2009-03-11 | Paper |
| Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction | 2009-03-11 | Paper |
| Arithmetic Strengthening for Shape Analysis | 2009-03-03 | Paper |
| Model Checking – My 27-Year Quest to Overcome the State Explosion Problem | 2009-01-27 | Paper |
| Verification of Supervisory Control Software Using State Proximity and Merging | 2008-09-02 | Paper |
| Verification of evolving software via component substitutability analysis | 2008-07-30 | Paper |
| The Birth of Model Checking | 2008-07-15 | Paper |
| Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations | 2008-07-15 | Paper |
| Computing Differential Invariants of Hybrid Systems as Fixedpoints | 2008-07-15 | Paper |
| DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC | 2008-07-15 | Paper |
| Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems | 2008-04-11 | Paper |
| Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages | 2008-04-11 | Paper |
| State/Event Software Verification for Branching-Time Specifications | 2007-11-29 | Paper |
| SAT-Based Compositional Verification Using Lazy Learning | 2007-11-29 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2007-09-28 | Paper |
| Program Compatibility Approaches | 2007-09-11 | Paper |
| Satisfiability Checking of Non-clausal Formulas Using General Matings | 2007-09-04 | Paper |
| Verification of SpecC using predicate abstraction | 2007-06-21 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2007-05-02 | Paper |
| Verification, Model Checking, and Abstract Interpretation | 2007-02-12 | Paper |
| Concurrent software verification with states, events, and deadlocks | 2006-10-25 | Paper |
| Computer Aided Verification | 2006-01-10 | Paper |
| FM 2005: Formal Methods | 2006-01-10 | Paper |
| Hybrid Systems: Computation and Control | 2005-11-11 | Paper |
| Tools and Algorithms for the Construction and Analysis of Systems | 2005-11-10 | Paper |
| Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems | 2005-10-19 | Paper |
| An Iterative Framework for Simulation Conformance | 2005-10-18 | Paper |
| CONCUR 2004 - Concurrency Theory | 2005-08-23 | Paper |
| Predicate abstraction of ANSI-C programs using SAT | 2004-11-22 | Paper |
| Efficient verification of sequential and concurrent C programs | 2004-11-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4818818 | 2004-09-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4817533 | 2004-09-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4738460 | 2004-08-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4427894 | 2003-09-14 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4417923 | 2003-07-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4804909 | 2003-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4804901 | 2003-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4787240 | 2003-01-09 | Paper |
| Verification of out-of-order processor designs using model Checking and a light-weight completion function | 2002-07-08 | Paper |
| Bounded model checking using satisfiability solving | 2002-05-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754081 | 2001-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2754079 | 2001-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4518908 | 2001-08-05 | Paper |
| Model checking. | 2001-01-01 | Paper |
| The Verus language: Representing time efficiently with BDDs | 2000-12-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4494391 | 2000-12-11 | Paper |
| NuSMV: A new symbolic model checker | 2000-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4255570 | 1999-08-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4255551 | 1999-08-17 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4255565 | 1999-08-17 | Paper |
| Analytica --- an experiment in combining theorem proving and symbolic computation | 1999-06-29 | Paper |
| A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata | 1999-02-25 | Paper |
| Analysis and verification of real-time systems using quantitative symbolic algorithms | 1999-01-01 | Paper |
| State space reduction using partial order techniques | 1999-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4885884 | 1997-02-17 | Paper |
| A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems | 1993-06-29 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4037084 | 1993-05-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4027622 | 1993-02-21 | Paper |
| PARTHENON: A parallel theorem prover for non-horn clauses | 1992-09-27 | Paper |
| Symbolic model checking: \(10^{20}\) states and beyond | 1992-09-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3204066 | 1989-01-01 | Paper |
| Reasoning about networks with many identical finite state processes | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3204034 | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4733398 | 1989-01-01 | Paper |
| Reasoning about procedures as parameters in the language L4 | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4207567 | 1989-01-01 | Paper |
| Characterizing finite Kripke structures in propositional temporal logic | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3028984 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3743254 | 1987-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4721963 | 1986-01-01 | Paper |
| Automatic verification of finite-state concurrent systems using temporal logic specifications | 1986-01-01 | Paper |
| Automatic Verification of Sequential Circuits Using Temporal Logic | 1986-01-01 | Paper |
| The complexity of propositional linear temporal logics | 1985-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3704886 | 1985-01-01 | Paper |
| Hierarchical verification of asynchronous circuits using temporal logic | 1985-01-01 | Paper |
| Can message buffers be axiomatized in linear temporal logic? | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3326819 | 1984-01-01 | Paper |
| The characterization problem for Hoare logics | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3329397 | 1984-01-01 | Paper |
| Effective Axiomatizations of Hoare Logics | 1983-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3336675 | 1982-01-01 | Paper |
| Using branching time temporal logic to synthesize synchronization skeletons | 1982-01-01 | Paper |
| Task management in Ada—A critical evaluation for real-time multiprocessors | 1981-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3906386 | 1980-01-01 | Paper |
| Synthesis of Resource Invariants for Concurrent Programs | 1980-01-01 | Paper |
| Proving correctness of coroutines without history variables | 1980-01-01 | Paper |
| Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems | 1979-01-01 | Paper |
| Program invariants as fixedpoints | 1979-01-01 | Paper |
