A Coq Library for Verification of Concurrent Programs

DOI10.1016/j.entcs.2007.11.010zbMath1278.68152OpenAlexW2113275908MaRDI QIDQ2871836

Naoki Kobayashi, Reynald Affeldt

Publication date: 10 January 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.11.010

zbMATH Keywords

concurrent programsproof assistantpi-calculusCoq

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)

Related Items (6)

Implementation of a reversible distributed calculus ⋮ An extensible approach to session polymorphism ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ The GDML and EuKIM Projects: Short Report on the Initiative ⋮ A Coq Library for Verification of Concurrent Programs ⋮ \( \pi\) with leftovers: a mechanisation in Agda

Uses Software

• Coq
• Isabelle/HOL
• Why3
• HOL
• Pict

Cites Work

• A calculus of mobile processes. II
• \(\pi\)-calculus in (Co)inductive-type theory
• On the desirability of mechanizing calculational proofs
• A type system for lock-free processes
• A Coq Library for Verification of Concurrent Programs
• An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
• Formal Verification of an Incremental Garbage Collector
• Anytime, anywhere
• Mobile values, new names, and secure communication
• Types for Proofs and Programs
• Formal Methods at the Crossroads. From Panacea to Foundational Support
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Coq Library for Verification of Concurrent Programs