# Synchronous Programming with Refinement Types

Jiawei Chen  University of MichiganUnited States ,  José Luiz Vargas de
Mendonça  University of MichiganUnited States ,  Bereket Shimels Ayele  Addis
Ababa Institute of TechnologyEthiopia ,  Bereket Ngussie Bekele  Addis Ababa
Institute of TechnologyEthiopia ,  Shayan Jalili  Ford Motor CompanyUnited
States ,  Pranjal Sharma  University of MichiganUnited States ,  Nicholas
Wohlfeil  University of MichiganUnited States ,  Yicheng Zhang  University of
MichiganUnited States and  Jean-Baptiste Jeannin  University of MichiganUnited
States

(Date: June 2024)

###### Abstract.

Cyber-Physical Systems (CPS) consist of software interacting with the physical
world, such as robots, vehicles, and industrial processes. CPS are frequently
responsible for the safety of lives, property, or the environment, and so
software correctness must be determined with a high degree of certainty. To
that end, simply testing a CPS is insufficient, as its interactions with the
physical world may be difficult to predict, and unsafe conditions may not be
immediately obvious. Formal verification can provide stronger safety
guarantees but relies on the accuracy of the verified system in representing
the real system. Bringing together verification and implementation can be
challenging, as languages that are typically used to implement CPS are not
easy to formally verify, and languages that lend themselves well to
verification often abstract away low-level implementation details. Translation
between verification and implementation languages is possible, but requires
additional assurances in the translation process and increases software
complexity; having both in a single language is desirable. This paper presents
a formalization of MARVeLus, a CPS language which combines verification and
implementation. We develop a metatheory for its synchronous refinement type
system and demonstrate verified synchronous programs executing on real
systems.

##  1\. Introduction

Much of the software we encounter, for example in automobiles, airplanes, or
appliances, may interact with its physical environment, and thus are cyber-
physical systems (CPS). Many CPS, such as those controlling vehicles or
industrial processes, may pose great risk of harm in the event of a software
failure. The development of safe CPS is therefore essential but is complicated
by the difficulty of testing such systems, since their physical nature makes
it difficult to exhaustively test all possible system and environmental
configurations.

To this end, formal verification is an attractive approach that can be used to
ascertain system safety. Hybrid automata (Alur et al., 1993) are commonly used
to model CPS, though they do not directly represent executable programs. Other
work in verifying CPS include Kind (Hagen and Tinelli, 2008) and Kind 2
(Champion et al., 2016), which generate invariants for discrete-time
synchronous programs using an incremental, bounded SMT-based approach.
Although formal verification is more thorough than testing, it carries its own
set of challenges. Mainstream programming languages common in CPS and embedded
software development are challenging to verify, as their semantics are often
not well-defined or precise enough. On the other hand, languages primarily
designed for formal verification might abstract away too many implementation-
level details of the original system to generate executable programs (Platzer,
2008; Alur et al., 1993). Translation between verification and execution
languages is possible but may introduce bugs of its own if unable to capture
subtleties of the original system (Malecha et al., 2016). Verified translation
is possible (Bohrer et al., 2018), though translation of any kind adds
complexity to the development and debugging workflow. Combining verification
and execution into a single programming language avoids some of the
compromises of either approach, giving CPS developers the assurance that the
properties they verify carry over to the real system.

The idea of languages that permit both verification and execution is not new;
indeed, projects like Koord (Ghosh et al., 2020a), VeriDrone (Malecha et al.,
2016) and VeriPhy (Bohrer et al., 2018) offer verification and execution of
CPS, with special consideration given towards ensuring run-time behavior
reflects what was verified. In Koord, multi-agent robotics systems are modeled
in a language with formal semantics that allows direct verification and
simulation. Programs can execute via a middleware layer (Ghosh et al., 2020b)
that replicates shared variables and interfaces with platform-specific
controllers on real robots. System evolution follows a round-based approach
that alternates between system and environment evolution, solving the common
issue of synchronizing logical with physical time in a hybrid system model
(Ghosh et al., 2020a). VeriPhy (Bohrer et al., 2018) describes a method for
constructing CPS models and specifications in differential dynamic logic (dL)
that can be soundly translated into a runtime monitor. This allows the safe
mixing of a more optimal, but perhaps occasionally unsafe controller, with a
safer alternative, though the method assumes such a safe controller exists. In
comparison the present work focuses on compile-time verification of safety
properties directly within an executable CPS language.

One approach to compile-time verification is to encode desired properties in
the language’s type system. As a result of the Curry-Howard-Lambek isomorphism
relating data types to propositions, a derivation of said augmented type
directly implies the provability of the property. Dependent- and refinement-
type systems such as that of F* (Swamy et al., 2016) or Liquid Haskell (Jhala
and Vazou, 2020), introduce predicate constraints on the program’s terms, and
thus allow one to statically reason about a program’s runtime behavior. A
series of syntax-directed type-checking rules can then be used to generate
constraints for a given program and its specification, the validity of which
implies satisfaction of the specification.

This paper presents a formalization of the MARVeLus (Method for Automated
Refinement-type Verification of Lustre) type system. In existing work (Chen et
al., 2022), typing rules for MARVeLus were proposed, along with an
implementation of a verified robot collision avoidance controller with
stationary obstacles. However, a proof of type safety had yet to be developed
for this language. In this paper, we present the following enhancements to
MARVeLus over existing work (Chen et al., 2022):

  1. (1)

A formalization of MARVeLus, introducing more precise operational semantics
based on comparable synchronous languages, the introduction of a subset of
Linear Temporal Logic (LTL) trace predicates for type specifications(Colaço et
al., 2006; Parissis, 1996; Caspi and Pouzet, 1996; Ratel, 1992; Caspi and
Pouzet, 1998), and adjustments to the existing type system to enable a proof
of type preservation;

  2. (2)

A definition and proof of type preservation for the synchronous refinement
type metatheory;

  3. (3)

Improved experimental methods supporting dynamic obstacles, such as collision
avoidance when following a moving vehicle.

We are primarily focused on the correct formalization of a type-safe
executable synchronous programming language. Although existing works present
proof automation (Boulmé and Hamon, 2001) or invariant generation techniques
(Champion et al., 2016) for similar languages, we note that these developments
are orthogonal to our present goals.

This paper is organized into five main parts. Section 2 introduces the
MARVeLus language and presents a motivating example. Section 3 covers
preliminary concepts and methods employed by MARVeLus for verification.
Sections 4, 5, and 6 respectively describe the syntax, semantics, and type
system that comprise our improved formalism for MARVeLus, including a
definition for type preservation in synchronous programs. Sections 7 and 8
detail the implementation of MARVeLus atop an existing synchronous language.
Finally, Sections 9 and 10 present the methods employed to execute MARVeLus on
hardware, including an experiment with physical robots. We then conclude with
a discussion of related work and future extensions.

##  2\. Overview

MARVeLus enables CPS developers to verify and deploy programs to real-world
CPS. By leveraging the existing synchronous program simulation and compilation
infrastructure of Zélus (Benveniste et al., 2011), the language benefits from
the great care already taken in ensuring its accuracy in modeling synchronous
programs (Benveniste et al., 2014; Bourke and Pouzet, 2013). To this, we add
automated verification of program properties expressed as type annotations
inspired by refinement types (Rondon et al., 2008; Vazou et al., 2014).

###  2.1. A Simple Industrial Controller

We present a simplified verification and implementation workflow to illustrate
how one might use the MARVeLus extensions in designing CPS software. Suppose
one wants to design an industrial controller responsible for maintaining the
liquid level in a tank, similar to the scenario described by Kamburjan
(Kamburjan, 2021). The tank has a maximum capacity of $20\text{\,}\mathrm{L}$
and a fixed outflow rate of $0.1\text{\,}\mathrm{L}\mathrm{/}\mathrm{s}$. We
require that the tank level stays within $1\text{\,}\mathrm{L}$ and
$19\text{\,}\mathrm{L}$ to prevent the tank from completely emptying or
overflowing. The controller switches a solenoid valve, which can only either
be completely open or closed, and can deliver
$0.5\text{\,}\mathrm{L}\mathrm{/}\mathrm{s}$ when open. We design the
controller so that it opens the valve when the tank level drops below
$1.5\text{\,}\mathrm{L}$ and closes the valve when it exceeds
$18.5\text{\,}\mathrm{L}$, to afford a $0.5\text{\,}\mathrm{L}$ safety margin.
For the sake of simulation, we assume this is a discrete-time system, with a
constant time step of $0.1\text{\,}\mathrm{s}$.

⬇

1let dt:{v:float | v > 0.} = 0.1

2let maxflow:{v:float | v > 0.} = 0.5

3let outflow:{v:float | v > 0.} = 0.1

4let minlevel:{v:float | v > 0} = 1.

5let maxlevel:{v:float | v > minlevel} = 19.

6let node exec () : {(vf:float)*(vl:float) | true} =

7 let rec ((flow, level):{(f:float)*(l:float) |

8 ((l >= minlevel && l <= maxlevel) &&

9 ((l <= (maxlevel -. dt *. (maxflow -. outflow)) && f = maxflow)

10 || (l >= (minlevel +. dt *. outflow) && f = 0.)))}) =

11 (0., 15.) fby

12 ((if (level <= (minlevel +. 0.5)) then maxflow else

13 (if (level >= (maxlevel -. 0.5)) then 0. else flow)),

14 (level +. (flow -. outflow) *. dt) models (robot_get ("level")))

15 in (() models robot_str ("flow", flow)); (flow, level)

Figure 1. The industrial controller code with added refinements and external
interfaces

A verified MARVeLus implementation is shown in Fig. 1. Lines 1-5 define system
constants such as the time step, maximum flow rate, and the tank’s outflow
rate. We refine these variables with type annotations, such as assuming they
are positive, and that the maximum tank level must be greater than the minimum
level. Lines 11-14 describe the state variables and their evolutions as a
stream of tuples, of which each element represents the flow rate and liquid
level at each instant. The type annotation on the tuple requires that both
elements are floats, and that together they satisfy the conditions given in
Lines 8-10. Note that we use f and l to refer to the first and second elements
of the tuple to distinguish them from their instantiations in the remainder of
the program.

The safety condition is specified on Line 8, requiring that the tank level
always remain between minlevel and maxlevel. However, this specification alone
is not sufficiently strong to verify the system, as it is not inductive. That
is to say, proving the satisfaction of the safety specification now does not
allow one to prove safety for the next time interval. Provided only this
specification, the verifier produces counterexamples, even if they are not
physically feasible. For instance, if the liquid level is at exactly
$19\text{\,}\mathrm{L}$ and the valve was open in the previous instant, the
controller cannot respond quickly enough to close the valve before the tank
overflows. However, we know that the system has started in a safe state, and
that the controller will not have allowed the liquid level to reach
$19\text{\,}\mathrm{L}$ with an open valve. Therefore, we must specify an
additional invariant (Lines 9-10) to assume that the controller will have made
the correct decision in the previous instant. Specifically, we assume that the
controller in the previous instant has left us with at least one time step to
react and prevent an unsafe condition. By inspecting the controller code, one
can assure themselves that this assumption is indeed satisfied. The verifier
can then use this fact to check that the controller will continue to make the
correct decision in the next instant, thus proving the property inductively.

Line 11 sets the initial condition of the system; we assume the tank level
begins at $15\text{\,}\mathrm{L}$ and the valve is initially closed. Lines
12-13 describe the controller’s behavior and its effect on the commanded flow
rate. The system reacts if the level approaches the limits and otherwise
retains the previous flow rate. Line 14 then evolves the physical system,
simulating the tank’s liquid level based on inflow and outflow rates, or
retrieving the actual tank level from a sensor labeled “level”. We use the
models syntax to separate the simulation model (on the left) and the actual
implementation (on the right); only the left side is verified, and we assume
that the supplied model accurately reflects the real system dynamics. Line 15
then publishes the commanded flow rate to an actuator labeled “flow”, and
returns the flow rate and level to be used in other parts of the program.

##  3\. Preliminaries

###  3.1. Synchronous Programming

Synchronous programming treats all program data as streams which may take on
different values at any given moment. Program computations are treated as
manipulations to these streams to influence their evolution in time. Streams
are well-suited for modeling embedded systems, which often handle streams of
inputs and outputs in real time (Florence et al., 2019). For example, an
autonomous vehicle must constantly interpret sensor data and produce control
commands in a timely fashion to avoid an accident. Synchronous programming has
gained significant traction in industry, where tools such as SCADE (a
derivative of Lustre) (Colaço et al., 2017) and Esterel (Boussinot and de
Simone, 1991) have been entrusted with designing integrated circuits,
avionics, and other critical systems. Thus, a verified synchronous language
has the advantage of familiarity for eventual industrial adoption.

Synchronous programming observes logical time, in which a clock cycle is
determined by certain actions or events involving the system, which may be
decoupled from physical (“wall-clock”) time. All computations in a synchronous
program must finish before the next clock cycle; thus, they are synchronized
by this basic unit of time. This lends itself well to the design of embedded
systems, as the data-flow model of synchronous programming closely resembles
the flow of signals in electronic circuits (Halbwachs et al., 1991a) and
imposes time constraints on computations. A complication that arises from
combining software with the physical environment is the reconciliation of
logical and physical clocks. In this paper, we focus only on discrete systems
and reserve the examination of verifying systems spanning these two time
domains for future work, noting that significant work has already gone into
accurately simulating hybrid programs in Zélus (Benveniste et al., 2011). We
discretize the dynamics and clock our synchronous program at the rate of
discretization. Since MARVeLus is primarily concerned with the types of
streams and the values they emit, we assume that all streams have compatible
clocks, a property already statically verified by the Zélus compiler.

Another useful property of synchronous programs is that they operate in
bounded memory (Bourke and Pouzet, 2013; Caspi et al., 1987), which limits the
number of previous state values that are allowed to be observed at any time.
This precludes, for instance, the arbitrary storage of sensor values, and
makes memory usage more predictable. This is especially important for embedded
systems, which often have limited computational resources. By construction,
streams can only access a fixed number of previous states to derive the next
state.

Lustre, and by extension Zélus, also observe a notion of causality, meaning
that a program may only depend on values available in past cycles, and on
present values in a way that does not produce circular dependencies. For
instance, a stream may not instantaneously depend on its own value in the
current cycle, but may depend on the value of another stream, provided the
other stream does not already depend on it. Causality is a useful property for
a CPS modeling language as it ensures systems created in the language are
physically feasible. Causality is checked statically by the Zélus compiler and
has already been formalized as a dedicated causality-analysis type system in
existing work (Benveniste et al., 2014; Cuoq and Pouzet, 2001), so we
henceforth assume that programs we check already obey causality with respect
to this formalism. To this end, we assume that a term $e$ is always well-typed
in the causality type system (Cuoq and Pouzet, 2001).

###  3.2. Refinement Types

Refinement types enhance the standard type system by allowing types to be
specified using logical predicates that can take values of terms as inputs.
These predicates serve as constraints on the base type such that all terms
that inhabit the refined type satisfy the predicate. For instance, positive
floating-point numbers can be specified using the refinement type ${\\{w:{\sf
float}\ |\ w>0.\\}}$

Refinement types belong to the broader field of dependent types, which are,
generally speaking, types that can depend on the values of terms (Cardone,
2005). Although full dependent type theory has the advantage of expressiveness
(Swamy et al., 2016), refinement types lend themselves well to generating
verification conditions that depend on terms, while remaining decidable if
restricted to the theories of equality, uninterpreted functions, and real
arithmetic (Rondon et al., 2008). As a result, refinement types lose the
expressivity of allowing arbitrary functions in refinements, abstracting away
the bodies of non-arithmetic functions (Rondon et al., 2008), which if
interpreted would jeopardize decidability (Jhala and Vazou, 2020).

###  3.3. Verification Via Typing

