Combining Model Checking and Deduction
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3757688 (Why is no real title available?)
- scientific article; zbMATH DE number 52331 (Why is no real title available?)
- scientific article; zbMATH DE number 52516 (Why is no real title available?)
- scientific article; zbMATH DE number 1254648 (Why is no real title available?)
- scientific article; zbMATH DE number 2161330 (Why is no real title available?)
- scientific article; zbMATH DE number 194539 (Why is no real title available?)
- scientific article; zbMATH DE number 3999882 (Why is no real title available?)
- scientific article; zbMATH DE number 2102725 (Why is no real title available?)
- scientific article; zbMATH DE number 7088727 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 5194318 (Why is no real title available?)
- scientific article; zbMATH DE number 3299649 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- scientific article; zbMATH DE number 3322506 (Why is no real title available?)
- scientific article; zbMATH DE number 965572 (Why is no real title available?)
- A theory of timed automata
- Abstraction and abstraction refinement
- Algebraic laws for nondeterminism and concurrency
- An Early Program Proof by Alan Turing
- An axiomatic basis for computer programming
- Automated deduction for verification
- BDD-based symbolic model checking
- Binary decision diagrams
- Combining model checking and testing
- Computational Complexity
- Computer Aided Verification
- Explicit-state model checking
- Finiteness is mu-ineffable
- First-order dynamic logic
- Graph Games and Reactive Synthesis
- Handbook of mathematical logic. With the cooperation of H. J. Keisler, K. Kunen, Y. N. Moschovakis, A. S. Troelstra. 2nd printing
- Handbook of model checking
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Interpolation and model checking
- Isabelle/HOL. A proof assistant for higher-order logic
- Low-level liquid types
- Modal logic
- Model Checking Real-Time Systems
- Model checking parameterized systems
- Myths about the mutual exclusion problem
- Predicate abstraction for program verification
- Propositional SAT solving
- SAT-Based Model Checking
- SAT-Based Model Checking without Unrolling
- Satisfiability modulo theories
- Simplification by Cooperating Decision Procedures
- Soundness and Completeness of an Axiom System for Program Verification
- Symbolic model checking in non-Boolean domains
- Symbolic optimization with SMT solvers
- Temporal logic and fair discrete systems
- Ten Years of Hoare's Logic: A Survey—Part I
- The mu-calculus and Model Checking
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Understanding IC3
- Using branching time temporal logic to synthesize synchronization skeletons
- Verification of Hybrid Systems
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
Cited in
(7)- Interpolation and model checking
- scientific article; zbMATH DE number 1538014 (Why is no real title available?)
- scientific article; zbMATH DE number 1759597 (Why is no real title available?)
- Temporal logic and fair discrete systems
- Modular analysis of distributed hybrid systems using post-regions
- Combining termination proofs in model transformation systems
- Practical abstractions for automated verification of message passing concurrency
This page was built for publication: Combining Model Checking and Deduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176378)
