Formalizing process algebraic verifications in the calculus of constructions

DOI10.1007/BF01212523zbMath0868.68078OpenAlexW2912259090MaRDI QIDQ1355748

Jan Friso Groote, Marc Bezem, Roland N. Bol

Publication date: 17 August 1997

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01212523

zbMATH Keywords

process algebraalternating bit protocolreal-life protocols

Mathematics Subject Classification ID

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

Uses Software

• Coq
• Automath

Cites Work

• Specification and compositional verification of real-time systems
• The calculus of constructions
• Type theory and concurrency
• Discrete time process algebra
• Proving Liveness Properties of Concurrent Programs
• Process Algebra
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item