Verification via typing relies on the Curry-Howard-Lambek isomorphism to
relate desired program properties (propositions) with types, and thus property
checking becomes type checking (Cardone, 2005). Furthermore, type-checking is
performed statically at compile-time, so verification at this stage in
compilation has the chance to catch bugs in the program before any code is
actually executed. This is particularly attractive to CPS, where testing on a
real system can be difficult, risky, or costly. Verification via typing also
allows our verifier implementation to be modular; all terms still possess a
base type that can be checked using the existing type checker, while terms
augmented with type refinements can provide additional information or
conditions to the verifier. This allows the base Zélus type checker to remain
independent of our additions. Refinement types (Jhala and Vazou, 2020) provide
a method of adding annotations to the type system while maintaining
decidability. An additional benefit of introducing verification through type-
checking is that it promotes modularity in user code; terms that have been
type-checked can then be re-used in other parts of the source code, carrying
with them the proof of safety (Eichholz et al., 2022). This can be especially
important with large and/or long-term projects requiring extensive integration
or regression testing of patches or updates.

##  4\. Syntax

$\displaystyle v~{}::=~{}$ $\displaystyle~{}c$ Literal Values
$\displaystyle|~{}(v_{1},~{}v_{2}...,~{}v_{n})$ Tuples $\displaystyle
e~{}::=~{}$ $\displaystyle~{}v$ Values $\displaystyle|~{}{\sf
let}_{h}~{}(x:\tau)=e_{1}{\sf~{}in~{}}e_{2}$ Local Bindings
$\displaystyle|~{}{\sf let~{}rec}_{h}~{}(x:\tau)=e_{1}{\sf~{}in~{}}e_{2}$
Recursive Bindings $\displaystyle|~{}f~{}x$ Application
$\displaystyle|~{}e_{1}{\sf~{}fby~{}}e_{2}$ Stream Composition
$\displaystyle|~{}{\sf delay}(e)$ Delayed Evaluation
$\displaystyle|~{}(e_{1},~{}e_{2}...,~{}e_{n})$ Tuples of Expressions
$\displaystyle|~{}{\sf if~{}}x_{c}{\sf~{}then~{}}e_{t}{\sf~{}else~{}}e_{f}$
Conditionals $\displaystyle|~{}e{\sf~{}models~{}}r$ Modeling $\displaystyle
r~{}::=~{}$ $\displaystyle~{}{\sf robot\\_{get}~{}}k$ Robot Get
$\displaystyle|~{}{\sf robot\\_{str}~{}}k~{}e$ Robot Store $\displaystyle
d~{}::=~{}$ $\displaystyle~{}{\sf let~{}}f~{}(x:\tau_{1}):\tau_{2}=e$ Named
Function Definition Figure 2. MARVeLus Syntax

The stream syntax (Fig. 2) is modeled around Lustre streams, which forms a
discrete-time subset of the existing Zélus syntax (Benveniste et al., 2011).
Similarly to other synchronous languages (Caspi and Pouzet, 1996), we make the
distinction between values $v$, which are constants emitted by stream
expressions. We introduce a new entry $h$ (“history”) in recursive and non-
recursive local bindings, which embeds a bound variable’s past values into the
syntax. This is essential for our operational semantics as stream expressions
can depend on values that have occurred in the past and thus we may need to
recover those values to re-construct the appropriate derivation tree. A
syntactic sugar we employ is allowing local bindings to be defined without
histories; these are considered uninitialized and are implicitly assigned
empty histories ($h=[]$) Similarly to other refinement type systems (Rondon et
al., 2008; Jhala and Vazou, 2020), we require that certain constructs take
variable arguments (such as function application and conditionals) to simplify
the metatheory by preventing the introduction of arbitrary expressions into
refinement predicates (Jhala and Vazou, 2020). Another syntactic sugar we
employ is to allow certain non-variable terms syntactically considered “safe”
for the refinement logic to be used as argument functions (such as simple
arithmetic expressions and conditionals), which greatly simplifies programs
written in the real-world implementation of the language. We note that Zélus
only supports named function definition at the top-level (Benveniste et al.,
2011), which we replicate.

Some elements of the syntax are not user-facing and are exclusively to support
internal functionality. The ${\sf delay}()$ operator is one such case, which
allows an expression’s evaluation to be deferred for one instant while
preserving its original behavior despite environment updates. Likewise, we
only allow let-bindings (both recursive and non-recursive) without initialized
histories (i.e. $h=[]$) in the user-facing portion of the language. This
ensures prevents arbitrary values from being introduced to histories.

As part of the robotics extensions to Zélus, we introduce built-in keywords to
facilitate reading and writing values to hardware ($r$) as shared variables
labeled by string constants $k$. Additionally, we introduce the syntax ${e\
{\sf models}\ r}$ which allows one to define two implementations for a
stream—a deterministic model for simulation and verification, and the
implementation involving real hardware. As it is impossible to predict or
verify at compile-time the exact outputs produced by real sensors, the CPS
designer is responsible for ensuring that the model accurately represents
actual behavior. In addition to the robotics extensions, we introduce the
syntax necessary to support refinement types in Zélus.

###  4.1. Specification Syntax

The core of the specification syntax (Fig. 3) is derived from similar
refinement type systems (Jhala and Vazou, 2020; Rondon et al., 2008).
Typically, refinement type systems require that refinement predicates come
from decidable logics such as the quantifier-free logic of equality,
uninterpreted functions, and linear arithmetic. We note that allowing
nonlinear polynomial real arithmetic maintains decidability, as shown by
Tarski (Tarski, 1951). We find this addition useful for specifying the
kinematics of physical systems and it is supported by the Z3 solver (de Moura
and Bjørner, 2008).

A type can either be a base type $b$, which represents a stream consisting
solely of values belonging to a particular primitive data type, or refinement
types. Refinement types of the form ${\\{w:b\ |\ \varphi\\}}$ allow one to
specify streams that satisfy a predicate $\varphi$, and introduce a value
variable $w$ which binds to any term inhabiting the type, allowing $\varphi$
to reference terms (Rondon et al., 2008). For example, one may write the type
of non-negative integers as ${\\{w:\sf{int}\ |\ w\geq 0\\}}$. As a natural
extension of standard refinement types, predicates in our refinement type
specifications become streams of Boolean values.

One of our main contributions over existing work (Chen et al., 2022) is
extending the predicate syntax of MARVeLus to explicitly accommodate select
temporal predicates from Linear Temporal Logic (LTL) (Pnueli, 1977). The
refinement predicates discussed thus far form the syntax of “state
predicates”, which in the absence of temporal operators, reason about the
immediate value of a stream at the current instant. To this, we add the
temporal operators “Always” ($\square$) and “Next” ($\ocircle$), along with
the conjunction of predicates containing these operators. This expanded set
comprises the full set of specifications we allow as refinement predicates in
the type syntax. While LTL normally includes other temporal operators along
with disjunction at the top-level, we choose to focus primarily on safety
properties which can be expressed globally (i.e. with $\square$), which allows
proofs to be inductive. In practice this is often sufficiently rich for
describing most desirable behaviors of safety-critical CPS, as these
properties typically require specifying that something either always or never
happens.

$\displaystyle\tau~{}::=~{}$ $\displaystyle
b~{}|~{}\\{v:b~{}|~{}\varphi\\}~{}|~{}\tau\rightarrow\tau$ Types
$\displaystyle b~{}::=~{}$ $\displaystyle{\sf int}~{}|~{}{\sf
float}~{}|~{}{\sf bool}~{}|~{}b_{1}\times b_{2}\times...\times b_{n}$ Base
Types $\displaystyle p,q::=$ $\displaystyle\ {\sf true}\ |\ {\sf false}\ |\ x\
|\ e_{1}=e_{2}\ |\ e_{1}>e_{2}\ |\ p\land q\ |\ \lnot p$ State Predicates
$\displaystyle\varphi,\psi::=$ $\displaystyle\ p\ |\ \square\varphi\ |\
\ocircle\varphi\ |\ \varphi\land\psi$ Trace Predicates Figure 3. Refinement
Type Syntax, where we note that $e_{1},e_{2}$ are terms within the logic of
quantifier-free equality, uninterpreted functions, and arithmetic (QF-EUFA)

##  5\. Stream Semantics

MARVeLus programs operate on streams of data, producing values at each
instant. Although the streams themselves do not terminate, they may emit a
value at a given instant representing the stream’s current state. Lustre’s
clock calculus allows streams that do not emit values on all clock cycles
(Halbwachs et al., 1991b), but we currently consider only streams that are
compatible with the basic clock, i.e. streams that always emit a value on
every cycle of the most frequent clock.

We describe the operational semantics of MARVeLus with the judgement
$S;~{}\sigma\vdash e\stackrel{{\scriptstyle v}}{{\hookrightarrow}}e^{\prime}$,
which represents the stream $e$ in stream context $\sigma$ and function
context $S$ that simultaneously transitions into the new stream $e^{\prime}$
and emits a value $v$ at each clock cycle. Similarly to other interpretations
of Lustre semantics (Ratel, 1992), the context $\sigma$ is comprised of
mappings between variables and histories of their past values (Fig. 4). That
is, for any $x\in{\sf dom}({\sigma})$, $\sigma(x)=h$ where
$h=v^{-n}::v^{-n+1}...v^{0}$ is a history of the past values of $x$, up to the
immediately preceding time instant.

$\displaystyle\sigma~{}$ $\displaystyle::=~{}\varnothing~{}|~{}\sigma,x=h$
$\displaystyle S~{}$ $\displaystyle::=~{}\varnothing~{}|~{}S,f(x)=e$
$\displaystyle h~{}$ $\displaystyle::=~{}[]~{}|~{}h::v$ $\displaystyle{\sf
prev}(h::v)$ $\displaystyle\triangleq h$ $\displaystyle{\sf prev}(\sigma)$
$\displaystyle\triangleq\\{{\sf prev}(\sigma(x))~{}|~{}x\in{\sf
dom}({\sigma})\\}$ Figure 4. Definitions for function environment $S$, term
environment $\sigma$, and the histories $h$ of variables bound in $\sigma$

Consistent with the design of Lustre (Halbwachs et al., 1991b), loops and
recursive function calls are excluded. As a result, the evaluation of a stream
$e$ at any instant is terminating, meaning a value $v$ is always emitted on a
transition of $e$.

One of the challenges in deriving operational semantics arose from reconciling
the behavior of recursively-defined streams (${\sf let~{}rec}$) with stream
composition (${\sf fby}$). In an earlier iteration of the semantics (Chen et
al., 2022), the left and right hand sides of (${\sf fby}$) are evaluated
simultaneously. When a stream depends on its past values, it necessarily
employs fby to both initialize the stream and delay self-references so that
they do not result in unbounded recursion. For example, in the program ${\sf
let\ rec}\ {x=0\ {\sf fby}\ x+1}\ {\sf in}\ {x}$, $x$ is defined initially as
0, and then for all subsequent instants is defined as the sum of 1 and the
past value of $x$. This is not straightforward to characterize in a syntax-
guided manner. Part of the reason is that, when evaluating $0\ {\sf fby}\
x+1$, the notion of the left-hand side becoming the initial value of $x$ is
lost. This information is only known at the level of the recursive let-
binding. This is problematic if the left and right sides of $0\ {\sf fby}\
x+1$ must be evaluated together, because $x+1$ cannot be computed unless $x$
is known to be initially $0$, which is not known until $0\ {\sf fby}\ x+1$ is
fully evaluated! In other (non-operational) semantics (Caspi and Pouzet, 1998,
1996), this was in part resolved by deferring the computation of the right-
hand side of fby (or its semantic equivalent). However, simply deferring the
computation reveals a new problem: if the deferred expression contains free
variables that have updated since the delay occurred, the behavior of this
expression will change so that it no longer behaves like a properly delayed
version of itself. Prior semantics address this by either storing intermediate
values for delayed terms (akin to a buffer) (Caspi and Pouzet, 1998), or by
leaving variables symbolic (Caspi and Pouzet, 1996). Our operational approach
takes inspiration from the former, in that local bindings maintain a history
of their variables’ past values so that deferred computations can refer back
to the states of variables from the time before the delay occurred. Finally,
one more issue to address is preserving this history in a syntactical manner.
At each time instant, the operational semantics for the next step is derived
independently as a new derivation tree. As such, the derivation needs to be
re-populated with the past values of variables from the previous derivation so
that the histories of variables can be recovered. This motivated the changes
we made to the semantics of fby and let-bindings, and is essential for a
syntax-directed operational semantics.

###  5.1. Summary of Stream Behaviors

Drawing inspiration from Lustre and Esterel (Ratel, 1992; Parissis, 1996;
Colaço et al., 2006), we define the operational semantics of MARVeLus in Fig.
LABEL:fig:streamsemantics

  1. (1)

Constant Streams: These are literals lifted from the base language; they
return a fixed value each instant. Lustre treats all primitives as constant
streams (i.e. 5 in Lustre is the constant stream that always emits 5) (Caspi
et al., 1987), and we adopt this convention as well.

  2. (2)

Variables: Variables return the most recent value bound to it in $\sigma$. A
variable $x$ steps to $x$ because variables themselves do not update; instead
their entry in $\sigma$ is updated at each time instant to reflect the value
of the stream to which the variable was originally bound; this update is
performed by (S-LET) and (S-LETREC), the two places where new variables are
bound.

  3. (3)

Pointwise Applications of Functions to Argument Streams: Similarly to how a
function can be mapped over an array, we define the pointwise application of a
named function $f$ on an argument variable $x$ as $f~{}x$, the resultant
stream being $f$ applied to the most recent value bound to $x$. Functions are
imported from the non-stream base language and are assumed to be well-typed
with respect to that language. The semantics are defined by the rule (S-APP).

  4. (4)

Compositions of Streams: Lustre and Zélus allow a stream to be “attached” to
another via $s{\sf~{}fby~{}}t$ (pronounced “followed-by”), resulting in a new
stream consisting of the initial value of $s$ followed by the stream $t$
delayed by one clock, i.e. $s_{0},~{}t_{1},~{}t_{2},...$. The behavior of
${\sf~{}fby~{}}$ is defined by the rule (S-FBY). When the expression
$e_{1}{\sf~{}fby~{}}e_{2}$ is evaluated, it emits the value that $e_{1}$ emits
when it is evaluated, and then rewrites to ${\sf delay}(e_{2})$. While
intuitively one may think the result should simply be $e_{2}$, as the purpose
of ${\sf fby}$ is to defer computation of the second computation, it is
possible that free variables occur in $e_{2}$. This requires special treatment
because the values of these free variables may have updated during the
previous evaluation, and so $e_{2}$ evaluated in the current instant may not
produce the same values it did in the previous instant. The intent of
${\sf~{}fby~{}}$ is to “delay” the second expression by one instant, so that
it produces the same values it would have had it not been delayed, but one
instant later. Essentially this “shifts” its behavior in time while also
accounting for variables that may be assigned new values in the meantime. This
operation could only be done through a special ${\sf delay}()$ operator and
corresponding (S-DELAY) semantics, which bridges the past and the present to
allow expressions and their behaviors to be preserved in a newer context.

  5. (5)

Delaying Streams: Streams that are delayed by ${\sf fby}$ may contain
variables which were bound outside the scope of the ${\sf fby}$. Consider the
program in Fig. 5(a). Note how the variable $y$ is used inside the scope of a
${\sf fby}$ (in $x+y$), but $y$ is bound outside the scope of this delay. This
means that $y$ is continually assigned new values by the evaluation of
$0{\sf~{}fby~{}}1$, which is not under a delay. If ${\sf fby}$ simply deferred
evaluation of $x+y$ without considering that variables will have updated in
the meantime, the first evaluation of $x+y$ will have skipped the initial
value of $y$, putting $x$ and $y$ out of sync with one another. Furthermore,
$x$ will instantaneously depend on itself. Therefore, evaluation of ${\sf
fby}$ is accompanied by ${\sf delay}$, which re-evaluates expressions in the
previous context. Because previous values of variables in $\sigma$ are
retained in ${\sf let}$ and ${\sf let~{}rec}$, the only places that bind new
variables, it is possible to “rewind” $\sigma$ to previous states simply by
removing the last value from each entry. In other words, the previous
$\sigma$, ${\sf prev}({\sigma})$ is always completely recoverable from
$\sigma$. This is encapsulated by ${\sf prev}()$ operator (Fig. 4). Variables
that are delayed are guaranteed to have a value available in its corresponding
context, since they are updated at least as many times as ${\sf delay}$ is
applied through (S-FBY), since each delay will have been accompanied by an
evaluation of the outer sub-expression which bound the variable. Therefore, it
is impossible to revert $\sigma$ to a state before the “beginning of time” for
a program.

  6. (6)

