key: cord-0060809-pkv60tvs
authors: Foster, Simon; Huerta y Munive, Jonathan Julián; Struth, Georg
title: Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
date: 2020-04-01
journal: Relational and Algebraic Methods in Computer Science
DOI: 10.1007/978-3-030-43520-2_11
sha: b262153b5989e1c543d9c87d123de938b772670d
doc_id: 60809
cord_uid: pkv60tvs

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 the program structure and generating verification conditions at this level. Lenses capture hybrid program stores in a generic algebraic way. The approach has been formalised with the Isabelle/HOL proof assistant. Several examples explain the workflow with the resulting verification components.

Differential dynamic logic (dL) is a prominent deductive method for verifying hybrid systems [26] . It extends dynamic logic with specific inference rules for reasoning about the discrete control and continuous dynamics that characterise such systems. Continuous evolutions are modelled by dL's evolution commands within a hybrid program syntax. These declare a vector field and a guard, which is meant to hold along the evolution. Reasoning with evolution commands in dL requires either explicit solutions to differential equations represented by the vector field, or invariant sets [28] that describe these evolutions implicitly. Verification components inspired by dL have already been formalised in the Isabelle proof assistant [16] . Yet the shallow embedding used in this work has shifted the focus from the original proof-theoretic approach to a semantic one, and ultimately to predicate transformer algebras supporting a different workflow.

Dynamic logics and predicate transformers are powerful tools. They support reasoning about program equivalences and transformations far beyond what standard program verification requires [4] . For the latter, much simpler Hoare logics generate precisely the verification conditions needed. Asking about the feasibility of a differential Hoare logic (dH) is therefore natural. As Hoare logic is strongly related to Morgan's refinement calculus [25] , it is equally reasonable to ask whether and how a Morgan-style differential refinement calculus (dR) might allow constructing hybrid programs from specifications.

A prima facie answer to these questions seems positive: after all, the laws of Morgan's refinement calculus can be proved using the rules of Hoare logic, which in turn are derivable within dynamic logic. But the formalisms envisaged might not be expressive enough for hybrid program verification or less suitable than dL in practice. Conceptually it is also not obvious what exactly it would take to extend a standard Hoare logic or refinement calculus to hybrid programs.

Our main contribution consists in evidence that dH and dR are as applicable for verifying simple hybrid programs as dL, and that developing these methods requires simply adding a single Hoare-style axiom and a single refinement rule for evolution commands to the standard formalisms.

This conceptual simplicity is reflected in the Isabelle verification components for dH and dR. These reuse components for (refinement) Kleene algebra with tests [3, 13, 19] ((r)KAT) for the propositional Hoare logic and refinement calculi, ignoring assignment and evolution commands. The axioms and laws for these basic commands are derived in a concrete state transformer semantics for hybrid programs [15] over a generic hybrid store model based on lenses [10] , reusing other Isabelle components [8, 9, 15] . Data-level verification conditions are discharged using Isabelle's impressive components for ordinary differential equations [17] .

This simple modular development evidences the benefits of algebraic reasoning and shallow embeddings with proof assistants. Our verification components merely require formalising a state transformer semantics for KAT and rKAT along the lines of [16] and concrete store semantics for hybrid programs. Lenses [10] give us the flexibility to switch seamlessly between stores based on real vector spaces or executable Euclidean spaces. Beyond that it suffices to derive a few algebraic laws for invariants and the Hoare-axioms and refinement laws for evolution commands in the concrete semantics. Program verification is then performed at the concrete level, but this remains hidden, as tactics generate data-level verification conditions automatically and we have programmed boiler-plate syntax for programs and correctness specifications.

Our Isabelle components support the workflows of dL in dH and dR. We may reason explicitly with solutions to differential equations and implicitly with invariant sets. We have formalised a third method in which solutions, that is flows, are declared ab initio in correctness specifications and need not be certified.

Our program construction and verification components have so far been evaluated on a small set of simple examples. Further work is needed to evidence scalability or compare performance with the standard dL tool chain. We present some examples to explain the work flows supported by dH and dR. With Isabelle tactics for automated verification condition generation in place, we notice little difference relative to our predicate transformer components [16] . The entire Isabelle formalisation is available online 1 .

