Theorem-proving analysis of digital control logic interacting with continuous dynamics

DOI10.1016/j.entcs.2015.10.008zbMath1351.68249OpenAlexW2252122258WikidataQ113317762 ScholiaQ113317762MaRDI QIDQ2520681

Jackson R. Mayo, Robert C. Armstrong, Geoffrey C. Hulette, Joseph R. Ruthruff

Publication date: 16 December 2016

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

zbMATH Keywords

hybrid systemstheorem provingformal methodscyber-physical systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Thermodynamics and heat transfer (80A99) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Uses Software

• Coq
• KeYmaera

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Buridan's principle
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives

This page was built for publication: Theorem-proving analysis of digital control logic interacting with continuous dynamics