A Hoare logic for linear systems

DOI10.1007/S00165-011-0180-9MaRDI QIDQ469998zbMATHOpenAlexDBLPWikidataFDO

Authors Rob Arthan, Paulo Oliva, Ursula Martin Webb

Publication date 11 November 2014

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-011-0180-9

zbMATH Keywords

linear systemscontrol systemsHoare logicformal verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Linear systems in control theory (93C05)

Recommendations

• Hoare Logic in the Abstract
• Hybrid diagrams
• Differential Logic for Reasoning About Hybrid Systems
• The calculus of signal flow diagrams. I: Linear relations on streams.
• scientific article; zbMATH DE number 1956625

Cites work

• scientific article; zbMATH DE number 3514020 (Why is no real title available?)
• scientific article; zbMATH DE number 1182386 (Why is no real title available?)
• scientific article; zbMATH DE number 1956625 (Why is no real title available?)
• scientific article; zbMATH DE number 233974 (Why is no real title available?)
• A general framework for sound and complete Floyd-Hoare logics
• A tutorial on coinductive stream calculus and signal flow graphs
• An axiomatic basis for computer programming
• Computer Science Logic
• FM 2005: Formal Methods
• Formal methods for industrial applications. Specification and programming the Steam Boiler Control
• Hidden verification for computational mathematics
• Hoare Logic in the Abstract
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Traced monoidal categories

Cited in

(8)

• scientific article; zbMATH DE number 1956625 (Why is no real title available?)
• Refinement for signal flow graphs
• Graphical piecewise-linear algebra
• Fifty years of Hoare's logic
• A UTP approach for rTiMo
• scientific article; zbMATH DE number 1980939 (Why is no real title available?)
• Formalization of linear space theory in the higher-order logic proving system
• Mechanically proving determinacy of hierarchical block diagram translations

Describes a project that uses

Uses Software

• SPIN
• ClawZ
• Circus

This page was built for publication: A Hoare logic for linear systems

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