scientific article; zbMATH DE number 177240

MaRDI QIDQ4037091zbMATH OpenFDO

Authors Olivier Coudert, Jean Christophe Madre, Christian Berthet

Publication date 18 May 1993

zbMATH Keywords

behavioral equivalenceBoolean functiontemporal logictyped decision graphsverification algorithmverification of sequential machines

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 177500
• scientific article; zbMATH DE number 177519
• Automatic Verification of Sequential Circuits Using Temporal Logic
• scientific article; zbMATH DE number 3932379
• Automatic verification of finite-state concurrent systems using temporal logic specifications

Cited in

(13)

• An experience in proving regular networks of processes by modular model checking
• On the complexity of analysis and manipulation of Boolean functions in terms of decision graphs
• Structuring and automating hardware proofs in a higher-order theorem- proving environment
• The temporal boolean derivative applied to verification of extended finite state machines
• The Birth of Model Checking
• scientific article; zbMATH DE number 4035144 (Why is no real title available?)
• scientific article; zbMATH DE number 139803 (Why is no real title available?)
• scientific article; zbMATH DE number 177500 (Why is no real title available?)
• Proof tactics for a theory of state machines in a graphical environment
• Vectorized symbolic model checking of computation tree logic for sequential machine verification
• Functional extension of symbolic model checking
• Comparing generic state machines
• Automated temporal reasoning about reactive systems

This page was built for publication:

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