IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale

In this section, we consider two ways to specify continuous dynamical systems [71]: explicitly via flows and implicitly via systems of ordinary differential equations (ODEs). Flows are functions \(\varphi :T\rightarrow \mathcal {C}\rightarrow \mathcal {C}\), where T is a non-discrete submonoid of the real numbers \(\mathbb {R}\) representing time. Similarly, \(\mathcal {C}\) is a set with some topological structure like a vector space or a metric space. We emphasise this intuition using an overhead arrow for elements \(\vec {c}\in \mathcal {C}\) and refer to \(\mathcal {C}\) as a continuous state space. By definition, flows are continuously differentiable ( \(C^1\)) functions and monoid actions: they satisfy the lawsGiven a state \(\vec {c}\in \mathcal {C}\), the trajectory \(\varphi _{\vec {c}}:T\rightarrow \mathcal {C}\), such that \(\varphi _{\vec {c}}\, t = \varphi \, t\, \vec {c}\), is a curve modelling the continuous dynamical system’s evolution in time and passing through \(\vec {c}\). The orbit map \(\gamma ^\varphi : \mathcal {C}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\, \mathcal {C}\), such that \(\gamma ^\varphi \, \vec {c} = {{\,\mathrm{\mathcal {P}}\,}}\, \varphi _{\vec {c}}\, T\), gives the graph of this curve for \(\vec {c}\), where \({{\,\mathrm{\mathcal {P}}\,}}\) denotes both the powerset operation and the direct image operator.

