Combining Model Checking and Deduction
From MaRDI portal
Publication:3176378
DOI10.1007/978-3-319-10575-8_20zbMath1392.68265OpenAlexW2804061523MaRDI QIDQ3176378
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_20
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Using branching time temporal logic to synthesize synchronization skeletons
- Handbook of mathematical logic. With the cooperation of H. J. Keisler, K. Kunen, Y. N. Moschovakis, A. S. Troelstra. 2nd printing
- Myths about the mutual exclusion problem
- Finiteness is mu-ineffable
- First-order dynamic logic
- A theory of timed automata
- Isabelle/HOL. A proof assistant for higher-order logic
- Understanding IC3
- SAT-Based Model Checking without Unrolling
- Temporal Logic and Fair Discrete Systems
- Explicit-State Model Checking
- Binary Decision Diagrams
- BDD-Based Symbolic Model Checking
- Propositional SAT Solving
- SAT-Based Model Checking
- Satisfiability Modulo Theories
- Abstraction and Abstraction Refinement
- Interpolation and Model Checking
- Predicate Abstraction for Program Verification
- Combining Model Checking and Testing
- Model Checking Parameterized Systems
- The mu-calculus and Model Checking
- Graph Games and Reactive Synthesis
- Model Checking Real-Time Systems
- Verification of Hybrid Systems
- Symbolic Model Checking in Non-Boolean Domains
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Algebraic laws for nondeterminism and concurrency
- Simplification by Cooperating Decision Procedures
- Ten Years of Hoare's Logic: A Survey—Part I
- Soundness and Completeness of an Axiom System for Program Verification
- Handbook of Model Checking
- An Early Program Proof by Alan Turing
- Automated deduction for verification
- Low-level liquid types
- Computer Aided Verification
- Computational Complexity
- Symbolic optimization with SMT solvers
- An axiomatic basis for computer programming
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Combining Model Checking and Deduction
