Combining theorem proving and model checking through symbolic analysis

DOI10.1007/3-540-44618-4_1MaRDI QIDQ4536588zbMATH OpenFDO

Authors Natarajan Shankar

Publication date 28 November 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44618-4_1

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Combinations of model checking and theorem proving
• Symbolic analysis of transition systems
• Programming a symbolic model checker in a fully expansive theorem prover
• Combining Model Checking and Deduction
• Explicit-symbolic modelling for formal verification

Cited in

(11)

• Tool support for learning Büchi automata and linear temporal logic
• Symbolic analysis of transition systems
• Explicit-symbolic modelling for formal verification
• Combining Model Checking and Deduction
• Symbolic Protocol Analysis with Disequality Constraints Modulo Equational Theories
• Verifying Reference Counting Implementations
• Combinations of model checking and theorem proving
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving
• First order Büchi automata and their application to verification of LTL specifications
• Providing a formal linkage between MDG and HOL

Describes a project that uses

Uses Software

• PVS
• Cadence SMV
• HOL

This page was built for publication: Combining theorem proving and model checking through symbolic analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4536588)