A Kleene algebra with tests [19] (KAT) is a structure (K, B, +, ·, 0, 1, * , ¬) where (B, +, ·, 0, 1, ¬) is a boolean algebra with join +, meet ·, complementation ¬, least element 0 and greatest element 1, B ⊆ K, and (K, +, ·, 0, 1, * ) is a Kleene algebra-a semiring with idempotent addition equipped with a star operation that satisfies the axioms 1 + α · α * ≤ α * and γ + α · β ≤ β → α * · γ ≤ β, as well as their opposities, with multiplication swapped. The ordering on K is defined by α ≤ β ↔ α + β = β, as idempotent semirings are semilattices.

Elements of K represent programs; those of B tests, assertions or propositions. The operation · models the sequential composition of programs 2 , + their nondeterministic choice, (−) * their finite unbounded iteration. Program 0 aborts and 1 skips. Tests are embedded implicitly into programs. They are meant to hold in some states of a program and fail in others; pα (αp) restricts the execution of program α in its input (output) to those states where test p holds. The ordering ≤ is the opposite of the refinement ordering on programs (see Sect. 7).

Binary relations of type P (S × S) form KATs [19] when · is interpreted as relational composition, + as relational union, (−) * as reflexive-transitive closure and the elements of B as subidentities-relations below the relational unit. This grounds KAT within standard relational imperative program semantics. However, we prefer the isomorphic representation known as state transformers of type S → P S. Composition · is then interpreted as Kleisli composition

where the order on functions has been extended pointwise, and complementation is given by

We freely identify predicates, sets and state transformers below η S , which are isomorphic: P ∼ = {s | P s} ∼ = λs. {x | x = s ∧ P s}. A state transformer KAT over S is any subalgebra of Sta S. KAT has been formalised via type classes in Isabelle [2] . As these allow only one type parameter, we use an alternative to the standard two-sorted approach that expands a Kleene algebra K by an antitest function n : K → K from which a test function t : K → K is defined as t = n • n. Then K t = {α | t α = α} forms a boolean algebra in which n yields test complementation. It can be used in place of B. The state transformer KAT has been formalised for this article.

KAT provides a simple algebraic semantics for while programs with if p then α else β = p · α + ¬p · β and while p do α = (p · α) * · ¬p.

It captures validity of Hoare triples in a partial correctness semantics as

or equivalently by p · α ≤ α · q or p · α = p · α · q. It also allows deriving the rules of propositional Hoare logic [20] -disregarding assignments-which are useful for verification condition generation:

(h-while)

Rules for commands with invariant assertions α inv i are derivable in KAT, too (operationally, α inv i = α). An invariant for α ∈ K is a test i ∈ B satisfying {i} α {i}. Then, with loop α as syntactic sugar for α * , we obtain

We use (h-inv) for invariants for continuous evolutions of hybrid systems in Sects. 6, 7 and 8. The rules (h-inv-mult) and (h-inv-plus) are part of a procedure, described in Sect. 6. Rule (h-while-inv) is standard for invariants for while loops; (h-loop-inv) is specific to loops of hybrid programs (see Sect. 4). The rules for propositional Hoare logic in Isabelle have already been derived for KAT [2, 13] , those for invariants have been formalised for this work. By Proposition 2.1, all of them hold in particular in the state transformer semantics. We have formalised this fact with Isabelle. At this stage, verification condition rules for the basic commands for assignments and evolution commands are still missing. These are formalised within the concrete state transformer semantics (see Sect. 5).

Hybrid programs of differential dynamic logic (dL) [26] are defined by the syntax

that adds evolution commands x = f & G to the language of KAT-function ?(−) embeds tests explicitly into programs; in the tradition of KAT we leave this embedding implicit. Evolution commands introduce a time independent vector field f : S → S for an autonomous system of ordinary differential equations (ODEs) [28] together with a guard G, a predicate modelling boundary conditions or similar restrictions that hold along temporal evolutions. Guards are also known as evolution domain restrictions [6] .

Formally, we fix a state space S of the hybrid program such as S ⊆ R n for n ∈ N. We model continuous variables algebraically with lenses [10] to support different state space models generically. A lens x : A =⇒ S is a tuple x = (A, S, get, put), where A is a variable type. The functions get x : S → A and put x : S → A → S query and update the value of x in a particular state. They are linked by three intuitive algebraic laws [10] . For all s ∈ S and v, v ∈ A,

