Proving the Correctness of the Implementation of a Control-Command Algorithm

DOI10.1007/978-3-642-03237-0_9zbMath1248.68139OpenAlexW1490299611MaRDI QIDQ3392923

Olivier Bouissou

Publication date: 18 August 2009

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03237-0_9

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• PHAVer
• HyTech
• ASTREE
• GRKLib

Cites Work

• Switching in systems and control
• Validated solutions of initial value problems for ordinary differential equations
• Proving that programs eventually do something good
• Proving non-termination
• Zonotope/Hyperplane Intersection for Hybrid Systems Reachability Analysis
• Reachability of Uncertain Nonlinear Systems Using a Nonlinear Hybridization
• Static Analysis in Disjunctive Numerical Domains
• Static Analysis of Numerical Algorithms
• Periodically Controlled Hybrid Systems
• Uniform Stability of Switched Linear Systems: Extensions of LaSalle's Invariance Principle
• Abstract Interpretation Frameworks
• Hybrid Systems: Computation and Control
• Hybrid Systems: Computation and Control
• Numerical Software with Result Verification
• Abstract Interpretation of the Physical Inputs of Embedded Programs
• A Hybrid Denotational Semantics for Hybrid Systems
• Hybrid Systems: Computation and Control
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proving the Correctness of the Implementation of a Control-Command Algorithm