A mechanically verified theory of contracts

DOI10.1007/978-3-030-85315-0_9OpenAlexW3193928150MaRDI QIDQ2119969

Jean-Pierre Talpin, Benoît Boyer, Stéphane Kastenbaum

Publication date: 31 March 2022

Full work available at URL: https://arxiv.org/abs/2108.13647

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Coq
• Isabelle/HOL
• KeYmaera
• Simulink
• KeYmaera X

Cites Work

• Differential dynamic logic for hybrid systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Taming Dr. Frankenstein: contract-based design for cyber-physical systems
• Unifying theories of reactive design contracts
• An Assume/Guarantee Based Compositional Calculus for Hybrid CSP
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• Multiple Viewpoint Contract-Based Specification and Design
• Change and Delay Contracts for Hybrid System Component Verification

This page was built for publication: A mechanically verified theory of contracts