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

DOI10.1016/J.IPL.2016.02.001zbMATH Open1356.68177OpenAlexW2258230469MaRDI QIDQ264193FDOQ264193

Authors: 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

Recommendations

• scientific article; zbMATH DE number 1746646
• Bellerophon: tactical theorem proving for hybrid systems
• A light-weight integration of automated and interactive theorem proving
• Numerically-aided deductive safety proof for a powertrain control system
• Interactive theorem proving with temporal logic

zbMATH Keywords

verificationnonlinear controlformal methodsprototype verification systemtheorem proving

Mathematics Subject Classification ID

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

Cites Work

• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Untersuchungen über das logische Schliessen. I
• Modelling of Complex Systems: Systems as Dataflow Machines
• Isabelle/HOL. A proof assistant for higher-order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modeling and simulation in Scilab/Scicos with ScicosLab 4.4
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Simulation of ODE/PDE models with MATLAB, OCTAVE and SCILAB. Scientific and engineering applications
• Hybrid Systems: Computation and Control
• Assume-guarantee verification of nonlinear hybrid systems with ARIADNE

Cited In (6)

• Applications of real number theorem proving in PVS
• A light-weight integration of automated and interactive theorem proving
• Numerically-aided deductive safety proof for a powertrain control system
• Theorem-proving analysis of digital control logic interacting with continuous dynamics
• Bellerophon: tactical theorem proving for hybrid systems
• 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

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

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