We present VeriPhy, a verified pipeline which automatically transforms verified high-level
models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to …

This article answers fundamental safety questions for ground robot navigation: under which
circumstances does which control decision make a ground robot safely avoid obstacles …

Hybrid systems combine discrete and continuous dynamics, which makes them attractive as
models for systems that combine computer control with physical motion. Verification is …

This article proves the completeness of an axiomatization for differential equation invariants
described by Noetherian functions. First, the differential equation axioms of differential …

We prove the completeness of an axiomatization for differential equation invariants. First, we
show that the differential equation axioms in differential dynamic logic are complete for all …

We present simple new Hoare logics and refinement calculi for hybrid systems in the style of
differential dynamic logic.(Refinement) Kleene algebra with tests is used for reasoning about …

We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof
assistant by an algebraic model for hybrid program stores, a shallow expression model for …

Differential dynamic logic (dL) is a formal framework for specifying and reasoning about
hybrid systems, ie, dynamical systems that exhibit both continuous and discrete behaviors …

Numerical errors are insidious, difficult to predict and inherent in different levels of critical
systems design. Indeed, numerical algorithms generally constitute approximations of an …

We present a tool for verification of hybrid systems expressed in the sequential fragment of
HCSP (Hybrid Communicating Sequential Processes). The tool permits annotating HCSP …