Linking theorem proving and model-checking with well-founded bisimulation

DOI10.1007/3-540-48683-6_32MaRDI QIDQ4818805zbMATH OpenFDO

Authors Panagiotis Manolios, Kedar S. Namjoshi, Robert Summers

Publication date 24 September 2004

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

Full work available at URL https://doi.org/10.1007/3-540-48683-6_32

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

• Proof-checking protocols using bisimulations
• scientific article; zbMATH DE number 4022620
• A compositional protocol verification using relativized bisimulation
• scientific article; zbMATH DE number 3958712
• Programming a symbolic model checker in a fully expansive theorem prover

Cited in

(3)

• Specification and verification of concurrent programs through refinements
• Proof-checking protocols using bisimulations
• Ordinal arithmetic: Algorithms and mechanization

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Linking theorem proving and model-checking with well-founded bisimulation

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