Mechanizing a process algebra for network protocols
From MaRDI portal
Publication:287372
DOI10.1007/s10817-015-9358-9zbMath1356.68182arXiv1512.07304OpenAlexW2297246203MaRDI QIDQ287372
Peter Höfner, Timothy Bourke, Robert J. van Glabbeek
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1512.07304
process algebramobile ad hoc networksIsabelle/HOLinteractive theorem provingcompositional invariant proofswireless mesh networks
Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12)
Related Items
Depletable channels: dynamics, behaviour, and efficiency in network design ⋮ Analysing AWN-Specifications Using mCRL2 (Extended Abstract)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A framework for security analysis of mobile wireless networks
- A process calculus for mobile ad hoc networks
- An observational theory for mobile ad hoc networks (full version)
- Isabelle/HOL. A proof assistant for higher-order logic
- A structural approach to operational semantics
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Showing Invariance Compositionally for a Process Algebra for Network Protocols
- A Process Algebra for Wireless Mesh Networks
- Isabelle/jEdit – A Prover IDE within the PIDE Framework
- A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol
- Temporal Verification of Reactive Systems: Response
- A Calculus for Mobile Ad Hoc Networks
- Extending Sledgehammer with SMT Solvers
- Shared-Memory Multiprocessing for Interactive Theorem Proving
- Psi-calculi in Isabelle
