Formalizing process algebraic verifications in the calculus of constructions

DOI10.1007/BF01212523MaRDI QIDQ1355748zbMATH OpenOpenAlexFDO

Authors Marc Bezem, Jan Friso Groote, 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, https://research.tue.nl/nl/publications/52bd5fad-1231-4713-8986-40223cd5ef9e

zbMATH Keywords

alternating bit protocolprocess algebrareal-life protocols

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 683368
• scientific article; zbMATH DE number 3958712
• A full formalisation of -calculus theory in the calculus of constructions

Cites work

• A computer-checked verification of Milner's scheduler
• Discrete time process algebra
• scientific article; zbMATH DE number 4016181 (Why is no real title available?)
• scientific article; zbMATH DE number 3958712 (Why is no real title available?)
• scientific article; zbMATH DE number 4084989 (Why is no real title available?)
• scientific article; zbMATH DE number 3755842 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 683368 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Process Algebra
• Proving Liveness Properties of Concurrent Programs
• Specification and compositional verification of real-time systems
• The calculus of constructions
• Type theory and concurrency

Cited in

(12)

• Focus points and convergent process operators: A proof strategy for protocol verification
• Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
• HOCore in Coq
• scientific article; zbMATH DE number 683363 (Why is no real title available?)
• scientific article; zbMATH DE number 683368 (Why is no real title available?)
• scientific article; zbMATH DE number 1962750 (Why is no real title available?)
• Proving correctness of labeled transition systems by semantic tableaux
• An application of co-inductive types in Coq: verification of the alternating bit protocol
• Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
• scientific article; zbMATH DE number 5181778 (Why is no real title available?)
• A functional programming approach to the specification and verification of concurrent systems
• A refinement calculus for specifications in Hennessy-Milner logic with recursion

Describes a project that uses

Uses Software

• Coq
• Automath

This page was built for publication: Formalizing process algebraic verifications in the calculus of constructions

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