Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system

DOI10.1016/J.IPL.2016.02.001zbMath1356.68177OpenAlexW2258230469MaRDI QIDQ264193

Cinzia Bernardeschi, Andrea Domenici

Publication date: 6 April 2016

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11568/776232

zbMATH Keywords

verificationnonlinear controltheorem provingformal methodsprototype verification system

Mathematics Subject Classification ID

Nonlinear systems in control theory (93C10) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Related Items (1)

Verifying a scheduling protocol of safety-critical systems

Uses Software

• Coq
• Isabelle/HOL
• Scicos
• PVS
• KeYmaera
• NuSMV
• RSOLVER
• Benchmarks
• Uppaal
• ScicosLab
• HSolver
• HybridSal
• PVSio-web
• Manip

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Untersuchungen über das logische Schliessen. I
• Modeling and Simulation in Scilab/Scicos with ScicosLab 4.4
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Modelling of Complex Systems: Systems as Dataflow Machines
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Simulation of ODE/PDE Models with MATLAB®, OCTAVE and SCILAB
• Hybrid Systems: Computation and Control
• Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp>

This page was built for publication: Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system