The predicate x y checks independence of lenses x and y, which holds when x and y refer to two different regions of S. As each program variable is a lens x : R =⇒ S, state spaces S ⊆ R n require n independent lenses x 1 · · · x n . Yet more general state spaces such as vector spaces are supported as well.

Systems of ODEs are modelled using vector fields: functions of type S → S on some open set S. Geometrically, vector field f assigns vectors to each point of the state space S. A solution to the initial value problem (IVP) for the pair (f, s) and initial value (0, s) ∈ T × S, where T is an open interval in R containing 0, is then a function X : T → S that satisfies X t = f (X t)-an autonomous system of ODEs in vector form-and X 0 = s. Solution X is thus a curve in S through s, parametrised by T and tangential to f at any point in S; it is called the trajectory or integral curve of f at s whenever it is uniquely defined [28] .

For IVP (f, s) with continuous vector field f : S → S and initial state s ∈ S we define the set of solutions on T as

Each solution X is thus continuously differentiable and hence f • X integrable in T . For X ∈ Sols f T s and guard G : S → B, we then define the G-guarded orbit of X along T in s [16] as a state transformer γ X G : S → P S by

where ↓t = {t ∈ T | t ≤ t}. Intuitively, γ X G s is the orbit at s defined along the longest interval in T that satisfies guard G. We also define the G-guarded orbital of f along T in s [16] via the state transformer γ f G : S → P S as

In applications, ↓t is usually an interval [0, t] ⊆ T . Expanding definitions,

If denotes the predicate that holds of all states in S (or the set S itself), we write γ f instead of γ f . We define the semantics of the evolution command x = f & G [16] for any continuous f : S → S and G : S → B as

In the evolution command x = f & G, x is part of the traditional syntax used for specifying systems of ODEs, while de facto only a vector field f is specified. This explains why x does not appear in the right-hand side of (st-evl). Defining the state transformer semantics of assignments is standard [16] , though we generalise using lenses. First, we use lenses to define state updates:

for x : A =⇒ S, e : S → A, and σ : S → S. Intuitively, this updates the value of variable x in σ : S → S to the value given by "expression" e in state s. For variables x and y, for example, the expression x/(2 + y) is modelled by λs. get x s / (2 + get y s). We can also update n variables simultaneously:

where id is the identity function. State updates commute when assigning to independent lenses; they cancel one another out, when made to the same lens. We can then define a semantic analog of the substitution operator e[f/x] = e • [x → f ] that satisfies the standard laws [10] . Finally, we define the generalised simultaneous assignment operator

(st-assgn) that applies σ : S → S as an assignment. With our state update function, singleton assignment is a special case: (x := e) = x → e . These concepts allow us to derive standard laws for assignments, as for instance in schematic KAT [1] :

Here, x e means that the semantic expression e does not depend in its valuation on lens x [10] . An assignment of x to itself is simply skip. Two assignments to x result in a single assignment, with a semantic substitution applied.

Assignments to independent variables x and y commute provided that neither assigned expression depends on the corresponding variable. Assignment can be distributed through conditionals by a substitution to the condition. Such laws can be applied recursively for symbolic evaluation of hybrid programs.

Lenses support various store models, including records and functions [10] . We provide models for vector spaces, executable and infinite Euclidean spaces:

The vector lens selects the kth element of an n dimension vector using vec-nth and vec-upd from the HOL Analysis library [14] , which provides an indexed type for the space R n . The Euclidean lens uses executable Euclidean spaces [18] that provide a list representation of the vectors in the n-dimensional V via an ordered basis and an inner product. The function lens selects range elements of a function associated with a domain element i ∈ A. It can be used in particular with infinite Euclidean spaces, N → R. All three satisfy the lens axioms above. The development in this section has been formalised with Isabelle [8, 9, 15] , both for a state transformer and a relational semantics. An instance of the latter for particular vector fields with unique solutions forms the standard semantics of dL. By the direct connection to orbits or orbitals, the state transformer semantics is arguably conceptually simpler and more elegant.

In the state transformer semantics of Hoare triples, the Kleisli composition in the left-hand side of p · α ≤ α · q ensures that p holds before executing α. The right-hand side guarantees that q holds after its execution. Specifically for evolution commands, and consistently with dL, q holds along the entire orbit of a solution for f . We now complete the derivation of inference rules of dH by adding Hoare-style rules for assignments and evolution commands in the concrete state transformer semantics.