Robot-Specific Expressions: The “robot expressions” robot_get, robot_str, and
models serve to connect the rest of the semantics with real-world hardware and
are largely semantically transparent, with the exception of combining ${\sf
robot\\_{get}}$ with ${\sf models}$ when a program is running in “robot mode”.
In this mode, the program takes in real sensor values using ${\sf
robot\\_{get}}$. Since it is impossible to predict the values supplied by
real-world sensors and because ${\sf robot\\_{get}}$ can only be present on
the right-hand side of ${\sf models}$, ${\sf robot\\_{get}}$ as well as ${\sf
models}$ expressions in robot mode have no operational semantics. A ${\sf
models}$ expression while not in robot mode (as indicated by the side
condition) is completely transparent to the underlying stream expression, and
thus takes on identical semantics. ${\sf robot\\_str}$ is assumed to always be
a successful write operation performed on a piece of robot hardware, but has
no other effect on the MARVeLus program.

                    let rec x =
                  (let y = 0 fby 1 in (0 fby x+y))
                  in x

(a) A program that contains variables used inside the scope of ${\sf fby}$

${x}$${0}$${1}$${2}$${3}$${4}$${5}$${\ldots}$${y}$${0}$${1}$${1}$${1}$${1}$${1}$${\ldots}$
(b) Improperly delayed variables. The arrows represent the values of $x$ and
$y$ that are used when computing the next value of $x$. Note how the first
value of $y$ is skipped in computing $x+y$

${x}$${0}$${0}$${1}$${2}$${3}$${4}$${\ldots}$${y}$${0}$${1}$${1}$${1}$${1}$${1}$${\ldots}$
(c) Properly delayed variables. No values of $y$ are skipped when computing
$x+y$.

Figure 5. Traces of the variables $x$ and $y$ in a stream program (5(a)), if
the variables are improperly (5(b)) and properly (5(c)) delayed

  7. (7)

Stream Recursion: Streams can be defined recursively in terms of themselves. A
stream ${\sf let\ rec}\ {x=e_{1}}\ {\sf in}\ {e_{2}}$ can be constructed where
$x$ may occur in $e_{1}$ under special circumstances. Although recursively
defined streams syntactically resemble recursive definitions in conventional
languages by also using the ${\sf rec}$ keyword, their semantics are entirely
different. As with Lustre, MARVeLus considers variables to be identically
equal to their definitions (Halbwachs et al., 1991a). Consequently, one must
be mindful of circular dependencies in definitions. Streams must not be
defined in terms of their current values, as one may produce contradictions
(${\sf let\ rec}\ {x=x+1}\ {\sf in}\ {x}$) or nondeterministic behavior (${\sf
let\ rec}\ {x=x}\ {\sf in}\ {x}$). Both scenarios fall under the category of
“instantaneous dependencies” since the value of $x$ at the current instant
cannot be determined as it depends on its current value. These are not well-
formed programs and are statically rejected. As such, (S-LETREC) allows the
evaluation of $e_{1}$, whose value will determine the current value of $x$ to
reference $x$ up to and including its previous value, but not its current
value. A ${\sf nil}$ is inserted at the end of $\sigma(x)$ since the last
position is reserved for the current value of a variable (which is yet to be
determined). The evaluation of $e_{2}$ is then allowed to reference the
current value of $x$, as one would expect in a local binding. Recursively
defined streams must delay references to themselves using the ${\sf fby}$
keyword, which also serves to define the stream’s initial value(s). This
ensures that streams are causal, depending on strictly prior values. The
stream ${\sf let\ rec}\ {x=0\ {\sf fby}\ x+1}\ {\sf in}\ {x}$ is well-formed,
because the recursive reference to $x$ in its definition occurs behind a
delay. This stream initially produces the value $0$, and then for all
subsequent evaluations produces a value one more than its previous value. The
variable $x$ is annotated with a type $\tau$ to simplify type checking and
this type is likewise “stepped” to reflect the behavior of $x$ in subsequent
instants. The operator ${\sf tl}()$ along with the semantics of “stepping”
types is described in Section 6.

  8. (8)

Local Bindings: This expression type is similar to that of stream recursion,
with the exception that the evaluation of $e_{1}$ must not depend on $x$, as
this is not a recursive definition. Otherwise, all other behaviors, including
stepping the type annotation of $x$, are the same.

  9. (9)

Branching: Branching in MARVeLus behaves similarly to a multiplexer in a
digital circuit, in that the conditional selects the value of one of the two
streams to emit. The stream ${\sf
if~{}}x_{c}{\sf~{}then~{}}e_{t}{\sf~{}else~{}}e_{f}$ takes the current value
of the “true” branch $e_{t}$ or the “false” branch $e_{f}$ depending on the
truth value of $x_{c}$. As before, we assume all three streams have compatible
clocks. The two rules (S-IF-T) and (S-IF-F) correspond respectively to the
cases when $x_{c}$ emits true or false, and thus whether the stream emits the
value of $e_{t}$ (thus emitting $v_{t}$) or $e_{f}$ (thus emitting $v_{f}$).
The conditional does not affect the behavior of the branches themselves; the
branch not taken will transition as well as reflected in the rules. This
prevents the stream that is not selected from delaying indefinitely.

###  5.2. Predicate Semantics

MARVeLus allows one to define predicates in the style of Linear Temporal Logic
(Pnueli, 1977). Adopting the notation of Manna and Pnueli (Manna and Pnueli,
1992), we use $\vDash$ to denote satisfaction of a property over a stream and
$\VDash$ to denote satisfaction over a single state. In this section, we
denote streams $s$ as sequences of values $s_{i}$ for illustrative purposes.
Furthermore, we note that predicates themselves are in fact streams of Boolean
values in our system, with each value representing the predicate’s
satisfaction given the state of the stream at that instant. Since
specifications in MARVeLus are made with respect to the initial definitions of
streams (i.e. before program execution), predicates written by the user are
considered over the entire time period of the program, from the beginning of
program execution onwards.

####  5.2.1. State Predicates

For a state predicate $p$ and stream $s$,
$(s_{i},~{}s_{i+1},~{}s_{i+2},...)\vDash p$ if and only if $s_{i}\VDash p$.

####  5.2.2. Trace Predicates

Trace predicates offer a more holistic view of the stream’s behavior, and we
define a subset of those found in Linear Temporal Logic.

  1. (1)

Globally ($\square$): A property $\square\varphi$ requires that $\varphi$ be
satisfied for all values of a stream beginning at the present instant. That
is,
$(s_{i},~{}s_{i+1},~{}s_{i+2},...)\vDash(\square\varphi)_{i}\iff\forall(j\geq
i)\ .\ s_{j}\VDash\varphi_{i}$. Verification of these predicates in MARVeLus
is handled via induction; the left- and right-hand sides of a ${\sf fby}$
construct become the initial condition and inductive step, respectively. Since
refinement predicates are checked in the program’s initial instant,
satisfaction of $\square\varphi$ implies satisfaction of $\varphi$ for all
instants in time; thus $\square$ properties are invariant properties.

  2. (2)

Next ($\ocircle$): A property $\ocircle\varphi$ requires that $\varphi$ be
satisfied in the next instant. In other words,
$(s_{i},~{}s_{i+1},~{}s_{i+2},...)\vDash\ocircle\varphi\iff
s_{i+1}\VDash\varphi$

We additionally introduce ${\sf hd}($) as a convenience function that
transforms a trace predicate $\varphi$ such that for any streams $s$ and $t$,
$s\vDash\varphi\Rightarrow(s\ {\sf fby}\ t)\vDash{\sf hd}(\varphi)$. Thus,
${\sf hd}(\varphi)$ represents a condition that a stream with $s_{0}$ as its
initial value will satisfy, regardless of subsequent values, assuming that $s$
satisfies $\varphi$. This is useful for deriving properties about a stream
constructed using $s\ {\sf fby}\ t$, if properties are known about $s$ and $t$
individually. The transformation is defined recursively for state predicates
$p$ and trace predicates $\varphi,\psi$ in Fig. 7. The transformation for
state predicates and $\square$ are unsurprising; state predicates are only
ever concerned with the immediate value, and $\square\varphi$ follows from the
equivalence $\square\varphi\equiv\varphi\land\ocircle\square\varphi$. No
additional information can be learned from $\ocircle\varphi$ as its
satisfaction tells us nothing about the immediate value of the stream.

###### Lemma 0 (Correctness of hd).

For any stream $\sigma=(\sigma_{0},\ \sigma_{1},\ldots)$, if
$\sigma\vDash\psi$, then for any other stream $\tau=(\tau_{0},\
\tau_{1},\ldots)$, $(\sigma_{0},\ \tau_{1},\ \tau_{2}...\tau_{n}...)\vDash{\sf
hd}(\psi)$

###### Proof.

By induction on the definition of ${\sf hd}(\psi)$
Case $p$ where $p$ is a state predicate. Assume $\sigma\vDash p$. Then
$\sigma_{0}\VDash p$. Therefore, $(\sigma_{0},\ \tau_{1},\
\tau_{2}...\tau_{n}...)\vDash{\sf hd}(p)\equiv p$ for any $\tau$.

Case $\psi_{1}\land\psi_{2}$. Assume $\sigma\vDash\psi_{1}\land\psi_{2}$. Then
$\sigma\vDash\psi_{1}$ and $\sigma\vDash\psi_{2}$. By IH, $(\sigma_{0},\
\tau^{\prime}_{1},\ \tau^{\prime}_{2}...\tau^{\prime}_{n}...)\vDash{\sf
hd}(\psi_{1})$ for any $\tau^{\prime}$, and $(\sigma_{0},\ \tau^{\prime}_{1},\
\tau^{\prime}_{2}...\tau^{\prime}_{n}...)\vDash{\sf hd}(\psi_{2})$ for any
$\tau^{\prime}$. Therefore, $(\sigma_{0},\ \tau^{\prime}_{1},\
\tau^{\prime}_{2}...\tau^{\prime}_{n}...)\vDash{\sf
hd}(\psi_{1}\land\psi_{2})$.

Case $\square\psi$. Assume $\sigma\vDash\square\psi$. By induction hypothesis
(IH), $(\sigma_{0},\ \tau^{\prime}_{1},\
\tau^{\prime}_{2}...\tau^{\prime}_{n}...)\vDash{\sf hd}(\psi)$ for any
$\tau^{\prime}$. Therefore, $(\sigma_{0},\ \tau_{1},\
\tau_{2}...\tau_{n}...)\vDash{\sf hd}(\square\psi)\equiv{\sf hd}(\psi)$ for
any $\tau$.

Case $\ocircle\psi$. Trivial. $(\sigma_{0},\ \tau_{1},\
\tau_{2}...\tau_{n}...)\vDash{\sf hd}(\ocircle\psi)\equiv\top$ for any
$\sigma$ and $\tau$. ∎

$\displaystyle{\sf hd}(p)$ $\displaystyle\triangleq p$ $\displaystyle{\sf
impl}(q,p)$ $\displaystyle\triangleq\lnot q\lor p$ $\displaystyle{\sf
hd}(\varphi\land\psi)$ $\displaystyle\triangleq{\sf hd}(\varphi)\land{\sf
hd}(\psi)$ $\displaystyle{\sf impl}(q,\varphi\land\psi)$
$\displaystyle\triangleq{\sf impl}(q,\varphi)\land{\sf impl}(q,\psi)$
$\displaystyle{\sf hd}(\square\varphi)$ $\displaystyle\triangleq{\sf
hd}(\varphi)$ $\displaystyle{\sf impl}(q,\square\varphi)$
$\displaystyle\triangleq\square({\sf impl}(q,\varphi))$ $\displaystyle{\sf
hd}(\ocircle\varphi)$ $\displaystyle\triangleq\top$ $\displaystyle{\sf
impl}(q,\ocircle\varphi)$ $\displaystyle\triangleq\ocircle({\sf
impl}(q,\varphi))$ Figure 7. Inductive definitions of the hd and impl
operators. The impl operator is needed because the syntax only allows the
$\lor$ operator (and thus implications) at the level of state formulas.

##  6\. The MARVeLus Type System

Formal verification of MARVeLus programs relies upon type checking using
specifications supplied as type refinements. Our primary contribution to the
type system is the adaptation and implementation of refinement type
specifications for streams. Unique to our refinement type system is the
introduction of temporal operators in refinement predicates.

Fig. LABEL:fig:typingrules gives the set of typing rules, adopting the
proposed stream syntax.

###  6.1. Type Semantics

A stream’s type refinement specifies the stream’s behavior from the current
instant onwards. For example, a stream inhabiting the type ${\\{w:\sf{int}\ |\
\square(w\geq 0)\\}}$ is non-negative at the current instant, and will
continue to be non-negative in all subsequent time instants. We follow the LTL
convention in that predicates are checked for validity in the time instant in
which they occur. Thus, a stream’s type describes the stream’s immediate value
along with the values it will produce in the future. We use the same judgement
as Zélus (Benveniste et al., 2011)–$G,H\vdash e:\tau$–to express that, in
function context $G$ and stream context $H$, an expression $e$ has type
$\tau$. It has proven to be more manageable to separate imported functions
from the base language into a distinct environment $G$.

###  6.2. Environments, Types, and their Operations

