From model checking to a temporal proof

DOI10.1007/3-540-45139-0_1MaRDI QIDQ4531749zbMATH OpenFDO

Authors Doron Peled, Lenore D. Zuck

Publication date 23 May 2002

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2057/20570001

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2081113
• Certifying model checkers
• scientific article; zbMATH DE number 910719
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• scientific article; zbMATH DE number 3932379

Cited in

(20)

• Certifying proofs for SAT-based model checking
• TOrPEDO : witnessing model correctness with topological proofs
• From complementation to certification
• Simplification of proof procedures based on the path condition concepts
• Induction in compositional model checking
• Model-checking the preservation of temporal properties upon feature integration
• scientific article; zbMATH DE number 6117314 (Why is no real title available?)
• Lifting temporal proofs through abstractions
• scientific article; zbMATH DE number 2081113 (Why is no real title available?)
• RTDT: A front-end for efficient model checking of synchronous timing diagrams
• Evidence-based model checking
• An Experimental Spatio-Temporal Model Checker
• A proof theory for model checking: an extended abstract
• Integrating topological proofs with model checking to instrument iterative design
• Proving the refuted: symbolic model checkers as proof generators
• From Model Checking to a Temporal Proof for Partial Models
• The Power of Proofs: New Algorithms for Timed Automata Model Checking
• Decidability of model checking with the temporal logic EF
• Optimal proofs for linear temporal logic on lasso words
• Certifying rlive: a new proof strategy for liveness model checking

This page was built for publication: From model checking to a temporal proof

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