The assignment axiom of Hoare logic needs no explanation. Our concrete state transformer semantics allows us to derive it:

(h-assgn)

Hence all we need to add to Hoare logic is a rule for evolution commands. We restrict our attention to Lipschitz-continuous vector fields for which unique solutions to IVPs are guaranteed by Picard-Lindelöf's theorem [28] . These are (local) flows ϕ : T → S → S and X = ϕ s = λt. ϕ t s is the trajectory at s. Guarded orbitals γ f G then specialise to guarded orbits

where T is fixed by the Picard-Lindelöf theorem and U ⊆ T is a time domain of interest, typically an interval [0, t] for some t ∈ T [16] where, by contrast to the previous section ↓t = {t ∈ U | t ≤ t} is relativised to U . This gives us the flexibility to consider dynamics over closed time intervals and it allows us to focus on time intervals and IVPs starting at t = 0. Accordingly, (st-evl) specialises to the following state transformer semantics for evolution commands.

(

The following Hoare-style rule for evolution commands is then derivable. 

This finishes the derivation of rules for a Hoare logic dH for hybrid programs-to our knowledge, the first Hoare logic of this kind. As usual, there is one rule per programming construct, so that the recursive application of theh-assgnHoare logic together with (h-assgn) and (h-evl) generates proof obligations that are entirely about data-level relationships-the discrete and continuous evolution of hybrid program stores.

The rule (h-evl) supports the following procedure for reasoning with an evolution command x = f & G and set U in dH: 

A thermostat regulates the temperature T of a room between bounds T l ≤ T ≤ T h . Variable T 0 stores an initial temperature; ϑ indicates whether the heater is switched on or off. Within time intervals of at most τ minutes, the thermostat resets time to 0, measures the temperature, and turns the heater on or off dependent on the value obtained.

The notation x → s f x indicates that vector field f a c maps variable x to f x for x ∈ {T, T 0 , ϑ, t}. Working with vec-lens n k or eucl-lens n k , we write ; instead of · and use guard G to restrict evolutions between T l and T h by setting

The hybrid program therm below models the behaviour of the thermostat. To simplify notation, we separate into a loop invariant (I), discrete control (ctrl), and continuous dynamics (dyn).

abbreviation ctrl T l T h ≡ (t ::= 0 ); (T0 ::= T );

The correctness specification and verification of the thermostat with dH is then lemma thermostat-flow : assumes 0 < a and 0 ≤ τ and 0 < T l and T h < Tu

prefer 4 prefer 8 using local-flow-therm assms apply force+ using assms therm-dyn-up therm-dyn-down by rel-auto

The first line uses tactic hyb-hoare to blast away the structure of therm using dH.

To apply hyb-hoare, the program must be an iteration of the composition of two programs-usually control and dynamics. The tactic requires lifting the store to an Isabelle/UTP expression [10] , which is denoted by the U operator. Lemma local-flow-therm, whose proof captures the procedure described above, supplies the flow for f a c: ϕ a c τ = (−e −a·τ (c − T ) + c, τ + t, T 0 , ϑ) , for all τ ∈ R. The remaining proof obligations are inequalities of transcendental functions. They are discharged automatically using auxiliary lemmas.

Alternatively, dH supports reasoning with invariants for evolution commands instead of supplying flows to (h-evl). The approach has been developed in [16] . Our invariants generalise the differential invariants of dL [26] and the invariant sets of dynamical systems and (semi)group theory [28] . A predicate I : S → B is an invariant of the continuous vector field f : S → S and guard G :

The operation •P is the Kleisli extension (−) † in the powerset monad. Hence we could simply write (γ f G ) † I ⊆ I. The definition of invariance unfolds to ∀s. I s → (∀X ∈ Sols f T s.∀t ∈ T. (∀τ ∈ ↓t. G (X τ)) → I (X t)).

For G = we call I an invariant of f along T . Intuitively, invariants can be seen as sets of orbits. They are compatible with the invariants from Sect. 3. Hence we can use a variant of (h-inv) for verification condition generation:

The following lemma leads to a procedure. Lemma 6.2 ([16] ). Let f : S → S be a continuous vector field, μ, ν : S → R differentiable and T ⊆ R an interval such that 0 ∈ T . 

Variable h 0 stores an initial water level; π indicates whether the pump is on or off. The rate of change of the water-level is linear with slope

The vector field f for this behaviour and its invariant dI are abbreviation f k ≡ [π →s 0 , h →s k , h0 →s 0 , t →s 1 ]

Program tank-dinv for the controller is given by guard G h x k with h x ∈ {h l , h h } that restricts evolutions beyond h x , loop invariant I, control and dynamics:

We distinguish DINV and INV to structure specifications. The correctness specification and verification of the water tank with dH then proceeds as follows:

lemma tank-inv : assumes 0 ≤ τ and 0 < co and co < ci

prefer 4 prefer 7 using tank-diff-inv assms apply force+ using assms tank-inv-arith1 tank-inv-arith2 by rel-auto

Tactic hyb-hoare blasts away the control structure. The second proof line uses Lemma tank-diff-inv to check that dI is an invariant for any guard (Guard is a universally quantified variable in Lemma tank-diff-inv ), using the procedure outlined. Auxiliary lemmas discharge the remaining proof obligations.

A refinement Kleene algebra with tests (rKAT) [3] is a KAT (K, B) expanded by an operation [−, −] : B × B → K that satisfies, for all α ∈ K and p, q ∈ B,

The element [p, q] of K corresponds to Morgan's specification statement [25] . Variants of Morgan's laws [25] of a propositional refinement calculus-once more ignoring assignments-are then derivable in rKAT [3] .

(r-while)

We have also derived α ≤ [0, 1] and [1, 0] ≤ α, but do not use them in proofs. For invariants and loops, we obtain the additional refinement laws

(r-loop)

In Sta S, moreover, the following assignments laws are derivable [3] .

(r-assgnf)

The second and third law are known as leading and following law. They introduce an assignment before and after a block of code. Finally, we obtain the following refinement laws for evolution commands. 

The laws in this section form the differential refinement calculus dR. They suffice for constructing hybrid programs from initial specification statements by step-wise refinement incrementally and compositionally. A more powerful variant based on predicate transformersà la Back and von Wright [4] has been developed in [16] ; yet applications remain to be explored. A previous approach to refinement in dL [23] is quite different to the two standard calculi mentioned (see Conclusion).

We now construct program therm from Example 5.2 by step-wise refinement using the rules of dR.

lemma R-therm-down: assumes a > 0 and 0 ≤ τ and 0 < T l and

using therm-dyn-down[OF assms (1 ,3 ) , of -T h ] assms by rel-auto lemma R-therm-up: assumes a > 0 and 0 ≤ τ and 0 < T l and The refinement tactic pushes the refinement specification through the program structure until the only remaining proof obligations are atomic refinements. We only refine the atomic programs needed to complete proofs automatically; those for the first two assignment and the evolution commands.

Alternatively we may use differential invariants with dR to refine tank-dinv from Example 6.3. This time we supply a single structured proof to show another style of refinement. We abbreviate long expressions with schematic variables. lemma R-tank-inv : assumes 0 ≤ τ and 0 < co and co < ci

by (refinement, rel-auto ) moreover have ?R1 ≥ LOOP ((t ::= 0 );(h0 : The proof incrementally refines the specification of tank-dinv using the laws of dR. As in Example 7.2, after refining the first two assignments, tactic refinement completes the construction of ctrl. After that, the invariant is supplied via lemma tank-diff-inv from Example 6.3 to construct dyn. The final program is then constructed by transitivity of ≤. A more detailed derivation is also possible.

Finally, we present variants of dH and dR that start directly from flows ϕ : 

A ball falls down from height h ≥ 0, with x denoting its position, v its velocity and g its acceleration. Its kinematics is modelled by the flow

The ball bounces back elastically from the ground. This is modelled by a discrete control that checks for x = 0 and then flips the velocity. Guard G = (x ≥ 0) excludes any motion below the ground. This is modelled by the hybrid program [26] abbreviation bb-evol g h T ≡

Its loop invariant conjoins the guard G with a variant of energy conservation. The correctness specification and proof with dH and dR are then straightforward.

lemma bouncing-ball-dyn: assumes g < 0 and h ≥ 0

using assms by (rel-auto simp: bb-real-arith)

lemma R-bouncing-ball-dyn: In the refinement proof, the tactic leaves only the refinement for the assignment v ::= −v . This is supplied via lemma R-bb-assign and the remaining obligations are discharged with the same arithmetical facts.

We have contributed new methods and Isabelle components to an open modular semantic framework for verifying hybrid systems that so far focussed on predicate transformer semantics [16] ; more specifically a Hoare logic dH and a Morgan-style refinement calculus dR for hybrid programs, more generic state spaces modelled by lenses, improved Isabelle syntax for correctness specifications and hybrid programs, and increased proof automation via the tactics hyb-hoare and refinement. These components support three workflows based on certifying solutions to Lipschitz-continuous vector fields, reasoning with invariant sets for continuous vector fields, and working directly with flows without certification. Compared to the standard dL toolchain, dH and dR emphasise a natural mathematical style of semantic reasoning about dynamical systems, with minimal conceptual overhead relative to standard Hoare logics and refinement calculi. dH, in particular, is only used for automated verification condition generation. The modular approach with algebras and a shallow embedding has simplified the construction of these verification components and made it incremental relative to extant ones. Our framework is not only open to use any proof method and mathematical approach supported by Isabelle, it should also allow adding new methods, for instance based on discrete dynamical systems, hybrid automata or duration calculi [7, 22] , or integrate CAS's for finding solutions.

The relevance of dH and dR to hybrid systems verification is further evidenced by the fact that such approaches are not new: A hybrid Hoare logic has been proposed by Liu et al. [22] for a duration calculus based on hybrid CSP. It is conceptually very different from dH and dL. A differential refinement logic based on dL has been developed as part of Loos' PhD work [23] . It uses a proof system with inference rules for reasoning about inequalities between KAT expressions, which are interpreted as refinements between hybrid programs. According to the authors, it differs substantially from the standard approaches [4, 25] in that local instead of global refinement relations can be used. Nevertheless their refinement logic has the same expressivity as dL [23] , which is essentially a predicate transformer calculus for hybrid programs [16] and thus a refinement calculusà la Back and von Wright. Ultimately, this suggests that Loos' logic is more expressive than our Morgan-style calculus, but the relative merits of the two approaches remain to be explored. The proof theory of dL has already been deeply embedded in proof assistants [5] , yet with a focus on soundness proofs for its inference rules and a mechanisation of its idiosyncratic substitution calculus, but not as prima facie verification components.

The expressivity and complexity gap between Hoare logic and predicate transformer semantics is apparent within algebra. The weakest liberal precondition operator cannot be expressed in KAT [27] . The equational theory of KAT, which captures propositional Hoare logic, is PSPACE complete [21] , that of modal Kleene algebra, which yields predicate transformers, in EXPTIME [24] .

Finally, while KAT and rKAT are convenient starting points for building program construction and verification components for hybrid programs, the simple and more general setting of Hoare semigroups [27] would support developing hybrid Hoare logics for total program correctness-where balls may bounce forever-or even for multirelational semantics [11, 12] , which are relevant needed for differential game logic [26] . This is left for future work.

Kleene algebra with tests and program schematology

Kleene algebra with tests and demonic refinement algebras

Building program construction and verification tools from algebraic principles

Refinement Calculus-A Systematic Introduction

Formally verified differential dynamic logic

Verification of hybrid systems. Handbook of Model Checking

Hybrid relations in Isabelle/UTP

Optics in Isabelle/HOL. Archive of Formal Proofs

Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming. Archive of Formal Proofs

Unifying heterogeneous state-spaces with lenses

Binary multirelations. Archive of Formal Proofs

Taming multirelations

Program construction and verification components based on Kleene algebra

Type classes and filters for mathematical analysis in Isabelle/HOL

Verification components for hybrid systems

Predicate transformer semantics for hybrid systems: verification components for Isabelle/HOL

Ordinary differential equations. Archive of Formal Proofs

The flow of ODEs: formalization of variational equation and Poincaré map

Kleene algebra with tests

On Hoare logic and Kleene algebra with tests

The complexity of Kleene algebra with tests

A calculus for hybrid CSP

Differential refinement logic

Algebras of modal operators and partial correctness. Theoret

Programming from Specifications, 2nd edn

Logical Foundations of Cyber-Physical Systems

Hoare semigroups

Ordinary Differential Equations and Dynamical Systems

Acknowledgements. The authors wish to thank the reviewers for their very thorough and insightful comments, and to Sergey Goncharov and André Platzer for discussions on a preliminary version. The second author is sponsored by CONACYT's scholarship no. 440404; the first author is supported by the EPSRC project CyPhyAssure 3 (Grant EP/S001190/1).