Aside from the separation of function and stream environments, the two
environments are defined in the standard way (Fig. 11). By virtue of our
streams being constructed from initial values and subsequent steps (through
fby), it is convenient to define operators ${\sf hd}()$ and ${\sf tl}()$ to
extract the “immediate” and “suffix” of a type, respectively. For some type
$\tau$ that can be written as ${\\{w:b\ |\ {\sf
hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}}$, an expression of type ${\sf
hd}(\tau)$ is only required to satisfy the refinement predicate of $\tau$ in
the current step. Hence, it only needs to satisfy ${\sf hd}(\varphi_{1})$.
Similarly, an expression of type ${\sf tl}(\tau)$ must satisfy, immediately,
the refinement predicate that an expression of type $\tau$ will satisfy in the
next time instant. The ${\sf tl}()$ operator is particularly useful for
computing the types of rewritten expressions of the form
$e\stackrel{{\scriptstyle v}}{{\hookrightarrow}}e^{\prime}$, and so we extend
it to operate on the entire environment (${\sf tl}(H)$). Analogously to the
operational semantics, we must also capture a notion of “history” in the
typing context. However, the result is not as exact. If $\sigma$ represents a
variable’s past behavior, then $H$ represents its future. As a variable is
updated, its immediate future behavior specializes into a single value, which
in the next time instant, gets added to $\sigma$. This process “consumes” the
part of the refinement predicate that pertains to the current instant in
preparation for determining the variable’s future behavior. Unlike the case
for $\sigma$, reversing this process in $H$ is lossy, and the best we can
accomplish is an approximation of the original type. Thus, if we started with
a type ${\\{w:b\ |\ {\sf hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}}$ and
take its suffix ${\sf tl}({\\{w:b\ |\ {\sf
hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}})={\\{w:b\ |\ \varphi_{2}\\}}$, we
may not be able to recover ${\sf hd}(\varphi_{1})$, at least not
syntactically. However, we at least know that ${\sf prev}({{\sf tl}({\\{w:b\
|\ {\sf hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}})})$ is a subtype of
${\\{w:b\ |\ \ocircle\varphi_{2}\\}}$. Using this, and potentially additional
information brought in through invariants, we can approximate the type
environment from the previous time instant, which may suffice even if we
cannot recover the exact environment.

$\displaystyle H::=$ $\displaystyle\varnothing~{}|~{}H,x:\tau$ $\displaystyle
G::=$ $\displaystyle\varnothing~{}|~{}G,f(x):x:\tau_{1}\to\tau_{2}$
$\displaystyle{\sf hd}({\\{w:b\ |\ {\sf
hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}})\triangleq$
$\displaystyle{\\{w:b\ |\ {\sf hd}(\varphi_{1})\\}}$ $\displaystyle{\sf
tl}({\\{w:b\ |\ {\sf hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}})\triangleq$
$\displaystyle{\\{w:b\ |\ \varphi_{2}\\}}$ $\displaystyle{\sf
tl}(H)\triangleq$ $\displaystyle\\{{\sf tl}(H(x))~{}|~{}x\in{\sf dom}({H})\\}$
$\displaystyle{\\{w:b\ |\ {\sf hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}}$
$\displaystyle\preceq{\sf prev}({{\\{w:b\ |\ \varphi_{2}\\}}})\preceq{\\{w:b\
|\ \ocircle\varphi_{2}\\}}$ $\displaystyle{\sf prev}({H})\triangleq$
$\displaystyle\\{{\sf prev}({H(x)})~{}|~{}x\in{\sf dom}({H})\\}$ Figure 11.
Typing Environments, and the operations on types and environments.

###  6.3. Summary of Typing Rules

  1. (1)

Constants: (T-CONST) encapsulates the behavior of refinement type synthesis
for constants (Jhala and Vazou, 2020), assigning a specific singleton type to
constants. Since constants do not change, we can strengthen the refinement
predicate with $\square$ to require that the constant $c$ is typed as a stream
that is always equal to $c$.

  2. (2)

Variables: (T-VAR) performs selfification on variables (Jhala and Vazou, 2020;
Ou et al., 2004), which strengthens the type by explicitly requiring that the
refinement variable $v$ is always equal to the term variable $x$. This is
achieved by the addition of the $\square(v=x)$ constraint in the refinement.

  3. (3)

Stream Compositions: (T-FBY-0) and (T-FBY-1) generate the verification
conditions for typing the composition of two streams $e_{1}$ and $e_{2}$, with
associated predicates ${\sf hd}(\psi_{1})$ and $\psi_{2}$, respectively. Since
the resultant stream must not change its base type, we require that $e_{1}$
and $e_{2}$ type to the same base type. The fby construct allows one to
combine values of both streams $e_{1}$ and $e_{2}$; naturally, the resultant
stream inherits some properties of both. Crucially, the stream only takes the
first value of $e_{1}$, after which it replicates the behavior of the stream
$e_{2}$ but delayed by one cycle. Consequently, given $e_{1}$ satisfying
property $\psi_{1}$ for at least the first cycle and $e_{2}$ satisfying
$\psi_{2}$, the stream $e_{1}$ fby $e_{2}$ should satisfy both $\psi_{1}$ for
the first cycle, and also $\ocircle\psi_{2}$. The subscript denotes the value
“buffered” by fby, which is empty in the first cycle (T-FBY-0), and may be
occupied by a value in subsequent cycles (T-FBY-1). Since the first stream is
only considered in the first cycle and is disregarded in determining the
resultant type in (T-FBY-1), it is left unrefined. Instead, a stream’s
behavior with $\ {\sf fby}_{u}\ $ where $u\neq{\sf nil}$ is determined by the
$u$ and $e_{2}$.

  4. (4)

Local Bindings: We define recursive (T-REC) and non-recursive (T-LET) local bindings as usual, noting that (T-REC) is crucial for proving inductive invariants when paired with (T-FBY). We note that T-LET requires type annotations be well-formed ($G;~{}H\vdash\tau_{1}$), that is, the refinement predicate is a Boolean stream that only references in-scope variables. This is a direct lifting of the non-stream well-formedness judgement for other refinement type systems (Jhala and Vazou, 2020; Rondon et al., 2008). Suppose we want to verify that the program let rec x:{v:int | v >= 0} = 0 fby x + 1 in x types to $\\{v:{\sf int}~{}|~{}v\geq 0\\}$. Since $x$ is recursively defined, verifying that all values of $x$ are non-negative involves first verifying that the initial condition 0 and then the inductive definition x+1, with the assumption that $\square(x\geq 0)$ held in the previous instant. At first glance, the assumption $\square(x\geq 0)$ appears circular, essentially stating that the stream we want to check already satisfies the predicate we want to verify. However, we note that at each instant beyond the first time step, $x$ represents the stream in the current time step, whereas $x+1$ is the new definition that will take effect in the next time step. Therefore, the verification task shifts to proving that, assuming the stream $x$ already satisfies $\square(x\geq 0)$, the predicate $\square((x+1)\geq 0)$ is valid.

  5. (5)

Branching Expressions: As with other refinement type systems (Jhala and Vazou,
2020), the types of both branches can be expanded so that type refinements
only need to be satisfied when the conditional of that branch is satisfied.
This control-flow awareness prevents the type system from needlessly rejecting
terms that the program will have never reached. This notion is lifted into
stream types through the ${\sf impl}()$ operator, which inserts an implication
statement at the state-predicate level, achieving the same effect as in non-
stream refinement type systems with a similar rule.

  6. (6)

Function Application: Since functions are imported from a non-stream language
and applied point-wise to the values of stream variables, they are considered
constant and thus their types are unchanging over time. As a result, the
argument variable should type to the function’s argument type at all times. By
extension, the return type of the function application should be enforced for
all time. This is encapsulated by the (T-APP) rule, which augments the
original (non-stream) function type with the LTL $\square$ operator to require
that these properties hold over all time.

  7. (7)

Robot-specific commands Due to the unpredictability of real-world physical
parameters, we exclude robot_get and robot_store from refinement type-
checking, and treat them as functions that simply return the appropriate un-
refined term for the base Zélus type checker. Instead, we require that each
call to robot_get be accompanied by models, so that each variable intended to
derive values from the real world has a deterministic verifiable model.
Indeed, the user is responsible for ensuring that the model does in fact
reflect expected real-world conditions, which are impossible to predict at
compile-time. Since the models keyword is intended to be semantically
transparent, it directly inherits the type of its inner expression. Although
it is outside the control of MARVeLus, it is assumed that the robot-specific
command following models has the same type.

  8. (8)

Typing nil Since nilcan be pushed onto the history of any variable, we allow
it to type to anything. While this may appear disconcerting, the static
initialization and causality analyses in Zélus (Benveniste et al., 2011)
ensure that well-formed programs do not allow nilto be executed. That is, a
variable that does not have immediate self-dependencies or have circular
dependencies with other variables will never access a variable whose history
ends in nil.

  9. (9)

Subtyping We use the standard subtyping rules developed for Liquid Haskell
(Jhala and Vazou, 2020; Rondon et al., 2008). However, we note that, while
subtyping on base types operates on stream types, subtyping on functions
reverts to non-stream type checking, as functions are imported directly from
the base language.

###  6.4. Type Safety

We prove type safety roughly following the classical syntax-guided manner of
Wright and Felleisen (Wright and Felleisen, 1994). A key difference arises in
our type system from the decoupling of program terms from the values they
produce in the synchronous semantics. Type safety must apply not only to the
values emitted, but also to the subsequent evaluations of the stream term to
ensure that the program remains safe in the future. We also note that existing
work by Boulmé and Hamon (Boulmé and Hamon, 2001) has explored synchronous
properties of languages such as Lustre, some of which resemble progress in
conventional languages. We begin by defining convenience operators ${\sf
basetype}$ and ${\sf now}$, which “un-refine” a refined type and retrieve the
most recent (thus current) entry of a variable’s history, respectively:

$\displaystyle{\sf basetype}({\\{w:b\ |\ \varphi\\}})=b$ $\displaystyle{\sf
now}(h::v)=v$

We also define conditions under which the function and stream term
environments correspond with their type environment counterparts. Namely, we
want to enforce some notion of well-typedness on the environments:

###### Definition 1 (Function Environment Correspondence).

Environments $G$ and $S$ correspond when the following conditions are met:

  * •

${\sf dom}({G})\subseteq{\sf dom}({S})$

  * •

$\forall f\in{\sf dom}({G})$, $G;H\vdash S(f):G(x)$

###### Definition 2 (Stream Environment Correspondence).

Environments $H$ and $\sigma$ correspond when the following conditions are
met:

  * •

${\sf dom}({H})\subseteq{\sf dom}({\sigma})$

  * •

$\forall x\in{\sf dom}({H})$:

    * –

$G;H\vdash\sigma(x):{\sf basetype}(H(x))$ and

    * –

$G;H\vdash{\sf now}(\sigma(x)):{\sf hd}(H(x))$

  * •

${\sf prev}({\sigma})$ corresponds with any ${\sf prev}({H})$

Definition 1 is standard. We note the absence of $H$ in its typing judgement
as functions are judged in their original non-stream contexts using the
standard typing judgement. Definition 2 involves streams and thus requires
different treatment. Stream types determine a variable’s current and expected
future trajectory, while stream histories record a variable’s past and current
trajectory. They intersect at the present moment, where both the history and
type of a variable refer to the variable’s current state. Thus, at any given
moment, we can only make a precise, refinement typing judgement about the
variable’s current value. Since histories are initialized to be empty and are
extended only by let-bindings (recursive or otherwise), we can ensure that
let-bindings maintain correspondence between the type and term environments
for all time. This is proven explicitly in the (T-LETREC) case in our type
preservation proof, and assumed elsewhere. Because the ${\sf prev}({})$
operator is unable to exactly recover the original refinement of a type, we
simply require correspondence of ${\sf prev}({\sigma})$ with any ${\sf
prev}({H})$, noting that for any $H$ which evolves into $H^{\prime}$, ${\sf
prev}({H^{\prime}})$ will necessarily produce subtypes of variables in $H$. We
can however ascertain that a variable corresponds with its base type at any
point in time.

###### Theorem 1 (Type Safety).

If $H$ corresponds with $\sigma$ and $G$ corresponds with $S$, and if
$G;H\vdash e:\tau$, then $\exists e^{\prime}$ such that $S;\sigma\vdash
e\stackrel{{\scriptstyle v}}{{\hookrightarrow}}e^{\prime}$ where $v$ is a
value, $G,H\vdash v:{\sf hd}(\tau)$, and $G,{\sf tl}(H)\vdash e^{\prime}:{\sf
tl}(\tau)$

###### Proof.

By proving progress and preservation on well-typed terms. ∎

####  6.4.1. Progress

The standard notion of progress stipulates that a well-typed program term is
either a value or can undergo reduction via the semantic rules. Since all
MARVeLus streams are designed to emit values in perpetuity, including constant
streams, we must show that there is always a rule that allows the program to
take another semantic step, and thus emit another value.

###### Lemma 0 (Progress).

If $H$ corresponds with $\sigma$ and $G$ corresponds with $S$, if $G;H\vdash
e:\tau$, then $\exists e^{\prime}$ such that $S;\sigma\vdash
e\stackrel{{\scriptstyle v}}{{\hookrightarrow}}e^{\prime}$ where $v$ is a
value.

###### Proof.

By structural induction on the typing derivation of $e$.
Case T-CONST.

  * •

$G;H\vdash c:{\\{w:b\ |\ \square(w=c\\}}$

  * •

By S-CONST, $S;\sigma\vdash c\stackrel{{\scriptstyle c}}{{\hookrightarrow}}c$

  * •

By definition, $c$ is a value.

Case T-VAR.

  * •

$G;H\vdash x:{\\{w:b\ |\ \psi\land\square(w=x)\\}}$ for some refinement
predicate $\psi$

  * •

Because $x$ is well-typed, $x\in{\sf dom}({H})$.

  * •

By assumption, $x\in{\sf dom}({\sigma})$, and so $\sigma(x)=h::v$ for some
history $h::v$ where $G;H\vdash v:{\sf hd}(H(x))$ (need to specify a
particular $h$ and $v$ here?)

  * •

Therefore $S;\sigma,x=h::v\vdash x\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}x$

  * •

By definition of histories $v$ is a value.

Case T-FBY

  * •

$G;H\vdash e_{1}\ {\sf fby}\ e_{2}:{\\{w:b\ |\ {\sf
hd}(\psi_{1})\land\ocircle{\sf hd}(\psi_{2})\\}}$

  * •

By assumption, $G;H\vdash e_{1}:{\\{w:b\ |\ \psi_{1}\\}}$ and $G;H\vdash
e_{2}:{\\{w:b\ |\ \psi_{2}\\}}$

  * •

By IH, $S;\sigma\vdash e_{1}\stackrel{{\scriptstyle
v_{1}}}{{\hookrightarrow}}e_{1}^{\prime}$ and $S;\sigma\vdash
e_{2}\stackrel{{\scriptstyle v_{2}}}{{\hookrightarrow}}e_{2}^{\prime}$ where
$v_{1}$ and $v_{2}$ are values.

  * •

By S-FBY, $S;\sigma\vdash e_{1}\ {\sf fby}\ e_{2}\stackrel{{\scriptstyle
v_{1}}}{{\hookrightarrow}}{\sf delay}(e_{2})$

Case T-DELAY

  * •

$G;H\vdash{\sf delay}(e_{1}):\tau$

  * •

By assumption, $G;{\sf prev}({H})\vdash e:\tau$

  * •

Since $H$ and $\sigma$ correspond, ${\sf prev}({H})$ and ${\sf
prev}({\sigma})$ also correspond.

  * •

By IH, $S;{\sf prev}({\sigma})\vdash e\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e^{\prime}$ where $v$ is a value.

  * •

By S-DELAY, $S,\sigma\vdash{\sf delay}(e)\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}{\sf delay}(e^{\prime})$

Case T-IF

  * •

$G;H\vdash{\sf if}\ {x_{c}}\ {\sf then}\ {e_{t}}\ {\sf else}\ {e_{f}}:{\\{w:b\
|\ \psi\\}}$

  * •

By assumption:

    * –

$x_{c}\in{\sf dom}({H})$ and thus $x_{c}\in{\sf dom}({\sigma})$ and
$\sigma(x)=h::v_{c}$ for some $h$ and $v_{c}$ where $G;H\vdash v_{c}:{\sf
hd}(H(x))$

    * –

$G;H\vdash x_{c}:{\sf bool}$

    * –

$G;H\vdash e_{t}:{\\{w:b\ |\ {\sf impl}(x_{c},\psi)\\}}$

    * –

$G;H\vdash e_{f}:{\\{w:b\ |\ {\sf impl}(\neg x_{c},\psi)\\}}$

  * •

By IH:

    * –

$S;\sigma,x=h::v_{c}\vdash x_{c}\stackrel{{\scriptstyle
v_{c}}}{{\hookrightarrow}}x_{c}$ where $v_{c}$ is a value

    * –

$S;\sigma,x=h::v_{c}\vdash e_{t}\stackrel{{\scriptstyle
v_{t}}}{{\hookrightarrow}}e_{t}^{\prime}$ where $v_{t}$ is a value

    * –

$S;\sigma,x=h::v_{c}\vdash e_{f}\stackrel{{\scriptstyle
v_{f}}}{{\hookrightarrow}}e_{f}^{\prime}$ where $v_{f}$ is a value

  * •

Since $v_{c}$ is a value and a boolean, it can either be true or false.

  * •

Case $v_{c}={\sf true}$: By S-IF-T, $S;\sigma,x=h::v_{c}\vdash{\sf if}\
{x_{c}}\ {\sf then}\ {e_{t}}\ {\sf else}\ {e_{f}}\stackrel{{\scriptstyle
v_{t}}}{{\hookrightarrow}}{\sf if}\ {x_{c}}\ {\sf then}\ {e_{t}^{\prime}}\
{\sf else}\ {e_{f}^{\prime}}$

  * •

Case $v_{c}={\sf false}$: Symmetric on S-IF-F

Case T-LETREC

  * •

$G;H\vdash{\sf
let}_{h}{\sf~{}rec~{}}x:\tau_{1}=e_{1}{\sf~{}in~{}}e_{2}:\tau_{2}$

  * •

By assumption:

    * –

$\tau_{1}$ is well-formed in $G;H$

    * –

$G;H,x:\tau_{1}\vdash e_{1}:\tau_{1}$

    * –

$G;H,x:\tau_{1}\vdash e_{2}:\tau_{2}$

  * •

Since $\sigma$ corresponds with $H$, $x\in{\sf dom}({\sigma})$ and thus
$\sigma(x)=h::v$ where $G;H\vdash v:{\sf hd}(H(x))$

  * •

By IH:

    * –

$S;\sigma,x=h::{\sf nil}\vdash e_{1}\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e_{1}^{\prime}$ (using the fact that ${\sf nil}$ can
type to anything)

    * –

$S;\sigma,x=h::v\vdash e_{2}\stackrel{{\scriptstyle
v_{2}}}{{\hookrightarrow}}e_{2}^{\prime}$ where $v_{2}$ is a value.

  * •

By S-LETREC, $S,\sigma\vdash{\sf
let}_{h}{\sf~{}rec~{}}x:\tau_{1}=e_{1}{\sf~{}in~{}}e_{2}\stackrel{{\scriptstyle
v_{2}}}{{\hookrightarrow}}{\sf let}_{h::v}{\sf~{}rec~{}}x:{\sf
tl}(\tau_{1})=e_{1}^{\prime}{\sf~{}in~{}}e_{2}^{\prime}$

Case T-APP

  * •

$G,f:x:\tau_{1}\to{\\{w_{2}:b_{2}\ |\ \psi_{2}\\}};H\vdash
f~{}y:{\\{w_{2}:b_{2}\ |\ \square\psi_{2}[x\mapsto y]\\}}$

  * •

By assumption, $y\in{\sf dom}({H})$

  * •

Because $G$ corresponds with $S$, $f\in{\sf dom}({S})$ and is in particular
some $f(x)=e$ where $G\vdash f:x:\tau_{1}\to{\\{w_{2}:b_{2}\ |\ \psi_{2}\\}}$

  * •

Because $H$ corresponds with $\sigma$, $y\in{\sf dom}({\sigma})$ and
$\sigma(y)=h::v$ where $G;H\vdash v:{\sf hd}(H(y))$

  * •

By S-APP, $S,f(x)=e;\sigma,y=h::v\vdash f(y)\stackrel{{\scriptstyle e[x\mapsto
y]f(y)}}{{\hookrightarrow}}$ (TODO: prove that $e[x\mapsto y]$ is a value, in
non-stream semantics)

Case T-MODELS

  * •

$G;H\vdash{e\ {\sf models}\ r}:\tau$

  * •

Assume $\neg{\sf robot~{}mode}$

  * •

By assunmption, $G;H\vdash e:\tau$

  * •

By IH, $S;\sigma\vdash e\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e^{\prime}$ and $v$ is a value

  * •

By S-MODELS, $S;\sigma\vdash{e\ {\sf models}\ r}\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}{e^{\prime}\ {\sf models}\ r}$

Case T-SUB

  * •

$G;H\vdash e:\tau^{\prime}$

  * •

Based on the conditions laid out in (Borkowski et al., 2022), we are able to
“collapse” repeated invocations of T-SUB into a single subtyping derivation.

  * •

Then, the premise $G;H\vdash e:\tau$ must have been derived through a non-
subtyping rule.

  * •

By IH, $S;\sigma\vdash e\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e^{\prime}$

∎

####  6.4.2. Preservation

When a stream expression $e$ is evaluated, it not only produces a value $v$
representing its immediate state at this instant, but also becomes
$e^{\prime}$, representing the stream to be evaluated in the next instant.
Over the course of several evaluations, the stream that was once $e$ becomes
“realized” as a series of emitted values $v_{0},\ v_{1},\ v_{2}...$ and stream
definitions $e^{\prime},e^{\prime\prime},e^{\prime\prime\prime}...$. Combined
with the fact that refinement predicates are considered in the time instant in
which a stream is evaluated, this means that a predicate that accurately
describes a stream in one instant may no longer be satisfied over subsequent
evaluations. Consider the stream $s$ whose next values will be
$[-1,0,1,2,3...]$. The predicate $\varphi=(s<0)\land\ocircle\square(s\geq 0)$
accurately describes $s$ in the current time instant. However, after $s$ emits
a value and becomes $s^{\prime}$, whose next values are $[0,1,2,3...]$,
$\varphi$ no longer accurately describes $s^{\prime}$, as the value it emits
next will not be negative. This is expected, as the state predicate $s<0$
within $\varphi$ only applies to the first state of $s$. An implication that
arises is that type refinements also need to evolve over time to accurately
describe stream behavior, a phenomenon that is not normally seen in refinement
type systems. This somewhat complicates proofs of type safety, as stream
expressions that step do not necessarily continue to inhabit their original
types.

However, we note that a stream $e^{\prime}$ produced by evaluation of $e$ is a
“suffix” of $e$; in other words, the values emitted by $e^{\prime}$ are
identical to those emitted by $e$ after the first value. Likewise, if $e$
satisfies a predicate $\varphi$, then $e^{\prime}$ will satisfy its “suffix”.
This allows us to relate the types that $e$ and $e^{\prime}$ inhabit and
derive a modified notion of type safety, even if their types do not exactly
match. If a predicate $\varphi$ can be written as ${\sf
hd}(\varphi_{1})\land\ocircle\varphi_{2}$ for some secondary predicates
$\varphi_{1}$ and $\varphi_{2}$, then its suffix is $\varphi_{2}$. Thus, if
$e$ satisfies $\varphi$, and in the current context $e\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e^{\prime}$, then $v$ satisfies ${\sf hd}(\varphi_{1})$
and $e^{\prime}$ satisfies $\varphi_{2}$. From this, we can derive types such
that if $G;~{}H\vdash e:{\\{w:b\ |\ {\sf
hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}}$, then $G;~{}H\vdash v:{\\{w:b\
|\ {\sf hd}(\varphi_{1})\\}}$ and $G;~{}{\sf tl}(H)\vdash e^{\prime}:{\\{w:b\
|\ \varphi_{2}\\}}$ where ${\sf tl}(H)$ is the immediate successor of $H$:

${\sf dom}({{\sf tl}(H)})={\sf dom}({H}),~{}\forall~{}x\in{\sf dom}({{\sf
tl}(H)})~{}.~{}({\sf tl}(H)(x))={\sf tl}(H(x))$

where for a refined type $\tau={\\{w:b\ |\ {\sf
hd}(\varphi_{1})\land\ocircle\varphi_{2}\\}}$, ${\sf tl}(\tau)={\\{w:b\ |\
\varphi_{2}\\}}$. We prove that $\varphi_{1}$ and $\varphi_{2}$ exist for any
$\varphi$ constructed in our specification grammar:

###### Lemma 0 (Temporal Predicate Expansion).

Let $\psi$ be a temporal predicate. Then there exist $\psi_{1},\ \psi_{2}$
such that $\psi\equiv{\sf hd}(\psi_{1})\land\ocircle\psi_{2}$

###### Proof.

By induction on the specification grammar (Fig. 3)
Case $p$: $\Psi\equiv p$ (where $p$ is a state predicate): then
$\Psi_{1}\equiv p$ and $\Psi_{2}\equiv\top$ satisfy the desired condition.

Case $\land$: $\Psi\equiv\psi_{l}\ \land\ \psi_{r}$ (where $\land$ is a binary
logical connective): by IH, $\exists\psi_{l,1},\ \psi_{l,2}$ s.t.
$\psi_{l}\equiv{\sf hd}(\psi_{l,1})\land\ocircle\psi_{l,2}$ and likewise
$\exists\psi_{r,1},\ \psi_{r,2}$ s.t. $\psi_{r}\equiv{\sf
hd}(\psi_{r,1})\land\ocircle\psi_{r,2}$. Then $\Psi_{1}\equiv{\sf
hd}(\psi_{l,1}\land\psi_{r,1})$ and
$\Psi_{2}\equiv(\psi_{l,2}\land\psi_{r,2})$ satisfy the desired condition.

Case $\ocircle$: $\Psi\equiv\ocircle\psi$, therefore $\Psi_{1}\equiv\top$ and
$\Psi_{2}\equiv\psi$ satisfy the desired condition.

Case $\square$: We have $\Psi\equiv\square\psi$. By IH, $\exists\psi_{1},\
\psi_{2}$ s.t. $\psi\equiv{\sf hd}(\psi_{1})\land\ocircle\psi_{2}$. Note that
$\square\psi\equiv\psi\land\ocircle\square\psi$. Therefore
$\square\psi\equiv({\sf
hd}(\psi_{1})\land\ocircle\psi_{2})\land\ocircle\square\psi\equiv{\sf
hd}(\psi_{1})\land\ocircle(\psi_{2}\land\square\psi)$. Then
$\Psi_{1}\equiv\psi_{1}$ and $\Psi_{2}\equiv\psi_{2}\land\square\psi$ satisfy
the desired condition.

∎

###### Lemma 0 (Type Preservation).

Let $e$ be a synchronous stream expression. If $H$ corresponds with $\sigma$
and $G$ corresponds with $S$, then if $G,H\vdash e:\tau$ and
$S;~{}\sigma\vdash e\stackrel{{\scriptstyle v}}{{\hookrightarrow}}e^{\prime}$,
then $G,H\vdash v:{\sf hd}(\tau)$ and $G,{\sf tl}(H)\vdash e^{\prime}:{\sf
tl}(\tau)$

###### Proof.

By structural induction on the operational semantics derivation. We prove by
cases on the last rule used.
Case S-LETREC: ${\sf let~{}rec}_{h}~{}x:\tau=e_{1}{\sf~{}in~{}}e_{2}$

  * •

Assume $G;~{}H\vdash{\sf let~{}rec}_{h}~{}x:\tau=e_{1}{\sf~{}in~{}}e_{2}:\tau$
and $S;~{}\sigma\vdash{\sf
let~{}rec}_{h}~{}x:\tau=e_{1}{\sf~{}in~{}}e_{2}\stackrel{{\scriptstyle
w}}{{\hookrightarrow}}{\sf let~{}rec}_{h::v}~{}x:{\sf
tl}(\tau_{1})=e_{1}^{\prime}{\sf~{}in~{}}e_{2}^{\prime}$.

  * •

Furthermore, we prove that $h$ consists solely of well-typed values.
Specifically, we show that, after evaluation of (S-LETREC), $G;~{}H\vdash
v:{\sf hd}(\tau_{1})$ where $v$ is the last value in $h$. This ensures that
$\sigma$ stays consistent with $H$

  * •

Induct on the number of elements in $h$.

  * •

Suppose $h=[]$.

    * –

By assumption, $S;~{}\sigma,x=[{\sf nil}]\vdash e_{1}\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e_{1}^{\prime}$.

    * –

By assumption and the above, $S;~{}\sigma,x=[v]\vdash
e_{2}\stackrel{{\scriptstyle w}}{{\hookrightarrow}}e_{2}^{\prime}$.

    * –

T-LETREC must be the last (non-subtype (Borkowski et al., 2022)) rule used in
the typing derivation. By inversion:

      * *

$G;~{}H,x:\tau_{1}\vdash e_{1}:\tau_{1}$

      * *

$G;~{}H,x:\tau_{1}\vdash e_{2}:\tau$

    * –

Since $\tau_{1}$ is well-formed ($G;~{}H\vdash\tau_{1}$) and ${\sf
dom}({H})={\sf dom}({{\sf tl}(H)})$, ${\sf tl}(\tau_{1})$ is also well-formed,
i.e. $G;~{}{\sf tl}(H)\vdash{\sf tl}(\tau_{1})$

    * –

By the Induction Hypothesis and Lemma 3:

      * *

$G;~{}H,x:{\tau_{1}}\vdash v:{\sf hd}(\tau_{1})$. Thus $v$ is well-typed.

      * *

$G;~{}{\sf tl}(H),x:{\sf tl}(\tau_{1})\vdash e_{1}^{\prime}:{\sf
tl}(\tau_{1})$

      * *

$G;~{}H,x:{\tau_{1}}\vdash w:{\sf hd}(\tau)$

      * *

$G;~{}{\sf tl}(H),x:{\sf tl}(\tau_{1})\vdash e_{2}^{\prime}:{\sf tl}(\tau)$

    * –

By (T-FBY), $G;~{}{\sf tl}(H)\vdash{\sf let~{}rec}_{v}~{}x:{\sf
tl}(\tau_{1})=e_{1}^{\prime}{\sf~{}in~{}}e_{2}^{\prime}:{\sf tl}(\tau)$

    * –

Since $v$ is the only member of $h$, $h$ contains only well-typed values, and
thus the last value of $h$ has type ${\sf hd}(\tau_{1})$ in $H$.

  * •

Suppose $h\neq[]$. Suppose all prior values of $h$ are well-typed.

    * –

By assumption, $S;~{}\sigma,x=h::{\sf nil}\vdash e_{1}\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e_{1}^{\prime}$.

    * –

By assumption and the above, $S;~{}\sigma,x=h::v\vdash
e_{2}\stackrel{{\scriptstyle w}}{{\hookrightarrow}}e_{2}^{\prime}$

    * –

T-LETREC must be the last (non-subtype) rule used in the typing derivation. By
inversion:

      * *

$G;~{}H,x:\tau_{1}\vdash e_{1}:\tau_{1}$

      * *

$G;~{}H,x:\tau_{1}\vdash e_{2}:\tau$

    * –

Similarly to before, $G;~{}{\sf tl}(H)\vdash{\sf tl}(\tau_{1})$

    * –

By IH and Lemma 3 (same as the $h=[]$ case):

      * *

$G;~{}H,x:{\tau_{1}}\vdash v:{\sf hd}(\tau_{1})$. Thus $v$ is well-typed.

      * *

$G;~{}{\sf tl}(H),x:{\sf tl}(\tau_{1})\vdash e_{1}^{\prime}:{\sf
tl}(\tau_{1})$

      * *

$G;~{}H,x:{\tau_{1}}\vdash w:{\sf hd}(\tau)$

      * *

$G;~{}{\sf tl}(H),x:{\sf tl}(\tau_{1})\vdash e_{2}^{\prime}:{\sf tl}(\tau)$

    * –

By (T-FBY), $G;~{}{\sf tl}(H)\vdash{\sf let~{}rec}_{h::v}~{}x:{\sf
tl}(\tau_{1})=e_{1}^{\prime}{\sf~{}in~{}}e_{2}^{\prime}:{\sf tl}(\tau)$

    * –

Since the only new value added to the history is $v$ and $v$ is well-typed,
$h::v$ remains well-typed. Since it is at the end of $h$, the last value of
$h$ still has type ${\sf hd}(\tau_{1})$ in $H$

Case S-LET: Similar to S-LETREC.

Case S-FBY: $e_{1}\ {\sf fby}\ e_{2}$

  * •

Assume $G;~{}H\vdash e_{1}\ {\sf fby}\ e_{2}:{\\{w:b\ |\ {\sf
hd}(\psi_{1})\land\ocircle\psi_{2}\\}}$ and $\sigma\vdash e_{1}\ {\sf fby}\
e_{2}\stackrel{{\scriptstyle v}}{{\hookrightarrow}}{\sf delay}(e_{2})$.

  * •

By assumption, $S;~{}\sigma\vdash e_{1}\stackrel{{\scriptstyle
v_{1}}}{{\hookrightarrow}}e_{1}^{\prime}$

  * •

T-FBY must be the last (non-subtyping) rule used in the typing derivation. By
inversion:

    * –

$G;~{}H\vdash e_{1}:{\\{w:b\ |\ {\sf hd}(\psi_{1})\\}}$

    * –

$G;~{}H\vdash e_{2}:{\\{w:b\ |\ \psi_{2}\\}}$

  * •

By IH, $G;~{}H\vdash v_{1}:{\\{w:b\ |\ {\sf hd}({\sf
hd}(\psi_{1}))\\}}\equiv{\\{w:b\ |\ {\sf hd}(\psi_{1})\\}}$.

  * •

By applying (T-DELAY) on $e_{2}$ and noting that ${\sf prev}({{\sf
tl}(H)})(x)\preceq H(x)$ for all $x\in{\sf dom}({H})$, ${\sf
tl}(()H)\vdash{\sf delay}(e_{2}):{\\{w:b\ |\ \psi_{2}\\}}$

Case S-DELAY: ${\sf delay}(e)$

  * •

Assume $G;~{}H\vdash{\sf delay}(e_{1}):\tau$

  * •

By assumption, $S~{}{\sf prev}({\sigma})\vdash e\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e^{\prime}$

  * •

T-DELAY must be the last (non-subtyping) rule used in the typing derivation.
By inversion, $G;~{}{\sf prev}({H})\vdash e:\tau$

  * •

By IH and using Lemma 3 to split $\tau$:

    * –

$G;~{}{\sf prev}({H})\vdash v:{\sf hd}(\tau)$. Since $v$ is a value, it is a
constant and thus $G;~{}H\vdash v:{\sf hd}(\tau)$

    * –

$G;~{}{\sf tl}({\sf prev}({H}))\vdash e^{\prime}:{\sf tl}(\tau)$

  * •

Since ${\sf tl}({\sf prev}({H}))\equiv H$, $G;~{}H\vdash e^{\prime}:{\sf
tl}(\tau)$

  * •

Using (T-DELAY), $G;~{}{\sf tl}(H)\vdash{\sf delay}(e^{\prime}):{\sf
tl}(\tau)$

Case S-IF-T: ${\sf if}\ {x_{c}}\ {\sf then}\ {e_{t}}\ {\sf else}\ {e_{e}}$

  * •

Assume $G;~{}H\vdash{\sf if}\ {x_{c}}\ {\sf then}\ {e_{t}}\ {\sf else}\
{e_{f}}:{\\{w:b\ |\ \psi\\}}$ and $S;~{}\sigma,x=h::{\sf true}\vdash({\sf
if~{}}x{\sf~{}then~{}}e_{t}{\sf~{}else~{}}e_{f})\stackrel{{\scriptstyle
v_{t}}}{{\hookrightarrow}}({\sf
if~{}}x{\sf~{}then~{}}e_{t}^{\prime}{\sf~{}else~{}}e_{f}^{\prime})$

  * •

By assumption:

    * –

$S;~{}\sigma,x=h::{\sf true}\vdash e_{t}\stackrel{{\scriptstyle
v_{t}}}{{\hookrightarrow}}e_{t}^{\prime}$

    * –

$S;~{}\sigma,x=h::{\sf true}\vdash e_{f}\stackrel{{\scriptstyle
v_{f}}}{{\hookrightarrow}}e_{f}^{\prime}$

  * •

T-IF must be the last (non-subtyping) rule used in the typing derivation. By
inversion:

    * –

$G;~{}H\vdash x_{c}:{\sf bool}$

    * –

$G;~{}H\vdash e_{t}:{\\{w:b\ |\ {\sf impl}(x_{c},\psi)\\}}$

    * –

$G;~{}H\vdash e_{f}:{\\{w:b\ |\ {\sf impl}(\lnot x_{c},\psi)\\}}$

  * •

By IH and using Lemma 3 to split $\psi$:

    * –

$G;~{}{\sf tl}(H)\vdash e_{t}^{\prime}:{\sf tl}({\\{w:b\ |\ {\sf
impl}(x_{c},\psi)\\}})$

    * –

$G;~{}{\sf tl}(H)\vdash e_{f}^{\prime}:{\sf tl}({\\{w:b\ |\ {\sf impl}(\lnot
x_{c},\psi)\\}})$

    * –

$G;~{}{\sf tl}(H)\vdash x_{c}:{\sf tl}({\sf bool})$ (equivalent to just
(bool))

    * –

$G;~{}H\vdash v_{t}:{\sf hd}({\\{w:b\ |\ {\sf impl}(x_{c},\psi)\\}})$. Since
the current value of $x_{c}$ is true, ${\sf hd}({\sf
impl}(x_{c},\psi))\equiv{\sf hd}(\psi)$. Therefore $G;~{}H\vdash v_{t}:{\sf
hd}({\\{w:b\ |\ \psi\\}})$.

  * •

By (T-IF): $G;~{}{\sf tl}(H)\vdash({\sf
if~{}}x{\sf~{}then~{}}e_{t}^{\prime}{\sf~{}else~{}}e_{f}^{\prime}):{\sf
tl}({\\{w:b\ |\ \psi\\}})$

Case S-IF-F: Symmetric to S-IF-T. Case S-CONST: $c$ where $c$ is a constant

  * •

By Lemma 3, ${\sf tl}({\\{w:b\ |\ \square(w=c)\\}})\equiv{\\{w:b\ |\
\square(w=c)\\}}$

  * •

By Lemma 3, ${\\{w:b\ |\ \square(w=c)\\}}\preceq{\sf hd}({\\{w:b\ |\
\square(w=c)\\}})\equiv{\\{w:b\ |\ w=c\\}}$. Therefore $G;~{}H\vdash c:{\sf
hd}({\\{w:b\ |\ \square(w=c)\\}})$

  * •

Since $c$ is a constant, no free variables can occur in $c$. Therefore,
$G;~{}{\sf tl}(H)\vdash c:{\sf tl}({\\{w:b\ |\ \square(w=c)\\}})$

Case S-VAR: $x$

  * •

Assume $G;~{}H\vdash x:{\\{w:b\ |\ \psi\land\square(w=x)\\}}$ and
$S;~{}\sigma,x=h::v\vdash x\stackrel{{\scriptstyle v}}{{\hookrightarrow}}x$

  * •

Since the environment is non-empty (because $x$ can step), this must be a sub-
term of either ${\sf let}$ or ${\sf let~{}rec}$. In Case S-LETREC, we showed
that for $\sigma(x)=h$ and $H(x)=\tau$, the last value of $h$ types to ${\sf
hd}(\tau)$ in $H$. Therefore, $G;~{}H\vdash v:{\sf hd}({\\{w:b\ |\ \psi\\}})$.

  * •

Because $v$ is the current value of $x$, $v=x$ (state predicate). Thus the
type can be augmented as follows: $G;~{}H\vdash v:{\sf hd}({\\{w:b\ |\
\psi\land\square(w=x)\\}})$, noting that for any $\varphi$, ${\sf
hd}(\square\varphi)\equiv\varphi$.

  * •

By definition of ${\sf tl}(H)$, $({\sf tl}(H))(x)={\sf tl}({\\{w:b\ |\
\psi\\}})$

  * •

By T-VAR, $G;~{}{\sf tl}(H)\vdash x:{\sf tl}({\\{w:b\ |\
\psi\land\square(w=x)\\}})$

Case S-APP: $f\ y$

  * •

Assume $G,f:x:{\\{w_{1}:b_{1}\ |\ \varphi_{1}\\}}\to{\\{w_{2}:b_{2}\ |\
\varphi_{2}\\}};~{}H\vdash f~{}y:{\\{w_{2}:b_{2}\ |\
\square\varphi_{2}[x\mapsto y]\\}}$ and $S,f(x)=e;\sigma,y=h::v\vdash
f(y)\stackrel{{\scriptstyle e[x\mapsto v]}}{{\hookrightarrow}}f(y)$

  * •

The last (non-subtyping) rule in the typing derivation must be T-APP. By
inversion, $G,f:y:\tau_{1}\to\tau_{2};~{}H\vdash y:{\\{w_{1}:b_{1}\ |\
\square\varphi_{1}\\}}$

  * •

Because ${\sf tl}({\\{w_{1}:b_{1}\ |\
\square\varphi_{1}\\}})\equiv{\\{w_{1}:b_{1}\ |\ \square\varphi_{1}\\}}$, then
$G,f:y:\tau_{1}\to\tau_{2};~{}{\sf tl}(H)\vdash y:{\sf tl}({\\{w_{1}:b_{1}\ |\
\square\varphi_{1}\\}})$

  * •

Using similar reasoning as in Case S-VAR, the last value of $y$’s history,
$v$, has type $G,f:y:\tau_{1}\to\tau_{2};~{}H\vdash v:{\sf
hd}({\\{w_{1}:b_{1}\ |\ \square\varphi_{1}\\}})$

  * •

Using the standard substitution lemma on values extended to constants,
$G,f:y:\tau_{1}\to\tau_{2};~{}H\vdash e[x\mapsto v]$

  * •

By (T-APP) and extending the substitution lemma to type refinements that do
not change over time: $G,f:x:{\\{w_{1}:b_{1}\ |\
\varphi_{1}\\}}\to{\\{w_{2}:b_{2}\ |\ \varphi_{2}\\}};~{}{\sf tl}(H)\vdash
f~{}y:{\sf tl}({\\{w_{2}:b_{2}\ |\ \square\varphi_{2}[x\mapsto y]\\}})$ which
is equivalent to ${{\\{w_{2}:b_{2}\ |\ \square\varphi_{2}[x\mapsto y]\\}}}$

Case S-MODELS: $e{\sf~{}models~{}}r$

  * •

Assume $S,\sigma\vdash e{\sf~{}models~{}}r\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e^{\prime}{\sf~{}models~{}}r$. Also assume that the
program is not running in robot mode (ie the program behavior is exclusively
defined by the model $e$. Further assume that $G;~{}H\vdash
e{\sf~{}models~{}}r:\tau$.

  * •

By assumption, $S,\sigma\vdash e\stackrel{{\scriptstyle
v}}{{\hookrightarrow}}e^{\prime}$.

  * •

T-MODELS must be the last (non-subtype) rule used in the typing derivation. By
inversion, $G;~{}H\vdash e:\tau$.

  * •

By IH, $G;~{}{\sf tl}(H)\vdash e^{\prime}:{\sf tl}(\tau)$

  * •

By T-MODELS, $G;~{}{\sf tl}(H)\vdash e^{\prime}{\sf~{}models~{}}r:{\sf
tl}(\tau)$

∎

The interpretation of this theorem is that, if some expression satisfies a
property, then evaluating that expression results in a value that satisfies
that property for the single time instant in which it is used, and the
remaining rewritten expression will continue to satisfy the remaining “suffix”
of the property. Note that $e^{\prime}$ is typed in a modified environment
${\sf tl}(H)$, which expresses the notion of variables updating across time
instants. We prove this theorem holds in our type system via induction on the
operational semantics derivation (Appendix A).

##  7\. Implementation and Verification of a Robotics Application

The increasing automation of automobiles and other modes of transport sees a
corresponding increase in the responsibilities of software for the safety of
passengers, cargo, and infrastructure (Ames et al., 2014; Platzer, 2018). As
safety-critical CPS, transportation automation is a fitting application for
MARVeLus. We develop our example around vehicle collision avoidance, which is
responsible for maintaining safe separation of the controlled “ego” vehicle
from other vehicles in the environment. We base our model partially on
existing work formally verifying collision avoidance for adaptive cruise
control in autonomous vehicles (Mehra et al., 2015; Chen et al., 2022), with
the primary difference being the use of a discretized model for two moving
vehicles.

We make the simplifying assumption that the vehicles involved move along a
single one-dimensional path, as is the case for autonomous vehicles with
existing lane-keeping, guided buses, or rail vehicles. Thus, the ego vehicle
maintains separation by controlling its acceleration only. We also assume that
the ego vehicle is traveling behind another vehicle, which is the only other
participant in the scenario. The other (henceforth “leader”) vehicle is free
to take arbitrary actions, bounded only by acceleration limits. Besides
externally observable properties (such as velocity and position), the ego
vehicle has no a priori knowledge of the leader’s actions. The property we
verify is that collision never occurs. Given that the ego vehicle starts
behind the leader, this property can be expressed as
$\square(x^{f}<x^{\ell})$; that is, the ego vehicle position $x^{f}$ never
exceeds the leader’s position $x^{\ell}$. Since we are primarily interested in
verifying the control logic, we assume the ego vehicle has perfect knowledge
of its own position and velocity, as well as that of the leader, and the
vehicle instantaneously attains the commanded acceleration.

In our deterministic simulation, we implement the “worst-case” situation, in
which the ego vehicle is accelerating at its maximum allowable rate while the
leader suddenly brakes with maximum force until it completely stops. This
ensures that the ego vehicle will also react safely to the less aggressive
maneuvers that it is more likely to encounter in normal operation.

We model the collision-avoidance scenario as a discrete-time system (Fig. 12),
in which the leader and follower dynamics evolve at a constant time step of
$dt$ seconds. At each time step, vehicle position and velocity are integrated
using the standard kinematic equations of motion, while their accelerations
are determined by the vehicle’s controller in response to the updated velocity
and position values. The ego vehicle initially accelerates at the maximum
possible rate $a_{max}$ and applies full braking acceleration $-b$ when it
determines it is no longer safe to continue accelerating. The leader vehicle
coasts at its starting velocity for a predetermined distance, after which it
brakes with acceleration $-b$ until it comes to a complete stop. The ego
vehicle has no knowledge of precisely when the leader will brake, and must
ensure it always maintains sufficient separation to safely stop at any time.
This is encoded into its controls as the relation
$(x^{f}_{n}+s^{f}_{n})\geq\left(x^{\ell}_{n}+\frac{(v^{\ell}_{n}-b\cdot
dt)^{2}}{2b}+\frac{(v^{\ell}_{n}-b\cdot dt)\cdot dt}{2}\right)$, which uses
the ego vehicle’s anticipated stopping distance under current conditions and
maximum braking $s^{f}$, and the assumption that the leader has already begun
braking, to determine their final positions. If the ego’s anticipated position
reaches or exceeds that of the leader’s, then it brakes until this condition
no longer holds. We constrain velocities to be non-negative, to model vehicles
stopping, rather than accelerating backwards, when the brakes are applied
while stationary. We note that the derivation of $s^{f}$, including its
discretization adjustment, has been covered in existing work (Loos et al.,
2011; Chen et al., 2022).

The formally-verified program consists of 89 lines of code, of which 52 are
executable code (44 for core functionality and 8 for robot interfaces and
logging) and 37 are additional lines for type specifications. Verification on
a 2019 MacBook Pro with a 1.4 GHz Intel Core i5-8257U processor and 16 GB of
memory typically takes less than 1.3 seconds.

$\displaystyle x^{\ell}_{0}$ $\displaystyle=x^{\ell}_{init}$ $\displaystyle
x^{\ell}_{n+1}$ $\displaystyle=x^{\ell}_{n}+v^{\ell}_{n}\cdot dt$
$\displaystyle v^{\ell}_{0}$ $\displaystyle=v_{init}$ $\displaystyle
v^{\ell}_{n+1}$ $\displaystyle=\max(0,v^{\ell}_{n}+a^{\ell}_{n}\cdot dt)$
$\displaystyle a^{\ell}_{0}$ $\displaystyle=0$ $\displaystyle a^{\ell}_{n+1}$
$\displaystyle=\begin{cases}-b&\text{if }(x^{\ell}_{n}\geq x_{brake})\\\
0&\text{otherwise}\\\ \end{cases}$ $\displaystyle x^{f}_{0}$ $\displaystyle=0$
$\displaystyle x^{f}_{n+1}$ $\displaystyle=x^{f}_{n}+v^{f}_{n}\cdot dt$
$\displaystyle v^{f}_{0}$ $\displaystyle=v_{init}$ $\displaystyle v^{f}_{n+1}$
$\displaystyle=\max(0,v^{f}_{n}+a^{f}_{n}\cdot dt)$ $\displaystyle a^{f}_{0}$
$\displaystyle=a_{max}$ $\displaystyle a^{f}_{n+1}$
$\displaystyle=\begin{cases}-b&\text{if
}(x^{f}_{n}+s^{f}_{n})\geq\left(x^{\ell}_{n}+\frac{(v^{\ell}_{n}-b\cdot
dt)^{2}}{2b}+\frac{(v^{\ell}_{n}-b\cdot dt)\cdot dt}{2}\right)\\\
a_{max}&\text{otherwise}\\\ \end{cases}$ $\displaystyle s^{f}_{n}$
$\displaystyle=\frac{(v^{f}_{n})^{2}}{2b}+(1+\frac{a_{max}}{b})(2v^{f}_{n}\cdot
dt+\frac{4a_{max}\cdot dt^{2}}{2})+\frac{v^{f}_{n}\cdot dt}{2}$
$\displaystyle\forall n\ .\ x^{f}_{n}<x^{\ell}_{n}$ Figure 12. Dynamics of the
discrete-time collision avoidance system. $x^{f}$ and $x^{\ell}$ are the
positions of the ego and leader vehicles, $v^{\ell}$ and $v^{f}$ are their
velocities, $a^{\ell}$ and $a^{f}$ their accelerations, and $s^{f}$ the
minimum stopping distance of the ego vehicle if it were to brake at the
current instant. The safety condition specifies that no collision between the
vehicles at any instant.

##  8\. Language Implementation

The refinement type verification is implemented as an additional pass in the
Zélus compiler. This step follows the type checking, which is responsible for
validating the base-types used in the program. The verification algorithm is
built using Z3(de Moura and Bjørner, 2008), an SMT-solver that provides the
support for proving logical propositions and searching for counterexamples.

MARVeLus extends the Zélus Compiler with refinement type checking for the
source code. This additional step identifies refinement type annotation in the
source program, translates the Zélus Abstract Syntax Tree (AST) to an AST with
Z3 data structures, generates verification conditions (VCs) and sends VCs to
the Z3 SMT solver to check for satisfiability. The compilation steps and
interfaces between Zélus and MARVeLus are illustrated in Fig. 13. An archive
of the source code is available in the non-anonymized supplementary materials.

Figure 13. MARVeLus compilation steps

MARVeLus implements refinement type checking through a combination of
synthesis and subtyping, allowing the program’s derived type to differ
somewhat from the specification type, so long as the former is stronger than
the latter. In other words, for an expression $e$ with synthesized type
$\\{v:b~{}|~{}\psi_{1}\\}$ and specification $\\{v:b~{}|~{}\psi_{2}\\}$,
$e:\\{v:b~{}|~{}\psi_{2}\\}$ if $\psi_{1}\implies\psi_{2}$. For instance, the
(T-FBY) rule synthesizes a precise type that is unlikely to match the original
specification. However, because the type produced by (T-FBY) is a precise
definition of the stream’s behavior, type-checking can proceed by attempting
to apply the subtyping relation here.

###  8.1. Generation of Verification Conditions

The refinement type pass in the compiler translates the Zélus AST enhanced
with refinement types to a Z3 AST. In this translation, the program
expressions, operations, patterns and equations are converted into Z3
expression objects. These objects are used to construct boolean expressions
that are used as verification conditions.

The verification conditions are generated following the typing rules defined
in Fig. LABEL:fig:typingrules. Each verification condition’s satisfiability is
checked using the Z3 SMT solver. Conditions proven to be true become powerful
statements when generating other verification conditions in later parts of the
program.

###  8.2. Verification of refinement variables

To verify a refinement typed variable declared in the form $var:\\{w:b\ |\
\varphi\\}=e$, the conjunction of all expressions, $\varphi_{i}$, in the
current environment, $E$, must imply that the refinement $\varphi$ is also
true, $\bigwedge^{E}\varphi_{i}\to\varphi$. From the variable declaration, the
expression $var=e$ is added to the expression environment as an assumption.

An SMT Solver checks satisfiability by finding an example that makes the
expression true. However, our goal is to prove that a verification condition
is always satisfied and we need to rearrange the verification condition so the
Z3 solver cannot find examples that make the verification condition false.
This is achieved by the negation of the initial expression, resulting in the
following verification condition: $\neg(\bigwedge^{E}\varphi_{i}\to\varphi)$.
If this verification condition is satisfied, the refinement type is not valid
and the program shows the counter-examples to the user. On the other hand, if
the verification condition is unsatisfiable, the refinement expression is
valid and the refinement type assumption is added to the expression
environment.

⬇

1 let pi = 3.14159 in

2 let w = 2.*.pi in

3 let y: { v : float | v >= pi} = 4.0 in y

In the above example, pi is a constant variable, w is declared in terms of pi,
and y is annotated with a refinement for which Z3 must check satisfiability.
The expression environment, $E$, after variable y is declared is

$E=(pi=3.14159)\wedge(w=2*pi)\wedge(y=4.0)$

Where the last expression corresponds to the assignment for the newly declared
refinement-type variable. To show the validity of the refinement predicate,
$\varphi\equiv(y>=pi)$, given the variable assignment, the following
verification condition is generated:

$\displaystyle\neg((pi=3.14159)\wedge(w=2*pi)\wedge(y=4.0)\to(y\geq pi))$

This expression is checked to be unsatisfiable by Z3, since $4\geq 3.14159$.
Therefore, the refinement type is valid and the condition $y\geq pi$ is then
added as an assumption to be used in further parts of the program.

###  8.3. Verification of refinement functions

A refinement function can be annotated with refined input arguments and a
refined return type. In the example shown below, f is a unary refinement
function of argument $\\{v:int\ |\ v<0\\}$ and return type $\\{v:int\ |\
v>=0\\}$. The steps to prove the refinement return type are similar to proving
refinement types for variables.

In this proof, a local expression environment is created to store function
body expressions and refinement-type information about the function arguments.
Once the local environment is built, the function return type is used to build
the verification condition that will be checked by Z3.

If the function return type is proven to be always true, it is added to a
function environment. The function environment is used to check that during a
function call, the arguments follow the constraints specified during the
function definition.

Once proved the function application to its argument is represented by an
uninterpreted function, which is supported by Z3.

⬇

1let f (x: { v : float | v < 0.}) : { v : float | v >= 0. } =

2 let y = x *. x in

3 y

In the above example, function $f$ only accepts negative float inputs and the
program ensures that the output is positive. The local expression environment
after function declaration and before the function proof is

$\displaystyle E=(x<0)\wedge(y=x*x)\wedge(v=y)$

Where the first condition is created from the argument refinement-type
definition, the second condition is created from the function body and the
third condition is a binding from the function return type to the function
body return variable. For this example, Z3 checks if the verification
condition $v\geq 0$ is satisfiable using the following verification condition:

$\displaystyle\neg((x<0)\wedge(y=x*x)\wedge(v=y)\to(v\geq 0))$

##  9\. Experimental Methods

Figure 14. System Architecture for the Collision Avoidance Demonstrator

In addition to the aforementioned language extensions, we also made
enhancements to the MARVeLus robot runtime (Chen et al., 2022) to support
multi-robot systems. We found that in practice, the original MARVeLus robotics
extensions were not easily scalable beyond a single robot, with unpredictable
latency being especially problematic for synchronizing multiple robots. We
retain the original software architecture, with separate code for the user
MARVeLus program and runtime, the robots’ kinematic models simulating the
vehicles’ physical attributes, and low-level drivers for sensors, actuators,
and networking (Fig. 14). These components all run locally onboard each robot.
We re-implemented the communications stack to accept synchronization commands
from a centralized server, ensuring timing consistency between experiments. We
selected the M-Bot Mini as our primary development target. The robots run
along an $8\text{\,}\mathrm{m}$ track (Fig. 15). The trusted software base of
our experiment consists of the MARVeLus compiler, runtime, kinematic models,
and sensor and low-level drivers. That is, we trust that sensor data is always
available and valid, and that actuators always attain their commanded values.
We also trust that communications is instantaneous and error-free, and that
data stays sufficiently consistent system-wide. Our verified control code runs
on the follower vehicle, while the leader vehicle acts independently. The
robots are equipped with wheel encoders to measure distance traveled and
velocity, and the leader vehicle reports its position and velocity to the ego,
to simulate the direct sensing that would in practice be performed using
computer vision or LiDAR. The leader and ego vehicles do not otherwise
communicate with one another.

Figure 15. Ego and Leader vehicles traveling on rails

In addition to the collision avoidance scenario described in Section 7, in
which the leader brakes abruptly and stops, we tested two other variations:
(1) The leader remains stationary throughout, simulating an obstacle present
on the track or roadway. (2) The leader decelerates to a constant slow speed,
but does not fully stop, allowing the ego vehicle to continue moving forward
as long as it maintains safe separation. When both robots have stopped, or
after a predetermined period of time in the case of the slow-moving leader,
the final distance between the two robots is recorded.

##  10\. Results

We first ran simulations of the experiments to obtain a basis of comparison
for the experimental results. We then conducted ten trials for each of the
three collision avoidance scenarios described in Section 9. The data obtained
from one trial of the collision avoidance scenario in which the leader brakes
abruptly and comes to a complete stop, is plotted in Fig. 16. Data and plots
from the other experiments are included in the appendix.

Figure 16. Relative kinematic plot for actual and simulated experiments

The kinematic data from the actual experiment differ somewhat from their
simulated counterparts, which we believe arose from subtle differences in
timing, initial conditions, or physical aspects of the real robots which were
not accounted for in our original model. The actual commanded accelerations
differed significantly from the simulation values, which is to be expected as
they are reacting to different positions and velocities at any given moment.
However, in spite of the variations in acceleration, the follower vehicle
maintains a safe distance from the leader vehicle, allowing for the actual
distance and velocity curves to converge to the simulated curves towards the
end of the experiment. After finishing each of the 10 trials in each scenario,
the distance between the leader and follower vehicle in their final positions
was manually measured and recorded. The sample statistics for these collected
distances can be seen in Table 1.

Table 1.  Summary statistics of final distance measurements between vehicles Statistic | Leader braking | Leader decelerating only | Leader stationary
---|---|---|---
Mean | 0.4610 m | 1.0135 m | 0.4826 m
Standard Deviation | 0.06 m | 0.4902 m | 0.0910 m
Minimum | 0.3429 m | 0.7049 m | 0.2794 m
Maximum | 0.5207 m | 2.1082 m | 0.5525 m

##  11\. Related Work

###  11.1. Verification of CPS

Hagen and Tinelli (Hagen and Tinelli, 2008) developed the Kind prover for
Lustre, which introduces SMT-based Lustre verification using $k$-induction, in
order to automate safety proofs on synchronous dataflow programs. As with
Kind, MARVeLus leverages SMT solving to inductively prove properties on
synchronous programs. Although MARVeLus and Kind take different approaches to
verification, a combined approach may lead to rigorous inductive proofs with
reduced effort in finding invariants.

Champion et al. (Champion et al., 2016) introduce Kind 2, an SMT-based model
checker that produces invariants for synchronous programs over a bounded
number of steps. For any successful proof, Kind 2 generates a proof
certificate in a k-induction invariant form that can be validated by other
solvers. In contrast to model-checking approach adopted by Kind 2, MARVeLus
uses type properties directly to verify programs, though the end goal of
reasoning on invariants remains similar.

Kamburjan (Kamburjan, 2021) presents an object-oriented approach to verifying
invariants in hybrid CPS. Similarly to MARVeLus, the rely-guarantee principle
resembles our use of inductive invariants in discrete models, but extends this
to the continuous space as well. To our knowledge, the work does not yet
appear to support real-time execution of verified source code.

###  11.2. Verification via Typing

Languages such as F* (Swamy et al., 2016) and Liquid Haskell (Jhala and Vazou,
2020) demonstrate the utility of allowing types to be augmented with
functional or logical annotations. Both F* and Liquid Haskell interpret type
annotations as constraints which are used to generate verification conditions
for SMT solvers, such as Z3 (de Moura and Bjørner, 2008). Many of the MARVeLus
type system components take cues from these two languages, lifting them into
the space of synchronous programming. We chose to adopt refinement types as
our theory of choice; although it is more constrained than dependent types,
the quantifier-free nature of refinement predicates allows for SMT-decidable
verification conditions and thus predictability (Jhala and Vazou, 2020). A
related application of verification via typing was demonstrated with $\Pi 4$,
a dependently-typed language for networking hardware.(Eichholz et al., 2022)

###  11.3. Verification and Execution

Aside from MARVeLus, VeriPhy (Bohrer et al., 2018) and Koord (Ghosh et al.,
2020a) also combine formal verification with execution on real systems.
Although the goals of MARVeLus and Koord are similar, they differ in that
Koord is intended primarily for higher-level coordination between robots,
while MARVeLus is more concerned with the lower-level controls that may be
specific to individual robots (Ghosh et al., 2020a). VeriPhy (Bohrer et al.,
2018) and similarly Melecha et al. (Malecha et al., 2016) link a high-level
abstract model of CPS to a lower-level implementation, either through runtime
monitoring and switching, or verified translation.

###  11.4. Testing Autonomous Vehicles at Small-Scale

Various experiments have previously been done on small-scale vehicles to
simulate real-world autonomous vehicles (Rusu et al., 2010; Wen et al., 2011;
Rupp et al., 2019). Rupp et al. (Rupp et al., 2019) simulated autonomous
vehicle maneuvers using scaled-down trucks and passenger cars equipped with
sensors, actuators, cameras, and communication devices. ACC was implemented
where two vehicles followed a lead vehicle with a constant distance or time
gap while the lead vehicle tracks a given velocity profile. The experiments
were done both with and without car-to-car communication. Position measurement
in the platooning experiments was done visually using fiducial markers, as
opposed to our simulated distance sensing.

##  12\. Future Work

###  12.1. Invariants

In its current implementation, MARVeLus simply checks typing constraints
supplied by the user, relying on the user to assess the feasibility of
counterexamples to refine the constraints with invariants. During program
verification, one may encounter spurious counterexamples, in which an unsafe
program state is found, but is not feasible in an actual system. These may be
countered by supplying the verifier with invariants, as we have done manually
in our example programs. In general, finding the necessary relations is not
immediately obvious and requires significant additional effort by the user.
There exist works that automate the process of inferring invariants (Ghorbal
and Platzer, 2014), including works that find invariants in synchronous
programs (Champion et al., 2016). Additionally, Liquid Haskell supports
refinement inference through Horn constraint solving (Jhala and Vazou, 2020),
which may be adapted to take advantage of synchronous programming properties.
Although orthogonal to the objectives of the current work, supporting
invariant generation would help to reduce the effort involved in refining
program constraints and improve user experience, particularly for complex
programs.

###  12.2. Trusted Components

Although developing a single language for verification and execution holds the
promise of a compact trusted base, the current implementation makes several
assumptions about the safety of components interacting with the user’s
verified MARVeLus code. Firstly, we assume that the compiler produces a safe
executable from the verified code. Formally-verified compilation of
synchronous programs has been explored in other works (Bourke et al., 2017),
which allows one to directly produce executables that provably reflect their
specified synchronous behavior. Combining our verification methods with a
formally-verified compiler would establish a certified chain of trust in the
compilation process.

Beyond compilation, we also trust the safety of MARVeLus runtime layer. For
instance, we trust that network latency and throughput can be disregarded for
the performance requirements of our runtime. However, this may not always be
the case in real applications, particularly for resource-constrained embedded
systems where the communications overhead may be nontrivial. Thus, it is
necessary to characterize and verify the message-passing protocol employed for
communications between the various robot components, of which there is
existing work (Anand and Knepper, 2015).

We also note that, for simplicity, we chose to write the low-level control
code in C, which includes feedback control for robot speed and heading. This
choice was intentional, as we chose to elide some of the lower-level
implementation details from our verified code example in favor of clarity.
However, we note that certain components, such as motor speed control and
velocity sensing, may be implemented in verified MARVeLus as well.

For CPS operating in the real world, trust goes beyond verifying the “cyber”
components only. Compile-time verification implicitly assumes that system or
environment assumptions hold for the real system. Error sources such as noise
or external perturbations that are not properly modeled may put the system
into an unsafe condition not accounted for in the specification and
verification steps. There is currently no way to enforce these assumptions at
runtime in MARVeLus. Runtime monitoring, perhaps based on the verified
invariants in MARVeLus code could be a potential method for mitigating or
notifying the system of anomalies (Baumeister et al., 2020; Bohrer et al.,
2018). Additionally, one may wish to obtain robustness measures on
verification results, to determine the system’s immunity to disturbances
(Fainekos and Pappas, 2009).

###  12.3. Richer Specifications

Along with simulation and modeling of discrete systems, Zélus supports hybrid
systems defined by differential equations, zero crossings, and labeled
automata (Bourke and Pouzet, 2013). Presently, MARVeLus covers a subset of the
discrete dynamics. Expanding the type theory to cover hybrid behavior would
allow MARVeLus programs to be applied to a much greater range of CPS
applications and provide more realistic models. This may be possible through
the use of differential invariants as in dL (Platzer, 2008) or barrier
certificates The current specification grammar can also be expanded to include
other temporal operators, leading to other properties outside of invariance to
be considered as well, and in fact there is existing work exploring the
semantics of temporal logic in hybrid systems (Jeannin and Platzer, 2014).
Finally, we currently disregard numerical precision and treat most numerical
values as floating-point numbers, which are interpreted internally as reals.
However, this can be imprecise, especially on embedded systems that have
limited support for high-precision floating-point numbers. Some research is
also present in the intersection of probabilistic and synchronous programming,
such as ProbZelus (Baudart et al., 2019), which may enable specification and
analysis of stochastic processes.

##  13\. Conclusion

MARVeLus provides a method for combining refinement types with synchronous
programming to formally verify cyber-physical systems directly in the source
language. Since programming languages typically used for CPS verification and
modeling may not be expressive enough for execution, and languages typically
used to program executable embedded programs may not have well-defined formal
semantics, it is not always clear whether a CPS implementation accurately
reflects its verified counterpart. Synchronous languages are well-suited for
modeling embedded systems; thus, presenting a verifiable and executable
language gives CPS designers increased confidence in developing safety-
critical systems. Part of this confidence comes from the certainty that the
verification results produced are indeed correct; the extended semantics and
type system we develop in this paper, along with the formal proof of type
preservation built upon these extensions of MARVeLus, paves the way towards
building this certainty in the language. By simplifying the process of
obtaining rigorous safety guarantees in CPS and providing a unified platform
in which one can not only verify but also implement CPS, MARVeLus provides an
end-to-end solution for accelerating the development of safety-critical
systems and lowering the barrier for entry to formal verification.

## References

  * (1)
  * Alur et al. (1993) Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei Hsin Ho. 1993.  Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems.  In _Hybrid Systems_ , G. Goos, J. Hartmanis, Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel (Eds.). Vol. 736. Springer Berlin Heidelberg, Berlin, Heidelberg, 209–229.  https://doi.org/10.1007/3-540-57318-6_30 Series Title: Lecture Notes in Computer Science.
  * Ames et al. (2014) Aaron D. Ames, Jessy W. Grizzle, and Paulo Tabuada. 2014\.  Control barrier function based quadratic programs with application to adaptive cruise control. In _53rd IEEE Conference on Decision and Control_. IEEE, Los Angeles, CA, USA, 6271–6278.  https://doi.org/10.1109/CDC.2014.7040372
  * Anand and Knepper (2015) Abhishek Anand and Ross Knepper. 2015.  ROSCoq: Robots Powered by Constructive Reals.  In _Interactive Theorem Proving_ , Christian Urban and Xingyuan Zhang (Eds.). Vol. 9236. Springer International Publishing, Cham, 34–50.  https://doi.org/10.1007/978-3-319-22102-1_3 Series Title: Lecture Notes in Computer Science.
  * Baudart et al. (2019) Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. 2019\.  Reactive Probabilistic Programming.  https://doi.org/10.48550/ARXIV.1908.07563
  * Baumeister et al. (2020) Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer, Maximilian Schwenger, and Christoph Torens. 2020.  RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft.  In _Computer Aided Verification_ , Shuvendu K. Lahiri and Chao Wang (Eds.). Vol. 12225. Springer International Publishing, Cham, 28–39.  https://doi.org/10.1007/978-3-030-53291-8_3 Series Title: Lecture Notes in Computer Science.
  * BeagleBoard ([n. d.]) BeagleBoard. [n. d.].  Robot Control.  https://github.com/beagleboard/librobotcontrol/releases
  * BeagleBoard (2018) BeagleBoard. 2018\.  BeagleBone® Blue.  https://beagleboard.org/blue
  * Benveniste et al. (2014) Albert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, and Marc Pouzet. 2014.  A type-based analysis of causality loops in hybrid systems modelers. In _Proceedings of the 17th international conference on Hybrid systems: computation and control - HSCC ’14_. ACM Press, Berlin, Germany, 71–82.  https://doi.org/10.1145/2562059.2562125
  * Benveniste et al. (2011) Albert Benveniste, Timothy Bourke, Benoît Caillaud, and Marc Pouzet. 2011.  A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code. In _Proceedings of the ninth ACM international conference on Embedded software - EMSOFT ’11_. ACM Press, Taipei, Taiwan, 137.  https://doi.org/10.1145/2038642.2038664
  * Bohrer et al. (2018) Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. 2018.  VeriPhy: verified controller executables from verified cyber-physical system models. In _Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation_. ACM, Philadelphia PA USA, 617–630.  https://doi.org/10.1145/3192366.3192406
  * Borkowski et al. (2022) Michael Borkowski, Niki Vazou, and Ranjit Jhala. 2022\.  Mechanizing Refinement Types (extended).  http://arxiv.org/abs/2207.05617 arXiv:2207.05617 [cs].
  * Boulmé and Hamon (2001) Sylvain Boulmé and Grégoire Hamon. 2001.  Certifying Synchrony for Free.  In _Logic for Programming, Artificial Intelligence, and Reasoning_ , G. Goos, J. Hartmanis, J. Van Leeuwen, Robert Nieuwenhuis, and Andrei Voronkov (Eds.). Vol. 2250. Springer Berlin Heidelberg, Berlin, Heidelberg, 495–506.  https://doi.org/10.1007/3-540-45653-8_34 Series Title: Lecture Notes in Computer Science.
  * Bourke et al. (2017) Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. 2017\.  A Formally Verified Compiler for Lustre.  _Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (2017), 586–601.
  * Bourke and Pouzet (2013) Timothy Bourke and Marc Pouzet. 2013.  Zélus: a synchronous language with ODEs. In _Proceedings of the 16th international conference on Hybrid systems: computation and control - HSCC ’13_. ACM Press, Philadelphia, Pennsylvania, USA, 113.  https://doi.org/10.1145/2461328.2461348
  * Boussinot and de Simone (1991) F. Boussinot and R. de Simone. 1991.  The ESTEREL language.  _Proc. IEEE_ 79, 9 (Sept. 1991), 1293–1304.  https://doi.org/10.1109/5.97299
  * Cardone (2005) Felice Cardone. 2005\.  Benjamin C. Pierce (ed.) Advanced Topics in Types and Programming Languages. The MIT Press (2005) ISBN 0-262-16228-8. £39.95. 574 pp. Hardbound.  _Comput. J._ 49, 1 (09 2005), 130–131.  https://doi.org/10.1093/comjnl/bxh138 arXiv:https://academic.oup.com/comjnl/article-pdf/49/1/130/1161818/bxh138.pdf
  * Caspi et al. (1987) P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. 1987\.  LUSTRE: A Declarative Language for Real-Time Programming. In _Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages_ (Munich, West Germany) _(POPL ’87)_. Association for Computing Machinery, New York, NY, USA, 178–188.  https://doi.org/10.1145/41625.41641
  * Caspi and Pouzet (1996) Paul Caspi and Marc Pouzet. 1996.  Synchronous Kahn networks. In _Proceedings of the first ACM SIGPLAN international conference on Functional programming - ICFP ’96_. ACM Press, Philadelphia, Pennsylvania, United States, 226–238.  https://doi.org/10.1145/232627.232651
  * Caspi and Pouzet (1998) Paul Caspi and Marc Pouzet. 1998.  A Co-iterative Characterization of Synchronous Stream Functions.  _Electronic Notes in Theoretical Computer Science_ 11 (1998), 1–21.  https://doi.org/10.1016/S1571-0661(04)00050-7
  * Champion et al. (2016) Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016.  The Kind 2 Model Checker. In _Computer Aided Verification_ , Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 510–517.
  * Chen et al. (2022) Jiawei Chen, José Luiz Vargas de Mendonça, Shayan Jalili, Bereket Ayele, Bereket Ngussie Bekele, Zhemin Qu, Pranjal Sharma, Tigist Shiferaw, Yicheng Zhang, and Jean-Baptiste Jeannin. 2022.  Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation. In _Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems_ _(FTSCS 2022)_. Association for Computing Machinery, New York, NY, USA, 68–79.  https://doi.org/10.1145/3563822.3568015
  * Colaço et al. (2006) Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. 2006\.  Mixing Signals and Modes in Synchronous Data-Flow Systems. In _Proceedings of the 6th ACM & IEEE International Conference on Embedded Software_ (Seoul, Korea) _(EMSOFT ’06)_. Association for Computing Machinery, New York, NY, USA, 73–82.  https://doi.org/10.1145/1176887.1176899
  * Colaço et al. (2017) Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. 2017\.  SCADE 6: A formal language for embedded critical software development (invited paper). In _2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)_. 1–11.  https://doi.org/10.1109/TASE.2017.8285623
  * Cuoq and Pouzet (2001) Pascal Cuoq and Marc Pouzet. 2001.  Modular Causality in a Synchronous Stream Language.  In _Programming Languages and Systems_ , Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, and David Sands (Eds.). Vol. 2028. Springer Berlin Heidelberg, Berlin, Heidelberg, 237–251.  https://doi.org/10.1007/3-540-45309-1_16 Series Title: Lecture Notes in Computer Science.
  * de Moura and Bjørner (2008) Leonardo de Moura and Nikolaj Bjørner. 2008.  Z3: An Efficient SMT Solver.  In _Tools and Algorithms for the Construction and Analysis of Systems_ , David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, C. R. Ramakrishnan, and Jakob Rehof (Eds.). Vol. 4963. Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340.  https://doi.org/10.1007/978-3-540-78800-3_24 Series Title: Lecture Notes in Computer Science.
  * Eichholz et al. (2022) Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini. 2022\.  Dependently-typed data plane programming.  _Proceedings of the ACM on Programming Languages_ 6, POPL (jan 2022), 1–28.  https://doi.org/10.1145/3498701
  * Fainekos and Pappas (2009) Georgios E Fainekos and George J Pappas. 2009.  Robustness of temporal logic specifications for continuous-time signals$.  _Theoretical Computer Science_ (2009), 30.
  * Florence et al. (2019) Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler. 2019.  A Calculus for Esterel: If Can, Can. If No Can, No Can.  _Proc. ACM Program. Lang._ 3, POPL, Article 61 (jan 2019), 29 pages.  https://doi.org/10.1145/3290374
  * Ghorbal and Platzer (2014) Khalil Ghorbal and André Platzer. 2014.  Characterizing Algebraic Invariants by Differential Radical Invariants.  In _Tools and Algorithms for the Construction and Analysis of Systems_ , David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, Erika Ábrahám, and Klaus Havelund (Eds.). Vol. 8413. Springer Berlin Heidelberg, Berlin, Heidelberg, 279–294.  https://doi.org/10.1007/978-3-642-54862-8_19 Series Title: Lecture Notes in Computer Science.
  * Ghosh et al. (2020a) Ritwika Ghosh, Chiao Hsieh, Sasa Misailovic, and Sayan Mitra. 2020a.  Koord: A Language for Programming and Verifying Distributed Robotics Application.  _Proc. ACM Program. Lang._ 4, OOPSLA, Article 232 (nov 2020), 30 pages.  https://doi.org/10.1145/3428300
  * Ghosh et al. (2020b) Ritwika Ghosh, Joao P. Jansch-Porto, Chiao Hsieh, Amelia Gosse, Minghao Jiang, Hebron Taylor, Peter Du, Sayan Mitra, and Geir Dullerud. 2020b.  CyPhyHouse: A programming, simulation, and deployment toolchain for heterogeneous distributed coordination. In _2020 IEEE International Conference on Robotics and Automation (ICRA)_. 6654–6660.  https://doi.org/10.1109/ICRA40945.2020.9196513
  * Hagen and Tinelli (2008) George Hagen and Cesare Tinelli. 2008.  Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. In _2008 Formal Methods in Computer-Aided Design_. 1–9.  https://doi.org/10.1109/FMCAD.2008.ECP.19
  * Halbwachs et al. (1991a) N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991a.  The synchronous data flow programming language LUSTRE.  _Proc. IEEE_ 79, 9 (Sept. 1991), 1305–1320.  https://doi.org/10.1109/5.97300
  * Halbwachs et al. (1991b) N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991b.  The synchronous data flow programming language LUSTRE.  _Proc. IEEE_ 79, 9 (1991), 1305–1320.  https://doi.org/10.1109/5.97300
  * Jeannin and Platzer (2014) Jean-Baptiste Jeannin and André Platzer. 2014.  dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems.  In _Automated Reasoning_ , David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Alfred Kobsa, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Demetri Terzopoulos, Doug Tygar, Gerhard Weikum, Stéphane Demri, Deepak Kapur, and Christoph Weidenbach (Eds.). Vol. 8562. Springer International Publishing, Cham, 292–306.  https://doi.org/10.1007/978-3-319-08587-6_22 Series Title: Lecture Notes in Computer Science.
  * Jhala and Vazou (2020) Ranjit Jhala and Niki Vazou. 2020.  Refinement Types: A Tutorial.  https://doi.org/10.48550/ARXIV.2010.07763
  * Kamburjan (2021) Eduard Kamburjan. 2021\.  From post-conditions to post-region invariants: deductive verification of hybrid objects. In _Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control_. ACM, Nashville Tennessee, 1–11.  https://doi.org/10.1145/3447928.3456633
  * LCM Project ([n. d.]) LCM Project. [n. d.].  Lightweight Communications and Marshalling.  https://lcm-proj.github.io/index.html
  * Loos et al. (2011) Sarah M. Loos, André Platzer, and Ligia Nistor. 2011\.  Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified.  In _FM 2011: Formal Methods_ , Michael Butler and Wolfram Schulte (Eds.). Vol. 6664. Springer Berlin Heidelberg, Berlin, Heidelberg, 42–56.  https://doi.org/10.1007/978-3-642-21437-0_6 Series Title: Lecture Notes in Computer Science.
  * Malecha et al. (2016) Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, and Sorin Lerner. 2016.  Towards foundational verification of cyber-physical systems. In _2016 Science of Security for Cyber-Physical Systems Workshop (SOSCYPS)_. 1–5.  https://doi.org/10.1109/SOSCYPS.2016.7580000
  * Manna and Pnueli (1992) Zohar Manna and Amir Pnueli. 1992.  _The Temporal Logic of Reactive and Concurrent Systems_.  Springer New York, New York, NY.  https://doi.org/10.1007/978-1-4612-0931-7
  * Mehra et al. (2015) Aakar Mehra, Wen-Loong Ma, Forrest Berg, Paulo Tabuada, Jessy W. Grizzle, and Aaron D. Ames. 2015\.  Adaptive cruise control: Experimental validation of advanced controllers on scale-model cars. In _2015 American Control Conference (ACC)_. IEEE, Chicago, IL, USA, 1411–1418.  https://doi.org/10.1109/ACC.2015.7170931
  * Ou et al. (2004) Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004\.  Dynamic typing with dependent types. In _Exploring New Frontiers of Theoretical Informatics: IFIP 18th World Computer Congress TC1 3rd International Conference on Theoretical Computer Science (TCS2004) 22–27 August 2004 Toulouse, France_. Springer, 437–450.
  * Parissis (1996) Ioannis Parissis. 1996\.  Test de logiciels synchrones spécifiés en Lustre.  (1996), 207.
  * Platzer (2008) André Platzer. 2008\.  Differential Dynamic Logic for Hybrid Systems.  _Journal of Automated Reasoning_ 41, 2 (Aug. 2008), 143–189.  https://doi.org/10.1007/s10817-008-9103-8
  * Platzer (2018) André Platzer. 2018\.  _Logical Foundations of Cyber-Physical Systems_.  Springer International Publishing, Cham.  https://doi.org/10.1007/978-3-319-63588-0
  * Pnueli (1977) Amir Pnueli. 1977\.  The temporal logic of programs. In _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_. 46–57.  https://doi.org/10.1109/SFCS.1977.32 ISSN: 0272-5428.
  * Ratel (1992) Christophe Ratel. 1992\.  _Définition et Réalisation d’un Outil de Vérification Formelle de Programmes LUSTRE: le Système LESAR_.  Ph. D. Dissertation. Université Joseph Fourier.  https://tel.archives-ouvertes.fr/file/index/docid/341223/filename/Ratel.Christophe_1992_these.pdf
  * Rondon et al. (2008) Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008\.  Liquid types. In _Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation - PLDI ’08_. ACM Press, Tucson, AZ, USA, 159\.  https://doi.org/10.1145/1375581.1375602
  * Rupp et al. (2019) Astrid Rupp, Markus Tranninger, Raffael Wallner, Jasmina Zubača, Martin Steinberger, and Martin Horn. 2019.  Fast and low-cost testing of advanced driver assistance systems using small-scale vehicles.  _IFAC-PapersOnLine_ 52, 5 (2019), 34–39.
  * Rusu et al. (2010) CG Rusu, IT Birou, and E Szöke. 2010.  Fuzzy based obstacle avoidance system for autonomous mobile robot. In _2010 IEEE International Conference on Automation, Quality and Testing, Robotics (AQTR)_ , Vol. 1. IEEE, 1–6.
  * Swamy et al. (2016) Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. 2016\.  Dependent Types and Multi-Monadic Effects in F*.  _SIGPLAN Not._ 51, 1 (jan 2016), 256–270.  https://doi.org/10.1145/2914770.2837655
  * Tarski (1951) Alfred Tarski. 1951\.  A Decision Method for Elementary Algebra and Geometry.  In _Quantifier Elimination and Cylindrical Algebraic Decomposition_. Springer, 24–84.
  * Vazou et al. (2014) Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014\.  Refinement types for Haskell. In _Proceedings of the 19th ACM SIGPLAN international conference on Functional programming_ _(ICFP ’14)_. Association for Computing Machinery, New York, NY, USA, 269–282.  https://doi.org/10.1145/2628136.2628161