Systems of ODEs are related to flows through their solutions. Formally, systems of ODEs are specified by vector fields \(f:T\rightarrow \mathcal {C}\rightarrow \mathcal {C}\), functions assigning vectors to points in space-time. A solution X to the system of ODEs specified by f is then a \(C^1\)-functionfor all t in some interval \(U\subseteq T\). This solution also solves the associated initial value problem (IVP) given by \((t_0,\vec {c})\) (denoted by \(X\in ivp \texttt {-} sols \, U\, f\, t_0\, \,\vec {c}\)) if it satisfiesThe existence of solutions to IVPs is guaranteed for continuous vector fields by the Peano theorem, albeit on an interval \(U\, \vec {c}\) depending on the initial condition \((t_0,\vec {c})\). Similarly, the Picard–Lindelöf theorem states that all solutions to the IVP \(X'\, t= f\, t\, (X\, t)\) with \(X\, t_0 = \vec {c}\) coincide in some interval \(U\, \vec {c} \subseteq T\) (around \(t_0\)) if f is Lipschitz continuous on T. In other words, it states that there is a unique solution to the IVP on \(U\, \vec {c}\). Thanks to this, when f is Lipschitz continuous on T, \(t_0 =0\), and \(U\, \vec {c} = T\) for all \(\vec {c}\in \mathcal {C}\), the solutions to the associated IVPs are exactly a flow’s trajectories \(\varphi _{\vec {c}}\), that isTherefore, the flow \(\varphi \) is the function mapping to each \(\vec {c}\in \mathcal {C}\) the unique \(\varphi _{\vec {c}}\) such that \(\varphi _{\vec {c}}\in ivp \texttt {-} sols \, T\, f\, 0\, \,\vec {c}\).

Having introduced some basic concepts from the theory of dynamical systems, we present our hybrid systems model. We represent these via hybrid programs which are traditionally defined syntactically [31, 61]. Yet, our approach is purely semantic and we merely provide the recursive definition below as a guide to what our semantics should model:Typically, x denotes variables; e and f are terms, and G and P are assertions. In dynamic logic [31], the statement \(x:=e\) represents an assignment of variable x to expression e, models testing whether P holds, while , \(\alpha \sqcap \beta \) and \(\alpha ^*\) are the sequential composition, nondeterministic choice, and finite iteration of programs \(\alpha \) and \(\beta \). Well-known while-programs emerge via the equationsBeyond these, differential dynamic logic ( \(\textsf{d}\mathcal {L}\)) [61] uses evolution commands \( x' = f \, \& \, G\) that represent systems of ODEs with boundary conditions or guards G. A guard G delimits the solutions’ range to the region described by G.

We use nondeterministic state transformers \(\alpha :\mathcal {S}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\mathcal {S}\) as our semantic representation for hybrid programs. Thus, our “hybrid programs” are really arrows in the Kleisli category of the powerset monad. Observe that a subset of these arrows also model “assertions”, namely the subidentities of the monadic unit \(\eta _\mathcal {S}\), such that \(\eta _\mathcal {S}\, s = \{s\}\) for all \(s\in \mathcal {S}\). That is, the functions mapping each state s either to \(\{s\}\) or to \(\emptyset \) model assertions where \(P\, s = \{s\}\) represents that P holds for s, and \(P\, s = \emptyset \) that P does not hold for s. Henceforth, we abuse notation and identify predicates \(P:\mathcal {S}\rightarrow \mathbb {B}\) (or \(P\in \mathbb {B}^\mathcal {S}\)), sets ( \(P\in {{\,\mathrm{\mathcal {P}}\,}}S\)), and subidentities of \(\eta _\mathcal {S}\), where \(\mathbb {B}\) denotes the Booleans. We also treat predicates as logic formulae by writing, for instance, \(P\wedge Q\) and \(P\vee Q\) instead of \(\lambda s.\ P\, s\wedge Q\, s\) and \(\lambda s.\ P\, s\vee Q\, s\). Thus, we denote the constantly true and constantly false predicates by \(\top \) and \(\bot \) respectively. They coincide with the \(\texttt {skip} \) and \(\texttt {abort}\) programs such that \(\texttt {skip} = \eta _\mathcal {S}\) and \(\texttt {abort}\, s = \emptyset \) for all \(s\in \mathcal {S}\). In this state transformer semantics, sequential compositions correspond to (forward) Kleisli compositions, nondeterministic choices are point-wise unions, and finite iterations are a limit of sequential compositions. That is,with \(\alpha ^{i+1}=\alpha ;\alpha ^i\) and \(\alpha ^{0}=\texttt {skip} \).

To introduce our state transformer semantics of assignments and ODEs, we first describe our store model. We use lenses [8, 24, 52] to algebraically characterise the hybrid store. Through an axiomatic approach to accessing and mutating functions, lenses allow us to locally manipulate program stores [18] and algebraically reason about program variables [23, 25]. Formally, a lens \(x\) with source \(\mathcal {S}\) and view \(\mathcal {V}\), denoted \(x{:}{:} \mathcal {V}\Rightarrow \mathcal {S}\), is a pair of functions \((get_x, put_x)\) with \(get_x: \mathcal {S}\rightarrow \mathcal {V}\) and \(put_x: \mathcal {V}\rightarrow \mathcal {S}\rightarrow \mathcal {S}\) such that

for all \(v,v'\in \mathcal {V}\) and \(s\in \mathcal {S}\). Usually, a lens \(x\) represents a variable, \(\mathcal {S}\) is the system’s state space and \(\mathcal {V}\) is the value domain for \(x\). Under this interpretation, \({\textit{get}}_x\) returns the value of variable \(x\) while \({\textit{put}}_x\) updates it. Yet, we sometimes interpret \(\mathcal {V}\) as a subregion of \(\mathcal {S}\), making \({\textit{get}}_x\) a projection or restriction and \({\textit{put}}_x\) an overwriting or substituting function. There are other models using diverse variable lenses, such as arrays, maps and local variables [18, 25].

We model expressions and assertions used in program syntax as functions \(e:\mathcal {S}\rightarrow \mathcal {V}\), which semantically are queries over the store \(\mathcal {S}\) returning a value of type \(\mathcal {V}\). We can use the \({\textit{get}}\) function to perform such queries by “looking up the value of variables”. For instance, if \(x, y {:}{:} \mathbb {R}\Rightarrow \mathcal {S}\) model independent program variables, and \(c\in \mathbb {R}\) is a constant, then the function \(\lambda s.\ ({\textit{get}}_x~s)^2 + ({\textit{get}}_y~s)^2 \le c^2\) represents the “expression” \(x^2 + y^2 \le c^2\). Then, function evaluation corresponds to computing the value of the expression at state \(s\in \mathcal {S}\).

With this representation, the state transformer \(\lambda s.\ \{{\textit{put}}_x\, (e\, s)\, s\}\) models a program assignment, denoted by \(x:= e\). More generally, we turn deterministic functions \(\sigma :\mathcal {S}\rightarrow \mathcal {S}\) into state transformers via function composition with the Kleisli unit, which we denote by \(\langle \sigma \rangle = \eta _\mathcal {S}\circ \sigma \). Then, representing expressions e as functions \(e:\mathcal {S}\rightarrow \mathcal {V}\), our model for variable assignments becomes

To derive in our framework a state transformer semantics \(\mathcal {S}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\mathcal {S}\) for evolution commands \( x' = f \, \& \, G\), observe that a flow’s orbit map \(\gamma ^\varphi :\mathcal {C}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\mathcal {C}\) with \(\gamma ^\varphi \, \vec {c}=\{\varphi \, t\, \vec {c}\mid t\in T\}\) is already a state transformer on \(\mathcal {C}\). It sends each \(\vec {c}\) in the continuous state space \(\mathcal {C}\) to the reachable states of the trajectory \(\varphi _{\vec {c}}\). Based on the relationship between flows and the solutions to IVPs from Sect. 3.1, we can generalise this state transformer to a set of all points \(X\, t\) of the solutions X of the system of ODEs represented by f, i.e. \(X'\, t = f\, t\, (X\, t)\), with initial condition \(X\, t_0 = \vec {c}\) over an interval \(U\, \vec {c}\) around \(t_0\) ( \(t_0\in U\,\vec {c}\)). Moreover, in line with \(\textsf{d}\mathcal {L}\), the solutions should remain within the guard or boundary condition G: \(\forall \tau \in U\, \vec {c}.\ \tau \le t\Rightarrow G\, (X\, \tau )\). Thus, to specify dynamical systems via ODEs f instead of flows \(\varphi \), we define the generalised guarded orbits map [50]

that also introduces guards G, initial conditions \(t_0\), and intervals \(U\, \vec {c}\). The set \({t}{{\downarrow }_{T}}\) is a downward closure \({t}{{\downarrow }_{T}} =\{\tau \in T\mid \tau \le t\}\) which in applications becomes the interval \([0,t]=\{\tau \mid 0\le \tau \le t\}\) because we usually fix \(U\, \vec {c}=\mathbb {R}_{\ge 0}=\{\tau \mid \tau \ge 0\}\) for all \(\vec {c}\in \mathcal {C}\). This is why we also abuse notation and write constant interval functions \(\lambda \vec {c}.\ T\) simply as T. Notice that when the flow \(\varphi \) for f exists, \(\gamma ^f\, \top \, T\, 0\, \vec {c} = \gamma ^\varphi \, \vec {c}\).

Lenses support algebraic reasoning about variable frames: the set of variables that a hybrid program can modify. In particular, they allow us to split the state space into continuous and discrete parts. We explain a lens-based lifting of guarded orbits \(\gamma ^f\, G\, U\, t_0\) from the continuous space \(\mathcal {C}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\mathcal {C}\) to the full state space \(\mathcal {S}\) in Sect. 5.2. This produces our state transformer for evolution commands \( (x' = f\, \& \, G)_U^{t_0}:\mathcal {S}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\mathcal {S}\). Intuitively, it maps each state \(s\in \mathcal {S}\) to all X-reachable states within the region G, where X solves the system of ODEs specified by f, and leaves intact the non-continuous part of \(\mathcal {S}\). Having the same type as the above-described state transformers enables us to seamlessly use the same operations on \( (x' = f\, \& \, G)_U^{t_0}\). This also enables us to do modular verification condition generation (VCG) of hybrid systems as described in Sect. 3.5.1.

Finally, we extend our state transformer semantics to a predicate transformer ( \(\mathbb {B}^\mathcal {S}\rightarrow \mathbb {B}^\mathcal {S}\)) semantics for verification condition generation (VCG). Concretely, we define two predicate transformers and use the definition of the first one for deriving partial correctness laws, including the rules of Hoare logic, and the definition of the second one for deriving reachability laws. We also exemplify the application of these to VCG.

Most modelling and programming languages support modules with local variables, constant declarations, and assumptions. We have implemented an Isabelle command that automates the creation of hybrid stores, which provide a local theory context for hybrid programs. We call these dataspaces, since they are state spaces that can make use of rich data structures in the program variables.

A dataspace has constants \(c_i: C_i\), named constraints \(a_i: P_i\) and state variables \(x_i: T_i\). In its context, we can create local definitions, theorems and proofs, which are hidden, but accessible using its namespace. Internally, the dataspace command creates an Isabelle with fixed constants and assumptions, inspired by previous work by Schirmer and Wenzel [66]. Like locales, dataspaces support a form of inheritance, whereby constants, assumptions, and variables can be imported from an existing dataspace (e.g. parent_store) and extended with further constants, assumptions, and variables.

Each declared state variable is assigned a lens \(x_i {:}{:} T_i \Rightarrow \mathcal {S}\), using the abstract store type \(\mathcal {S}\) with the lens axioms from Secion 3.3 as locale assumptions. We also generate independence assumptions, e.g. \(x_i\mathop {\,\bowtie \,}x_j\) for \(x_i\ne x_j\), that distinguish different variables semantically [25]. Formally, \(x\mathop {\,\bowtie \,}y\) if \({\textit{put}}_x\, u\circ {\textit{put}}_y\, v = {\textit{put}}_y\, v\circ {\textit{put}}_x\, u\) for all \(u,v\in \mathcal {V}\). That is, two lenses are independent if their \({\textit{put}}\) operations commute on all states.

As discussed in Sect. 3.3, expressions in our hybrid modelling language are modelled by functions of type \(\mathcal {S}\rightarrow \mathcal {V}\). Assertions are therefore state predicates, or “expressions” where \(\mathcal {V}= \mathbb {B}\). Discharging VCs requires showing that assertions hold for all states. For example, the law (wlp-test) requires us to prove a VC of the form \(P \Rightarrow Q\), that is, \(\forall s.\ P s\Rightarrow Q\, s\). Also, if we have state variables x and y, then proving the assertion \(x + y \ge x\) corresponds to proving the HOL predicate \({\textit{get}}_x~s + {\textit{get}}_y~s \ge {\textit{get}}_x~s\) for some arbitrary-but-fixed state s, which can readily by discharged using one of Isabelle’s proof methods (simp, auto etc.). We automate this process via our methods expr-simp and expr-auto.

Nevertheless, there remains a gap between the syntax used in typical programming languages and its semantic representation. Namely, users would prefer writing \(x^2 + y^2 \le c^2\) over \(\lambda s.\ ({\textit{get}}_x~s)^2 + ({\textit{get}}_y~s)^2 \le c^2\), and so, the main technical challenge is to seamlessly transform between the two. This can be achieved using Isabelle’s syntax pipeline, which significantly improves the usability of our tool.

Isabelle’s multi-stage syntax pipeline parses Unicode strings and transforms them into “pre-terms” [39]: elements of the ML term type containing syntactic constants. These must be mapped to previously defined semantic constants by syntax translations, before they can be checked and certified in the Isabelle kernel. Printing reverses this pipeline, mapping terms to strings.

We automate the translation between the expression syntax (pre-terms) and semantics using parse and print translations implemented in Isabelle/ML, as part of our Shallow-Expressions component. It lifts pre-terms by replacement of free variables and constants, and insertion of store variables ( \({{{\textsf {\textit{s}}}}}\)) and \(\lambda \)-binders. Its implementation uses the syntactic annotation \((t)_{{{{\textsf {\textit{e}}}}}}\) to lift the syntactic term t to a semantic expression in the syntax translation rules. The syntax translation is described by the following equations:where \(p \mathop {\,\rightleftharpoons \,}q\) means that pre-term p is translated to term q, and q printed as p. Moreover, \([-]_{{{\varvec{\mathsf{{ e}}}}}}\) is a constant that marks lifted expressions that are embedded in terms. When the translation encounters a name n (i.e. a free variable or constant), it checks whether n has a definition in the context. If it is a lens (i.e. \(n {:}{:} \mathcal {V}\Rightarrow \mathcal {S})\), then it inserts a \({\textit{get}}\). If it is an expression (i.e. \(n: \mathcal {S}\rightarrow \mathcal {V}\)), then it is applied to the state. Otherwise, it leaves the name unchanged, assuming it to be a constant. Function applications are also left unchanged by \(\rightleftharpoons \). For instance, \(((x + y)^2 / z)_{{{\varvec{\mathsf{{ e}}}}}} \rightleftharpoons [\lambda {{\varvec{\mathsf{{ s}}}}}.\, ({\textit{get}}_x~{{\varvec{\mathsf{{ s}}}}} + {\textit{get}}_y~{{\varvec{\mathsf{{ s}}}}})^2 / z]_{{{\varvec{\mathsf{{ e}}}}}}\) for variables (lenses) x and y and constant z. Once an expression has been processed, the resulting \(\lambda \)-term is enclosed in \([-]_{{{\varvec{\mathsf{{ e}}}}}}\). The pretty printer can then recognise a lifted term and print it. This process is fully automated, so that users see only the sugared expression, without the \(\lambda \)-binders, in both the parser and terms’ output during the proving process.

In our semantic approach, substitutions correspond to functions \(\sigma : \mathcal {S}\rightarrow \mathcal {S}\). We can then denote updates as sequences of variable assignments. That is, instead of directly manipulating the store \(s: \mathcal {S}\) with the lens functions, we provide user-friendly program specifications with the notation \(\sigma (x\!\leadsto \!e) = \lambda s.\,{\textit{put}}_x\, (e\, s)\, (\sigma \,s)\). Thus, assignments can be described as sequences of updates for lenses \(x_i {:}{:} \mathcal {V}_i \Rightarrow \mathcal {S}\) and “expressions” \(e_i: \mathcal {S}\rightarrow \mathcal {V}_i\):

Implicitly, any variable y not mentioned in such a substitution is left unchanged: \(y \leadsto y\). We further write \(e[v/x] = e \circ [x \leadsto v]\), with \(x {:}{:} \mathcal {V}\Rightarrow \mathcal {S}\), \(e: \mathcal {S}\rightarrow \mathcal {V}'\), and \(v: \mathcal {S}\rightarrow \mathcal {V}\), for the application of substitutions to expressions. This yields standard notations for program specifications, e.g. \((x:= e) = \langle [x \leadsto e] \rangle \) and . Using an Isabelle simplification procedure (a “simproc”), the simplifier can reorder assignments alphabetically according to their variable name, and otherwise reduce and evaluate substitutions during VCG [25]. We can extract assignments for x writing \(\langle \sigma \rangle _s\,x = {\textit{get}}_x \circ \sigma \) so that, e.g. \(\langle [x \leadsto e_1, y \leadsto e_2] \rangle _s\, x\) reduces to \(e_1\) when \(x \mathop {\,\bowtie \,}y\).

Vectors and matrices are ubiquitous in engineering applications and users of our framework would appreciate using familiar concepts and notations to them. This is possible due to our modelling language. In particular, vectors are supported by HOL-Analysis using finite Cartesian product types, (A,n) vec with the notation A⌃n. Here, A is the element type, and n is a numeral type denoting the dimension. The type of vectors is isomorphic to \([n] \rightarrow A\) where \([n]=\{1,\dots ,n\}\). A matrix is simply a vector of vectors, A⌃m⌃n, hence a map \([m] \rightarrow [n] \rightarrow A\). Building on this, we supply notation [[x11,...,x1n],...,[xm1,...,xmn]] for matrices and means for accessing coordinates of vectors via hybrid program variables [19]. This notation supports the inference of vector and matrices’ dimensions conveyed by the type variables.

Vectors and matrices are often represented as composite objects consisting of several values, e.g. \(p = (p_x, p_y)\in \mathbb {R}^2\). When writing specifications, it is often convenient to refer to and manipulate these components individually. We can denote such variables using component lenses and the lens composition operator. We write , for \(x_1{:}{:}\mathcal {S}_1 \Rightarrow \mathcal {S}_2\), \(x_2{:}{:}\mathcal {S}_2\Rightarrow \mathcal {S}_3\), for the forward composition and \({\textbf {1}}_\mathcal {S}{:}{:} \mathcal {S}\Rightarrow \mathcal {S}\) for the units in the lens category, but do not show formal definitions [25]. Intuitively, the composition selects part of a larger store as illustrated below.

We model vectors in \(\mathbb {R}^n\) as part of larger hybrid stores, lenses \(v{:}{:}\mathbb {R}^n\Rightarrow \mathcal {S}\), and project onto coordinate \(v_k{:}{:}\mathbb {R}\Rightarrow \mathcal {S}\) using lens composition and a vector lens \(\Pi (i){:}{:}\mathbb {R}\Rightarrow \mathbb {R}^n\): and \(i\in [n]=\{1,\dots ,n\}\). The lookup function \(\textit{vec-nth}: A^n \rightarrow [n] \rightarrow A\) and update function \(\textit{vec-upd}: A^n \rightarrow [n] \rightarrow A \rightarrow A^n\) come from HOL-Analysis and satisfy the lens axioms (lens-laws). Then, as an example, and for \(p {:}{:} \mathbb {R}^2 \Rightarrow \mathcal {S}\), using to first select the variable p and then the vector-part of the hybrid store. Intuitively, two vector elements are independent, \(\Pi (i) \mathop {\,\bowtie \,}\Pi (j)\) iff they have different indices, \(i \ne j\).

Lenses support algebraic manipulations of variable frames. A frame is the set of variables that a program is permitted to change. Variables outside of the frame are immutable. We first show how variable sets can be modelled via lens sums. Then we recall a predicate characterising immutable program variables [22]. Most importantly, we derive a frame rule à la separation logic for local reasoning with framed variables.

Variable lenses \(x_1 {:}{:} \mathcal {V}_1\Rightarrow \mathcal {S}\) and \(x_2 {:}{:}\mathcal {V}_2 \Rightarrow \mathcal {S}\) can be combined into lenses for variable sets with lens sum [25], \(x_1 \oplus x_2{:}{:} \mathcal {V}_1\times \mathcal {V}_2 \Rightarrow \mathcal {S}\) if \(x_1 \mathop {\,\bowtie \,}x_2\) viaThis combines two independent lenses into a single lens with a product view. It can be used to model composite variables, for example, \((x \oplus y):= (e, f)\) is a simultaneous assignment to x and y. We can decompose such a composite update into two atomic updates, with \([(x, y)\!\leadsto \!(e_1, e_2)] = [x\!\leadsto \!e_1, y\!\leadsto \!e_2]\). We can also use lens sums to model finite sets, for example \(\{x, y, z\}\) is modelled as \(x \oplus (y \oplus z)\). Each variable in such a sum may have a different type, e.g. \(\{v_x, \vec {p}\}\) is a valid and well-typed construction.

Lens sums are only associative and commutative up-to isomorphism of cartesian products. We need heterogeneous orderings and equivalences between lenses to capture this. We define a lens preorder [25], that captures the part-of relation between \(x_1 {:}{:} \mathcal {V}_1 \Rightarrow \mathcal {S}\) and \(x_2 {:}{:} \mathcal {V}_2 \Rightarrow \mathcal {S}\), e.g. \(v_x \preceq \vec {v}\) and \(\vec {p} \preceq \vec {p} \oplus \vec {v}\). Lens equivalence \({\cong } = {\preceq }\cap {\succeq }\) then identifies lenses with the same shape in the store. Then, for variable set lenses up-to \(\cong \), \(\oplus \) models \(\cup \), \(\mathop {\,\bowtie \,}\) models \(\notin \),

and \(\preceq \) models \(\subseteq \) or \(\in \). Since \(x_1 \preceq x_1 \oplus x_2\) and \(x_1 \oplus x_2 \cong x_2 \oplus x_1\), with our variable set interpretation, we can show, e.g., that \(x \in \{x, y, z\}\), \(\{x, y\} \subseteq \{x, y, z\}\), and \(\{x, y\} = \{y, x\}\). Hence we can use these lens combinators to construct and reason about variable frames.

We can use variable set lenses to capture the frame of a program. Let \(A{:}{:}\mathcal {V}\Rightarrow \mathcal {S}\) be a lens modelling a variable set. For \(s_1,s_2\in \mathcal {S}\) let \(s_1\approx _A s_2\) hold if \(s_1=s_2\) up-to the values of variables in A, that is \({\textit{get}}_A~s_1 = {\textit{get}}_A~s_2\). Local reasoning within A uses the lens quotient [18] \(x\mathop {\!\sslash \!}A\), which localises a lens \(x{:}{:} \mathcal {V}\Rightarrow \mathcal {S}\) to a lens \(\mathcal {V}\Rightarrow \mathcal {C}\). Assuming \(x\preceq A\), it yields \(x_1 {:}{:} \mathcal {V}\Rightarrow \mathcal {C}\) such that . For example, \(p_x \mathop {\!\sslash \!}p = \Pi (1)\) with \(\mathcal {C}=\mathbb {R}^n\).

We can also use lenses to describe when a variable does not occur freely in an expression or predicate with the unrestriction property: \(A \mathop {\sharp \,}e \Leftrightarrow \forall v.\, e \circ ({\textit{put}}_A~v) = e\) [25]. A variable x is unrestricted in e, written \(x \mathop {\sharp \,}e\), provided that e does not semantically depend on x for its evaluation. For example, \(x \mathop {\sharp \,}(y + 1)\), when \(x \mathop {\,\bowtie \,}y\), since \(y + 1\) does not mention x. We also define \((- A) \mathop {\sharp \,}e \Leftrightarrow \forall s_1\, s_2\, v.\, e\,({\textit{put}}_A\,v\,s_1) = e\, ({\textit{put}}_A\,v\,s_2)\) as the converse, which requires that e does not depend on variables outside of A.

Non-modification Next, we capture the non-modification of variables by a program. For \(\alpha :\mathcal {S}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\mathcal {S}\) and an expression (or predicate) e we define \(\alpha \mathop {{{{\textsf {\textit{nmods}}}}}\,}e \Leftrightarrow \left( \forall s_1\in \mathcal {S}.\ e(s_1) = e(s_2)\right) \), which describes when e does not depend on the mutable variable of \(\alpha \). The expression e can characterise a set of variables giving the set of immutable variables. For example, we have it that \((x:= x + 1) \mathop {{{{\textsf {\textit{nmods}}}}}\,}(y, z)\), when \(x \mathop {\,\bowtie \,}y\) and \(x \mathop {\,\bowtie \,}z\), since this assignment changes only x and no other variables.

Intuitively, non-modification \(\alpha \mathop {{{{\textsf {\textit{nmods}}}}}\,}x\), where x is a variable lens, is equivalent to the specification for \(\left\{ x = v\right\} \,\alpha \,\left\{ x = v\right\} \) for fresh logical variable v. This means that x retains its initial value in any final state of \(\alpha \). We prove the following laws for non-modification:

The variables in A are immutable for assignment \(x:= e\) provided x is not in A. A test modifies no variables, and therefore any set A is immutable. For the programming operators, non-modification is inherited from the parts. The final law shows that we can always shrink the specified set of immutable variables.

With these concepts in place, we derive two frame rules for local reasoning:

If program \(\alpha \) does not modify any variables mentioned in I, then I can be added as an invariant of \(\alpha \). In the first law, non-modification is checked directly of the variables used by I. In the second, which is an instance of the first, we instead infer the immutable variables of A and check that I does not depend on variables outside of A. With these laws, we can import invariants for a program fragment that refer to only those variables that are left unchanged. This allows us to perform modular verification, whereby we need only consider invariants of variables used in a component. In the following section, we show how this can be applied to systems of ODEs.

We extend previous components [50] for continuous dynamics with function framing techniques that project onto parts of the store. That is, we formally describe the implementation of the evolution command state transformer using the lens infrastructure described so far [21]. Specifically, we use framing to derive continuous vector fields ( \(\mathcal {C}\rightarrow \mathcal {C}\)) and flows from state-wide “substitutions” ( \(\mathcal {S}\rightarrow \mathcal {S}\)). We also add a non-modification rule for evolution commands. This supports local reasoning where evolution commands modify only continuous variables and leave discrete ones—outside a frame—unchanged.

Framing uses the second interpretation of lenses where the frame \(\mathcal {C}\) is a subregion of \(\mathcal {S}\) that we can access through \(x{:}{:}\mathcal {C}\Rightarrow \mathcal {S}\). We view the store as divided into its continuous \(\mathcal {C}\) and discrete parts and localise continuous variables to the former. The continuous part must have sufficient topological structure to support derivatives and is thus restricted to certain type constructions like normed vector spaces or the real numbers. However, the discrete part may use any type defined in HOL. With this view, we can use \({\textit{get}}_x\) and \({\textit{put}}_x\) to lift entities defined on \(\mathcal {C}\) or project those in \(\mathcal {S}\). For instance, given any \(s\in \mathcal {S}\) and a predicate \(G:\mathcal {S}\rightarrow \mathbb {B}\) (like the guards in evolution commands), there is a corresponding restriction \(G{\downarrow }^{s}_{x}:\mathcal {C}\rightarrow \mathbb {B}\) such that \(G{\downarrow }^{s}_{x}\, \vec {c} \Leftrightarrow G[\vec {c}/x]\Leftrightarrow G\, ({\textit{put}}_x\, \vec {c}\, s)\). Conversely, for \(s\in \mathcal {S}\) and X, a set of vectors in \(\mathcal {C}\), the set \(X{\uparrow }^{s}_{x} = {{\,\mathrm{\mathcal {P}}\,}}\, (\lambda \vec {c}.\ {\textit{put}}_x\, \vec {c}\, s)\, X\) has values in \(\mathcal {S}\).

More importantly, we can specify ODEs and flows via time-dependent deterministic functions (Sect. 4.3’s lens-subs). Given a lens \(x {:}{:} \mathcal {C}\Rightarrow \mathcal {S}\) from global store \(\mathcal {S}\) onto local continuous store \(\mathcal {C}\) and \(s\in \mathcal {S}\), we can turn any state-wide function \(f: T\rightarrow \mathcal {S}\rightarrow \mathcal {S}\) into a vector field \(f{\downarrow }^{s}_{x}:T\rightarrow \mathcal {C}\rightarrow \mathcal {C}\) by framing it via \(f{\downarrow }^{s}_{x}\, t\, \vec {c} = {\textit{get}}_x\left( (f\, t)\, ({\textit{put}}_x\vec {c}\, s)\right) \).

Using the previously described liftings and projections, we formally define the semantics of evolution commands. For this, we only need to lift the definition of generalised guarded orbits maps (orbit-map in Sect. 3.4) on the continuous \(\mathcal {C}\) to the larger space \(\mathcal {S}\). Thus, for substitution \(f:T\rightarrow \mathcal {S}\rightarrow \mathcal {S}\), predicate \(G:\mathcal {S}\rightarrow \mathbb {B}\), interval function \(U:\mathcal {C}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\, \mathbb {R}\), and \(t_0\in \mathbb {R}\) the state transformer \(\mathcal {S}\rightarrow {{\,\mathrm{\mathcal {P}}\,}}\mathcal {S}\) modelling evolution commands is where we abbreviate \({\textit{get}}_x\, s\) with \(x_{s}\). That is, evolution commands are state transformers that output those states whose discrete part remains unchanged from s but whose continuous part changes according to the ODEs’ solutions within G. With this, the law (wlp-evol) formally becomes

This says that the postcondition Q holds after an evolution command \( (x' = f\, \& \, G)_U^{t_0}\) for \(s\in \mathcal {S}\) if every solution X to the IVP corresponding to \((t_0, x_s)\) satisfies Q on every time t, provided G holds from the beginning of the interval \(t_0\in U\, x_s\) until t. Thus, VCG follows our description in Sect. 3: users must supply flows and evidence for Lipschitz continuity in order to obtain wlps. We provide tactics that automate these processes in Sect. 6.

We use Isabelle’s syntax translations to provide a natural syntax for specifying evolution commands. Users can write \(\{x_1' = e_1, \ldots , x_n' = e_n ~|~ G \, U\,V\, \mathop {\,@\,} t_0\}\) directly into the prover where each \(x_i{:}{:}\mathcal {V}_i\Rightarrow \mathcal {S}\) is a summand of the frame lens \(x=\{x_1, \ldots , x_n\}{:}{:}\mathcal {C}\Rightarrow \mathcal {S}\). Users can thus declare the ODEs in evolution commands coordinate-wise with lifted expressions \(e_i:\mathcal {S}\rightarrow \mathcal {V}_i\). They can also omit the parameters G, U, V and \(t_0\) which defaults them to \(\top \), \(\mathbb {R}_{\ge 0}\), \(\mathcal {C}\) and 0, respectively. If desired, they can also use product syntax \((x_1', \ldots , x_n') = (e_1, \ldots , e_n)\) or vector syntax \(x' = e\), and specify evolution commands using flows instead of ODEs with the notation \(\{\texttt {EVOL}\, x = e\, \tau \,|\, G\}\).

With these, non-modification of variables naturally extends to ODEs with the law

Specifically, any set of variables (A) without assigned derivatives in a system of ODEs is immutable. Then, by application of the frame rule, we can demonstrate that any assertion I that uses only variables outside of x is an invariant of the system of ODEs.

As discussed in Sect. 3, an alternative to using flows for verification of evolution commands is finding and certifying invariants for them. Mathematically, evolution commands’ invariants coincide with invariant sets for dynamical systems or \(\textsf{d}\mathcal {L}\) ’s differential invariants [50]. We abbreviate the statement “I is an invariant for the evolution command \( (x' = f\, \& \, G)_U^{t_0}\)” with the notation \( diff \texttt {-} inv \, x\, f\, G\, U\, t_0\, I\). In terms of Hoare logic, invariants for evolution commands satisfy Informally, \( diff \texttt {-} inv \, x\, f\, G\, U\, t_0\, I\) asserts that all states in the generalised guarded orbit \( (x' = f\, \& \, G)_U^{t_0}\, s\) of \(s\in \mathcal {S}\) such that \(I\, s\), will also satisfy I. In dynamical systems parlance, the orbits of the system of ODEs within the region characterised by I remain within I.

A common approach in hybrid program verification for certifying invariants for evolution commands is differential induction [59]. It establishes sufficient conditions for guaranteeing that simple predicates, such as (in)equalities, are invariants. From these, more complex predicates like conjunctions or disjunctions of these (in)equalities can be shown to be invariants using the rules (h-conji) and (h-disji).

Formally, if a predicate I is in negation normal form (NNF) in a first-order language for the real numbers \(\mathcal {L}_\mathbb {R}\langle 0,1,+,-,\cdot ,<,\le \rangle \), to show that it is an invariant, we can apply the rules (h-conji) and (h-disji) until the only remaining proof obligations are Hoare triples of literals. The negated literals can also be converted into positive ones via the equivalences \(\lnot (x<y)\Leftrightarrow y\le x\), \(\lnot (x\le y)\Leftrightarrow y<x\), and \(\lnot (x=y)\Leftrightarrow (y<x\vee x<y)\). The remaining proof obligations can be discharged by analysing the derivatives of the magnitudes represented in them as done in Example 9. In the sequel, we present the theory to do this analysis formally in our setting.

The discussion in Example 9 compares derivatives of expressions depending on the ODEs’ variables. In our semantic approach, the system of ODEs is modelled by a function \(f\, t:\mathcal {S}\rightarrow \mathcal {S}\) that becomes a vector field ( \(\mathcal {C}\rightarrow \mathcal {C}\)) after framing via some \(x{:}{:}\mathcal {C}\Rightarrow \mathcal {S}\), where \(\mathcal {C}\) is the continuous part of \(\mathcal {S}\). Similarly, our “expressions” are really functions \(e:\mathcal {S}\rightarrow \mathcal {U}\) (see Sect. 3.3), and we can assume that \(\mathcal {U}\) is a continuous state space to get “continuous expressions”. We frame these functions to the continuous part \(\mathcal {C}\) of \(\mathcal {S}\) to obtain our framed expressions \(e{\downarrow }^{x}_{s}:\mathcal {C}\rightarrow \mathcal {U}\) such that \(e{\downarrow }^{x}_{s} = e\circ (\lambda \vec {c}.\ {\textit{put}}_x\, \vec {c}\, s)\). We wish to “differentiate” these expressions as informally done in Example 9. Hence, for a general and formal treatment of our semantic entities, we use the Fréchet derivative of these framed expressions. More specifically, recall that, if a function \(F:\mathcal {C}\rightarrow \mathcal {U}\) between normed spaces \(\mathcal {C},\mathcal {U}\) is Fréchet differentiable at \(\vec {c}\), the Fréchet derivative of F at \(\vec {c}\) is the bounded linear operator \(D\, F\, \vec {c}: \mathcal {C}\rightarrow \mathcal {U}\) that attests this. In the finite-dimensional case, e.g. \(F:\mathbb {R}^n\rightarrow \mathbb {R}^m\) with \(m, n\in \mathbb {N}\), the Fréchet derivative \(D\, F\, \vec {c}\) is the Jacobian. It is well-known that if \(\vec {e}_i\) is the i-th unit vector of the canonical ordered base, the function \(\lambda \vec {x}.\ (D\, F\, \vec {x})\, \vec {e}_i\) provides the ith partial derivatives of F while the directional derivative of F in the direction of \(\vec {c}\) is \(\lambda \vec {x}.\ (D\, F\, \vec {x})\, \vec {c}\). With these ideas in mind, we define our framed Fréchet derivatives \(\mathcal {D}^{f}_{x}e:\mathcal {S}\rightarrow \mathcal {U}\) of expression \(e:\mathcal {S}\rightarrow \mathcal {U}\) in the direction of \(f:\mathcal {S}\rightarrow \mathcal {S}\) with respect to \(x{:}{:}\mathcal {C}\Rightarrow \mathcal {S}\) as [21] That is, they are the directional derivatives of framed expressions \(e{\downarrow }^{x}_{s}\) in the direction of the projection of f onto the continuous space \(\mathcal {C}\). These framed Fréchet derivatives capture the intuitive analysis performed in Example 9. In fact, the following rules are sound:

The rule (dinv-eq) asserts that showing that an equality is an invariant reduces to showing that both sides of the equality change at the same rate over time. Similarly, the rules (dinv-leq) and (dinv-less) state that showing that inequalities are invariants requires showing that the rates of change on both sides preserve or augment the initial difference.

From the users’ perspective, \(\mathcal {D}^{f}_{x}e\) operates as the derivative of expression e with respect to the variables x according to the system of ODEs f. Well-known laws hold. In summary, users can read (1) and (2) as stating that the derivative of constants or variables outside the frame of differentiation are 0. The law (3) says that the derivative of a variable inside the frame is dictated by the ODE, and thus, users simply need to substitute according to f. The remaining laws are well-known differentiation properties such as linearity of derivatives or the Leibniz rule.

Differential induction does not suffice to prove all invariant certifications [55, 58]. For instance, applying rule (dinv-less) to the dynamics \(x' =-x\) of Examples 1‐4 to show invariance of \(x>0\) does not lead to a concluding proof state. Indeed, \(\mathcal {D}^{[x\leadsto -x]}_{x}x=-x\) is not necessarily greater or equal to \(0=\mathcal {D}^{[x\leadsto -x]}_{x}0\). For those cases, differential dynamic logic \(\textsf{d}\mathcal {L}\) includes the differential ghost [55] rule which asserts the correctness of an evolution command given the correctness of a higher-dimensional but equivalent system of ODEs. Here we generalise our previous formalisation of this rule [21] and use it to derive \(\textsf{d}\mathcal {L}\) ’s three Darboux rules [55]. The latter concretise the ghost rule to the atomic cases of differential induction: (in)equalities. Thus, they help prove invariance of predicates where differential induction does not apply. Concretely, we formalise and prove the soundness of the rules:

where A is a square matrix, b is a vector, , x and y are independent variables \(y\!\mathop {\,\bowtie \,}\!x\), and y does not appear in G or f: \(y \mathop {\sharp \,}(G, f)\). In contrast with their usual presentation, our semantic formalisation of the Darboux rules also requires the existence of a third independent variable z such that \(z \mathop {\sharp \,}(G, f)\) because our proof requires two applications of the (dG) rule. More work is needed to provide an alternative proof without these conditions, and to generalise A and b in (dG) to be functions on x that do not mention y. The use of matrices in the (dG) rule was possible due to our previous work on linear systems [19, 34] but further generalisations are possible in terms of bounded linear operators.

Our tactic vderiv for automatically discharging statements of the form \(f' = g\) for functions \(f,g:\mathbb {R}\rightarrow \mathcal {C}\) has been described before [50] but it is a component of other tactics and we have extended its capabilities here. Essentially, by the chain rule of differential calculus, derivative laws often require further certifications of simpler derivatives. A recursive procedure emerges where the certification of \(f'\, t= g\, t\) with \(f= f_1\circ \cdots \circ f_n\) is determined by a list of proven derivative rules \((f_i\, (h\, t))'=f_i'(h\, t)\cdot (h'\, t)\) for \(i\in \{1,\dots ,n\}\) together with \(t'=1\). The tactic vderiv recursively applies these rules until it determines thatThen, it uses Isabelle’s support for (the undecidable problem of) higher-order unification to try to show thatFor this work, we have added derivative rules for the real-valued exponentiation \(\exp (-)\), the square root \(\sqrt{-}\), the tangent \(\tan (-)\) and cotangent \(\cot (-)\) trigonometric functions, and vectors’ inner products \(*_R\) and norms \(\Vert -\Vert \). The tactic vderiv is an integral part of those described below, and it is tacitly used in our example of Sect. 8.1.

As evidenced in Examples 1–4, verification of hybrid systems might depend on knowing that there is a unique solution for a system of differential equations. In practice, certifying the existence and uniqueness of solutions with a general-purpose prover has required finding the Lipschitz-continuity constant [21, 50]. If it exists, then by the Picard–Lindelöf theorem (see Sect. 3.1), there is an interval around the initial time where solutions to the system of ODEs are unique. Alternatively, a domain-specific prover can restrict the specification language to a fragment where uniqueness is guaranteed [59] albeit limiting the space of verifiable dynamics. Here, we provide the foundation for allowing a general-purpose prover to automatically certify the uniqueness of solutions to IVPs. Namely, we formalise the well-known fact that continuously differentiable ( \(C^1\)) functions are Lipschitz continuous. The statement of the Isabelle lemma is shown below.

Then, a procedure emerges when applying (wlp-flow) or (fdia-flow):

In Example 1, we use the fact that continuously differentiable ( \(C^1\)) functions are Lipschitz continuous to argue that a system of ODEs f has unique solutions by the Picard–Lindelöf theorem. Thus, formalisation of the rule is the first step towards automating the certification of the uniqueness of solutions to IVPs and a crucial step in hybrid system verification (via flows) in general-purpose proof assistants. Next, we provide tactics and to make certification of Lipschitz continuity as seamless in VCG as in pen and paper proofs, like that of Example 1. Our tactics automate an initial application, in a backward reasoning style, of our lemma . The tactics discharge the emerging proof obligations by replicating the behaviour of but using rules for continuity and Fréchet differentiability available in Isabelle’s HOL-Analysis library. The difference between both tactics is that allows users more control by enabling them to supply the derivative . We exemplify in VCG below:

In applications, we use our tactics on framed substitutions, e.g. , that represent systems of ODEs f. VCG also requires assumptions of lens-independence and satisfaction of lens laws due to our use of shallow expressions and frames. These are automatically provided by our Isabelle command and taken into account in our tactics. The tactic is indirectly used in the verification problem in Sect. 8.1. Both tactics automatically discharge proof obligations where the ODEs’ (the vector field f) form a linear system of ODEs. This already yields polynomial and transcendental functions as solutions \(\varphi \) to these systems. Accordingly, users can employ our tool support for linear systems of ODEs [34]. We leave the automation of Lipschitz continuity certification for non-linear systems as future work. Alternative proof strategies like differential induction (see Sect. 8) are also available for cases when these tactics fail.

In Sect. 6.2, we describe a procedure to verify the partial correctness of an evolution command by supplying the flow to its system of ODEs. Here, we automate the flow certification part of this procedure in a tactic . This proof method calls our two previously described tactics . The first one discharges the Lipschitz continuity requirement from the Picard–Lindelöf theorem to guarantee uniqueness of solutions to the associated IVP. The tactic certifies that the supplied flow \(\varphi \) is a solution to the system of ODEs. The following lines exemplify our tactic usage in hybrid systems verification tasks. Our tactic is robust as it automatically discharges frequently occurring proof obligations. Notice that for each Isabelle lemma below, there is a corresponding (local) Lipschitz continuity example from Sect. 6.2.

Crucially, certifies the exponential and trigonometric solutions required for these ODEs as evidenced by its successful application on the examples above and in the verification problem of Sect. 8.1.

In addition to our derivative, Lipschitz continuity, and flow automatic certifications, we have added various tactics for verification condition generation. The simplest one is . It merely calls Isabelle’s simplifier adding Sect. 3’s wlp  equational laws as rewriting rules except those for finite iterations and while loops which it initially tries to remove with invariant reasoning via (h-loopi) and (h-whilei). The tactic assumes that the hybrid program has the standard shape \(\texttt {loop } (\texttt {ctrl};\texttt {dyn})\texttt { inv }I\) iterating a discrete controller intervening in a continuous dynamical system as seen in Example 2. From this initial proof method, we create two tactics for supplying flows: the tactic takes as input a previously proven flow-certification theorem asserting our predicate . Alternatively, users can try to make this certification automatic with the tactic which requires as input a candidate solution \(\varphi \). It calls after applying and trying (wlp-flow) with the input \(\varphi \). The intention is that both and leave only proof obligations that require reasoning of first-order logic of real numbers. Complementary tactics and try to discharge these remaining proof obligations automatically leaving raw Isabelle terms in the proof obligations without our syntax translations. We have also supplied simple tactics for algebraic reasoning more interactively. Specifically, we have provided a tactic for distributing factors over additions and a tactic for simplifying powers in multi-variable monomials. See Sect. 8.1 for the application of these in a verification problem.

We have integrated two Computer Algebra Systems (CASs), namely SageMath and the Wolfram Engine, into Isabelle/HOL to supply symbolic solutions to ODEs. The user can make use of the integration via the command, which supplies a solution to the first ODE it finds within the current subgoal.

Below, we show an application of our integration and its corresponding output in Isabelle. Users can click the greyed-out area to automatically insert the suggestion.

Here, our plugin requests a solution to the ODE \(x' = 1\) from the Wolfram Engine. A \(\lambda \)-abstraction denotes the solution, which inputs the current time and has in its body the constructed substitution (see lens-subs). It provides the value for each continuous variable at time t. In this case, the substitution \([x \leadsto t + x]\) represents the solution \(x\, t = t + x\, 0\).

Our integration performs the following steps in order to produce a solution: We consider each of these stages below.

To have an extensible and modular interface, we implement (1) an intermediate data structure for representing ODEs and their solutions, and (2) procedures for translating back and forth between Isabelle and our intermediate representation. This allows us to capture the structure of the ODEs without the added overhead of Isabelle syntax. It also gives us a unified interface between Isabelle and any CAS.

Our plugin assumes that a system of ODEs is expressed as a substitution of the form \([x \leadsto e, y \leadsto f, \ldots ]\), as described in Sect. 5.2. Each expression ( \(e, f, \ldots \)) gives the derivative expression for each corresponding variable, potentially in terms of other variables. Naturally, for an ODE, these expressions are formed using only arithmetic operators and mathematical functions. We therefore derive the following constrained grammar for arithmetic expressions:

NConst represents numeric constants, such as e or \(\pi \). UOp is for unary operations and BOp is for binary operations. Both of these take a name, and the number of required parameter expressions. The name corresponds to the internal name for the operator in Isabelle/HOL. The operator “+”, for example, has the name Groups.plus_class.plus. We then have three constructors for numeric constants: NNat for naturals, NInt for integers and NReal for reals. We have three characterisations of variables: CVar are arbitrary but fixed variables, SVar are mutable (state) variables, and IVar represents the independent variable of our system, usually time.

A system of ODEs is then modelled simply as a finite map from variable names to derivative expressions. Converting back and forth between Isabelle terms (i.e. elements of the term datatype in Isabelle/ML) and the AExp datatype consists of recursing through the structure of the term, using a lookup table to translate each named arithmetic function.

Integrating a CAS into IsaVODEs consists of three separate components: a translation from the intermediate representation to the CAS input format, an interface with the CAS to obtain a solution, and a translation from the solution back into the required format.

Wolfram Engine The Wolfram Engine is the CAS behind WolframAlpha and Mathematica [76]. It is one of the leading CASs on the market, with powerful features for solving differential equations, amongst many other applications. The Wolfram language provides the DSolve function which produces solutions to various kinds of differential equations.

The basic building block for this integration is a representation of Wolfram expressions as an ML datatype. In the Wolfram language, everything is an expression [75], so this is sufficient for a complete interface. We represent these expressions as follows:

Real and Int represent real and integer numbers respectively. Id represented an identifiers, and Fun represents functions with only one list of arguments, which are distinguished from curried functions CurryFun with multiple sets of arguments.

Our approach for translation from AExp to expr is the following: Once we have a well-formed Wolfram expression, we use the wolframscript command-line interface to obtain a solution in the form of a list of Wolfram Rule expressions, which are isomorphic to our substitutions. We can parse the result back into the expr type, and translate this into the AExp type using a translation table for function names and the variable name mapping we constructed.

SageMath SageMath [72] is an open-source competitor to the Wolfram Engine. It is accessed via calls to a Python API. It integrates several open-source CASs to provide its functionality, choosing the best implementation for a particular symbolic computation. This makes SageMath an ideal target for integration with Isabelle.

The translation process is similar to our Wolfram Engine integration, but we also apply some preprocessing to the ODEs to make the solving more efficient. Since the CASs integrated with SageMath are better at solving smaller ODEs, we can improve their performance by rewriting the following kinds of ODEs: Capabilities There are two main cases where the integration fails to produce an Isabelle certification for a solution, despite the CAS returning a solution.

The first case happens when the provided solution contains a function not implemented in Isabelle. Instances of this case include functions defined in terms of integrals such as the error function or the Bessel function.

The second case concerns solutions which are undefined somewhere within their domain. Examples of this case include divisions by 0, which users can address by manually specifying the domain of the solution in Isabelle.

Despite these shortcomings, the CAS integration proves very effective at leveraging the solutions provided by CASs, as a large class of ODEs can be automatically solved and certified with minimal input from the user.

We have developed three main Eisbach proof methods for automating differential invariant proofs: , , and , which implement differential weakening, induction, and ghosts, respectively [50, 61]. We show the Eisbach declaration for some of them below. The first method, , applies the differential weakening law (theorem ) [59] to prove \(\left\{ P\right\} \,\{x' = f ~|~ G \}\,\left\{ Q\right\} \), when \(G \Rightarrow Q\). Proof of the implication is attempted via the proof method.

Application of differential induction (see Sect. 5.3) is automated by the dInduct proof method. Conjunctions and disjunctions are split via (h-conji) and (h-disji) (in Isabelle: ). To prove atomic goals \(\left\{ I\right\} \,\{x' = f ~|~ G \}\,\left\{ I\right\} \), our method (1) applies rules (dinv-eq)-(dinv-less) to produce a framed derivative expression (in Isabelle: ), and (2) calculates derivatives using the laws (1)-(7) (i.e. below), substitution laws, and basic simplification laws. This yields derivative-free equality or inequality predicates. The method uses only the simplifier for calculating invariants, and so it is both efficient and yields readable VCs.

For cases requiring deduction to solve the VCs, we have implemented , which applies expr-auto after dInduct, plus further simplification lemmas from HOL-Analysis. Ultimately such heuristics should be based on decision procedures [10, 17, 33, 42], as oracles or as verified components.

Should fail, our methods use the vector derivative laws from Isabelle’s ODEs library [35, 50]. These are more interactive methods as users need to provide the derivatives of both sides of the (in)equality. Yet, this provides more fine-grained control and makes the tactics more likely to succeed.

While suffices for simpler examples, differential induction must often be combined with weakening and cut rules. These rules have been explained elsewhere [50, 61]. This process is automated by a search-based proof method called . The following steps are executed iteratively until all goals are proved or no rule applies: (1) try any fact labelled with attribute facts, (2) try differential weakening to prove the goal, (3) try differential cut [58] to split it into two differential invariants, (4) try . The rules are applied using backtracking so that if one rule fails, another one is tried.

The method is called by dInv, which we applied in Sect. 2. The method allows us to prove a goal of the form \(\left\{ P\right\} \,\{x' = f ~|~ G \}\,\left\{ Q\right\} \) by supplying an assertion I, and proving that this is an invariant of \({\{x' = f ~|~ G \}}\) and also that \(P \Rightarrow I\). This method also requires us to apply differential cut and weakening laws.

Finally, the differential ghost law (dG) is automated through the dGhost proof method. We have complemented these tactics with sound rules from differential dynamic logic. Together with the tactics described in this Section, they enable users to seamlessly prove properties about hybrid systems in the style of \(\textsf{d}\mathcal {L}\). Yet, users of the general-purpose prover can also use the interactive style provided by Isabelle’s Isar scripting language [49]. See Sect. 8.2 for an example where our tactics largely automate a proof of invariance.

To culminate this section, we lay the foundations for further automating the verification process in our framework. Both and methods cannot certify complex real arithmetic proof obligations after discharging any derivative-related intermediate steps. In many cases, this requires determining the local minima and maxima of expressions and using them for further argumentation. A well-known application of differentiation is the analysis of real-valued functions: determining their local minima and maxima or where they are increasing or decreasing. Optimisation problems in physics and engineering frequently require this kind of analysis. Behind it, there are two key results generally called the first and second derivative tests. We formalise and prove these basic theorems in Isabelle/HOL, setting the foundation for automatic certification of the analysis of real-valued functions (see Sect. 8.3). We start by defining increasing/decreasing functions and local extrema:

We also prove simple consequences of these definitions on closed intervals [a, b] denoted in Isabelle as . For instance, we prove the transitivity of the increasing and decreasing properties over consecutive intervals and their relationship to local extrema. We exemplify some of these results below and refer to our repository for all proved properties.

Crucially, the proofs of all these results only require unfolding definitions and calling Isabelle’s auto proof method and Sledgehammer tool [53] to discharge the last proof obligation. We then use our definitions of increasing and decreasing functions to state and prove the first derivative test. It states that if the derivative of a function is greater (resp. less) than 0 over an interval T, then the function is increasing (resp. decreasing) on that interval. The simple 2-line proof above uses an intermediate lemma hiding our full proof of this basic result.

For the second derivative test, we formalise a frequently used property of continuous real-valued functions. Namely, that if a function maps a point t to some value above (resp. below) a threshold c, then there is an open set around t filled with points mapped to values above (resp. below) the threshold. This result and similar ones in terms of open balls with fixed radius around t appear in our formalisations. For these, we also complement Isabelle’s library of topological concepts with the definition of neighbourhood and some of its properties and characterisations.

Finally, the second derivative test states that if the derivative of a real-valued function is 0 at a point t, and its second derivative is continuous and positive (resp. negative) at t, then the original function has a local minimum (resp. maximum) at t.

As before, we provide the complete argument in the proof of our lemmas and . We refer interested readers to our repository for complete results. Sect. 8 provides an example where we use these derivative tests to reason about real-arithmetic properties and establish the progress of a dynamical system. Beyond that, this subsection showcases the openness of our framework. Anyone can formalise well-known analysis concepts that provide background theory engineering to increase proof automation or that generalise extant verification methods.

We have presented various tactics that increase proof automation for hybrid systems verification in our framework. The automation supports both, solution and invariant-based reasoning. The definition of the tactics and their testing covers more than 500 lines of Isabelle code. From these 500 lines, the tactics setup (definitions and lemmas) comprises approximately 200 lines. This number does not take into account our described formalisations. The tactics have simplified our verification experience by discharging certifications of the uniqueness of solutions or differential inductions. We have used them extensively in a set of 66 hybrid systems verification problems. See Sect. 7 for more details.

Our first problem illustrates the integration of all our features for ODEs. It describes the preservation of \(I \Leftrightarrow d_1^2 + d_2^2 = w^2\cdot p^2\wedge d_1=-w\cdot x_2\wedge d_2=w\cdot x_1\) for the ODEs \(x_1'=d_1, x_ 2'=d_2, d_1'=-w\cdot d_2, d_2'=w\cdot d_1\). Observe that the relationship between \(d_1\) and \(d_2\) in the system of ODEs is similar to that of scaled sine and cosine functions. Moreover, the invariant states a Pythagorean relation among them. Thus, we can expect the flow to involve trigonometric functions and the problem to be solved with differential invariants in \(\textsf{d}\mathcal {L}\) due to its previously limited capabilities to explicitly state these functions [29]. Indeed, differential induction in Isabelle/HOL can prove this example in one line:

In the proof above, the application of the lemma as an introduction rule splits the Hoare-triple in three invariant statements, one for each conjunct. The semicolon indicates to Isabelle that the subsequent tactic should be applied to all emerging proof obligations. Therefore, our tactic implementing differential induction for equalities (dinv-eq) is applied to each of the emerging invariant statements, which concludes the proof.

Nevertheless, we can also tackle this problem directly via the flow. Despite the fact that we suspect that the solutions involve trigonometric functions, obtaining the general solution is time-consuming. Therefore, we call our integration between the Wolfram language and Isabelle/HOL to provide the solution for us. We can use the supplied solution in the proof.

The first line of the proof applies our tactic with the suggested solution from . The solution’s syntax specifies one expression per variable in the system of ODEs. As explained in Sect. 6, the tactic applies the rule (wlp-flow), certifies that the corresponding vector field is Lipschitz-continuous by calling our tactic , and certifies that it is indeed the solution to the system of ODEs via our tactic . The command allows us to specify the name of the variables in the proof obligation so that we can use those names in our subsequent tactics. Our new tactic simplifies powers in the monomial expressions of the proof obligation. In the next line, our tactic calls twice but reorders factors in the order of its inputs and . The last line supplies the lemma (below) whose proof was provided by Sledgehammer [53].

This example shows the versatility of using general-purpose proof assistants for hybrid systems verification. Users can provide automation methods for invariant or flow certification. This allows the integration of unverified tools into the verification process. Fast certification enables ITPs to quickly validate CAS’ inputs. In terms of our contributions, this example showcases our shallow embedding’s intuitive syntax, our integration of the Wolfram language for suggesting simple solutions, and our tactics automating VCG, C1-lipschitz continuity, derivatives certification, and real-arithmetic reasoning.

We prove that the inequality \(I\Leftrightarrow x_1^4\cdot x_2^2 + x_1^2\cdot x_2^4 - 3\cdot x_1^2\cdot x_2^2 + 1 \le c\) is an invariant of the systemwhere we abuse notation and “equate” the vector field with its representation as a system of ODEs. In contrast with the previous benchmark, the solution to this system of ODEs is not easy to describe analytically. The following is a subexpression to the solution for \(x_2\) according to Wolfram \(\mid \)AlphaThe solution for \(x_2\) involves another four factors with integrals of fractions with denominators having square roots of square roots. Instead of computing these solutions and certifying them in Isabelle, we perform differential induction. We show that I is an invariant by proving that the framed Fréchet derivatives on both sides of the inequality are 0. In Isabelle/HOL, certification of this reasoning is automatic due to our tactic.

Although the problem is simpler through differential induction, readers should be aware that the simplicity of proving this invariance in Isabelle benefits greatly from our increased automation. We describe below the automated steps to conclude the proof. Thus, our tactic hides various logical, algebraic, differential and numerical computations and certifications. This example showcases the scalability of hybrid systems verifications in interactive theorem provers. Namely, with adequate tactic implementations, ITPs become more automated tools and easier to use over time.

Consider a rocket’s vertical liftoff and assume it loses fuel at a constant rate of \(k>0\) kilograms per second starting with \(m_0>k\) kilograms while its acceleration is equal to the amount of fuel left in it. These assumptions do not accurately model rockets’ liftoff; however, they suffice to produce a behaviour approximating the observed phenomena, see Fig. 2, and facilitate the presentation of our contributions. The corresponding system of ODEs and its solution are

where m is the fuel’s mass, v is the rocket’s velocity, y is its altitude, and t models time.

We study the rocket’s behaviour before it reaches a maximum altitude with its first-stage propulsion because the second stage should begin before the rocket starts falling. We therefore prove two things about the initial propulsion stage. The first is that no matter which height h we consider strictly below the maximum altitude \(H=2m_0^3/(3k^2)\), there will always be a state of the rocket greater than h approaching H. The second is that all scenarios with a single propulsion from the ground lead to altitudes lower than H. Using the abbreviations “ ” for f and “ ” for \(\varphi \), the verification of the first specification is now possible thanks to our implementation of forward diamonds.

The proof starts with the law (fdia-flow) using the lemma asserting that \(\varphi \) is the flow for f. The proof of this is now automatic due to our tactic . The second line of the proof for our specification culminates with some arithmetical reasoning, where we provide the time \(2m_0/k\) as the witness for the existential quantifier in the law (fdia-flow). That is, the time for the second 0-intercept of the velocity when the maximum altitude is reached.

The second specification looks equally simple and its three line proof is deceiving (see below). Our contributed tactics automatically handle VCG, derivative certifications, and uniqueness. However, as reported in Sect. 7, emerging arithmetic proof obligations often have to be checked separately. We do this with the lemma proved using our derivative tests from Sect. 6.7.

Our proof of analyses the altitude behaviour to the left ( \(x\le 2m_0/k\)) and right ( \(x> 2m_0/k\)) of the maximum altitude. Using the first derivative test, we show that, to the left, the altitude is increasing, and to the right, it is decreasing. Thus, the rocket achieves a maximum altitude at \(\langle 2m_0/k,2m_0^3/(3k^2)\rangle \). Accordingly, we repeat our use of the derivative test to show that the velocity remains above 0 in the interval \([0,2m_0/k]\).

This example illustrates the relevance of our additions of forward diamonds and derivative tests. The diamonds allow us to do reachability proofs and show progress for hybrid systems. The tests enable us to prove emerging real-arithmetic proof obligations after VCG and provide the basis for increasing automation in this subtask of the verification process.

We have showcased various examples illustrating the automation added to our hybrid system verification framework. We refer readers interested in more examples using, for instance, our integration of vectors and matrices to previous publications and our participation in ARCH competition reports [21, 34, 45, 47].