scientific article; zbMATH DE number 177240

MaRDI QIDQ4037091zbMATH OpenFDO

Authors Olivier Coudert, Jean Christophe Madre, Christian Berthet

Publication date 18 May 1993

zbMATH Keywords

Boolean functiontemporal logicbehavioral equivalenceverification algorithmtyped decision graphsverification 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)

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

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)