
Recent developments in formal verification have identified approximate
liftings (also known as approximate couplings) as a clean, compositional
abstraction for proving differential privacy. This construction can be defined
in two styles. Earlier definitions require the existence of one or more witness
distributions, while a recent definition by Sato uses universal quantification
over all sets of samples. These notions have each have their own strengths: the
universal version is more general than the existential ones, while existential
liftings are known to satisfy more precise composition principles.
We propose a novel, existential version of approximate lifting, called
$\star$lifting, and show that it is equivalent to Sato's construction for
discrete probability measures. Our work unifies all known notions of
approximate lifting, yielding cleaner properties, more general constructions,
and more precise composition theorems for both styles of lifting, enabling
richer proofs of differential privacy. We also clarify the relation between
existing definitions of approximate lifting, and consider more general
approximate liftings based on $f$divergences.

Data sharing among partnersusers, organizations, companiesis crucial
for the advancement of data analytics in many domains. Sharing through secure
computation and differential privacy allows these partners to perform private
computations on their sensitive data in controlled ways. However, in reality,
there exist complex relationships among members. Politics, regulations,
interest, trust, data demands and needs are one of the many reasons. Thus,
there is a need for a mechanism to meet these conflicting relationships on data
sharing. This paper presents Curie, an approach to exchange data among members
whose membership has complex relationships. The CPL policy language that allows
members to define the specifications of data exchange requirements is
introduced. Members (partners) assert who and what to exchange through their
local policies and negotiate a global sharing agreement. The agreement is
implemented in a multiparty computation that guarantees sharing among members
will comply with the policy as negotiated. The use of Curie is validated
through an example of a health care application built on recently introduced
secure multiparty computation and differential privacy frameworks, and policy
and performance tradeoffs are explored.

Structure editors allow programmers to edit the tree structure of a program
directly. This can have cognitive benefits, particularly for novice and
enduser programmers. It also simplifies matters for tool designers, because
they do not need to contend with malformed program text. This paper defines
Hazelnut, a structure editor based on a small bidirectionally typed lambda
calculus extended with holes and a cursor. Hazelnut goes one step beyond
syntactic wellformedness: its edit actions operate over statically meaningful
incomplete terms. Naively, this would force the programmer to construct terms
in a rigid "outsidein" manner. To avoid this problem, the action semantics
automatically places terms assigned a type that is inconsistent with the
expected type inside a hole. This safely defers the type consistency check
until the term inside the hole is finished. Hazelnut is a foundational
typetheoretic account of typed structure editing, rather than an enduser tool
itself. To that end, we describe how Hazelnut's rich metatheory, which we have
mechanized in Agda, guides the definition of an extension to the calculus. We
also discuss various plausible evaluation strategies for terms with holes, and
in so doing reveal connections with gradual typing and contextual modal type
theory, the CurryHoward interpretation of contextual modal logic. Finally, we
discuss how Hazelnut's semantics lends itself to implementation as a functional
reactive program. Our reference implementation is written using js_of_ocaml.

This paper describes the application of a highlevel language and method in
developing simpler specifications of more complex variants of the Paxos
algorithm for distributed consensus. The specifications are for MultiPaxos
with preemption, replicated state machine, and reconfiguration and optimized
with state reduction and failure detection. The language is DistAlgo. The key
is to express complex control flows and synchronization conditions precisely at
a high level, using nondeterministic waits and messagehistory queries. We
obtain complete executable specifications that are almost completely
declarativeupdating only a number for the protocol round besides the sets of
messages sent and received.
We show the following results: 1.English and pseudocode descriptions of
distributed algorithms can be captured completely and precisely at a high
level, without adding, removing, or reformulating algorithm details to fit
lowerlevel, more abstract, or less direct languages. 2.We created higherlevel
control flows and synchronization conditions than all previous specifications,
and obtained specifications that are much simpler and smaller, even matching or
smaller than abstract specifications that omit many algorithm details. 3.The
simpler specifications led us to easily discover useless replies, unnecessary
delays, and liveness violations (if messages can be lost) in previous published
specifications, by just following the simplified algorithm flows. 4.The
resulting specifications can be executed directly, and we can express
optimizations cleanly, yielding drastic performance improvement over naive
execution and facilitating a general method for merging processes. 5.We
systematically translated the resulting specifications into TLA+ and developed
machinechecked safety proofs, which also allowed us to detect and fix a subtle
safety violation in an earlier unpublished specification.

We present a new dynamic partialorder reduction method for stateless model
checking of concurrent programs. A common approach for exploring program
behaviors relies on enumerating the traces of the program, without storing the
visited states (aka stateless exploration). As the number of distinct traces
grows exponentially, dynamic partialorder reduction (DPOR) techniques have
been successfully used to partition the space of traces into equivalence
classes (Mazurkiewicz partitioning), with the goal of exploring only few
representative traces from each class.
We introduce a new equivalence on traces under sequential consistency
semantics, which we call the observation equivalence. Two traces are
observationally equivalent if every read event observes the same write event in
both traces. While the traditional Mazurkiewicz equivalence is controlcentric,
our new definition is datacentric. We show that our observation equivalence is
coarser than the Mazurkiewicz equivalence, and in many cases even exponentially
coarser. We devise a DPOR exploration of the trace space, called datacentric
DPOR, based on the observation equivalence. For acyclic architectures, our
algorithm is guaranteed to explore exactly one representative trace from each
observation class, while spending polynomial time per class. Hence, our
algorithm is optimal wrt the observation equivalence, and in several cases
explores exponentially fewer traces than any enumerative method based on the
Mazurkiewicz equivalence. For cyclic architectures, we consider an equivalence
between traces which is finer than the observation equivalence; but coarser
than the Mazurkiewicz equivalence, and in some cases is exponentially coarser.
Our datacentric DPOR algorithm remains optimal under this trace equivalence.

We propose an underapproximate reachability analysis algorithm for programs
running under the POWER memory model, in the spirit of the work on
contextbounded analysis intitiated by Qadeer et al. in 2005 for detecting bugs
in concurrent programs (supposed to be running under the classical SC model).
To that end, we first introduce a new notion of contextbounding that is
suitable for reasoning about computations under POWER, which generalizes the
one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a
polynomial size reduction of the contextbounded state reachability problem
under POWER to the same problem under SC: Given an input concurrent program P,
our method produces a concurrent program P' such that, for a fixed number of
context switches, running P' under SC yields the same set of reachable states
as running P under POWER. The generated program P' contains the same number of
processes as P, and operates on the same data domain. By leveraging the
standard model checker CBMC, we have implemented a prototype tool and applied
it on a set of benchmarks, showing the feasibility of our approach.

Diverse selection statements  ifthenelse, switch and trycatch  are
commonly used in modern programming languages. To make things simple, we
propose a unifying statement for selection. This statement is of the form
seqor(G_1,...,G_n) where each $G_i$ is a statement. It has a a simple
semantics: sequentially choose the first successful statement $G_i$ and then
proceeds with executing $G_i$. Examples will be provided for this statement.

To model relaxed memory, we propose confusionfree event structures over an
alphabet with a justification relation. Executions are modeled by justified
configurations, where every read event has a justifying write event.
Justification alone is too weak a criterion, since it allows cycles of the kind
that result in socalled thinair reads. Acyclic justification forbids such
cycles, but also invalidates event reorderings that result from compiler
optimizations and dynamic instruction scheduling. We propose the notion of
welljustification, based on a gamelike model, which strikes a middle ground.
We show that welljustified configurations satisfy the DRF theorem: in any
datarace free program, all welljustified configurations are sequentially
consistent. We also show that relyguarantee reasoning is sound for
welljustified configurations, but not for justified configurations. For
example, welljustified configurations are typesafe.
Welljustification allows many, but not all reorderings performed by relaxed
memory. In particular, it fails to validate the commutation of independent
reads. We discuss variations that may address these shortcomings.

We extend functional languages with highlevel exception handling. To be
specific, we allow sequentialdisjunction expressions of the form $E_0
\bigtriangledown E_1$ where $E_0, E_1$ are expressions. These expressions have
the following intended semantics: sequentially $choose$ the first successful
$E_i$ and evaluate $E_i$ where $i$ = 0 or 1. These expressions thus allow us to
specify an expression $E_0$ with the failurehandling (exception handling)
routine, i.e., expression $E_1$. We also discuss the class of
sequentialconjunction function declarations which is a dual of the former.

Static cache analysis characterizes a program's cache behavior by determining
in a sound but approximate manner which memory accesses result in cache hits
and which result in cache misses. Such information is valuable in optimizing
compilers, worstcase execution time analysis, and sidechannel attack
quantification and mitigation.Cache analysis is usually performed as a
combination of `must' and `may' abstract interpretations, classifying
instructions as either `always hit', `always miss', or `unknown'. Instructions
classified as `unknown' might result in a hit or a miss depending on program
inputs or the initial cache state. It is equally possible that they do in fact
always hit or always miss, but the cache analysis is too coarse to see it.Our
approach to eliminate this uncertainty consists in (i) a novel abstract
interpretation able to ascertain that a particular instruction may definitely
cause a hit and a miss on different paths, and (ii) an exact analysis, removing
all remaining uncertainty, based on model checking, using
abstractinterpretation results to prune down the model for scalability.We
evaluated our approach on a variety of examples; it notably improves precision
upon classical abstract interpretation at reasonable cost.

ProbNetKAT is a probabilistic extension of NetKAT with a denotational
semantics based on Markov kernels. The language is expressive enough to
generate continuous distributions, which raises the question of how to compute
effectively in the language. This paper gives an new characterization of
ProbNetKAT's semantics using domain theory, which provides the foundation
needed to build a practical implementation. We show how to use the semantics to
approximate the behavior of arbitrary ProbNetKAT programs using distributions
with finite support. We develop a prototype implementation and show how to use
it to solve a variety of problems including characterizing the expected
congestion induced by different routing schemes and reasoning probabilistically
about reachability in a network.

We present Low*, a language for lowlevel programming and verification, and
its application to highassurance optimized cryptographic libraries. Low* is a
shallow embedding of a small, sequential, wellbehaved subset of C in F*, a
dependentlytyped variant of ML aimed at program verification. Departing from
ML, Low* does not involve any garbage collection or implicit heap allocation;
instead, it has a structured memory model \`a la CompCert, and it provides the
control required for writing efficient lowlevel securitycritical code.
By virtue of typing, any Low* program is memory safe. In addition, the
programmer can make full use of the verification power of F* to write
highlevel specifications and verify the functional correctness of Low* code
using a combination of SMT automation and sophisticated manual proofs. At
extraction time, specifications and proofs are erased, and the remaining code
enjoys a predictable translation to C. We prove that this translation preserves
semantics and sidechannel resistance.
We provide a new compiler backend from Low* to C and, to evaluate our
approach, we implement and verify various cryptographic algorithms,
constructions, and tools for a total of about 28,000 lines of code,
specification and proof. We show that our Low* code delivers performance
competitive with existing (unverified) C cryptographic libraries, suggesting
our approach may be applicable to largerscale lowlevel software.

Bidirectional typechecking, in which terms either synthesize a type or are
checked against a known type, has become popular for its applicability to a
variety of type systems, its error reporting, and its ease of implementation.
Following principles from proof theory, bidirectional typing can be applied to
many type constructs. The principles underlying a bidirectional approach to
indexed types (generalized algebraic datatypes) are less clear. Building on
prooftheoretic treatments of equality, we give a declarative specification of
typing based on focalization. This approach permits declarative rules for
coverage of pattern matching, as well as support for firstclass existential
types using a focalized subtyping judgment. We use refinement types to avoid
explicitly passing equality proofs in our term syntax, making our calculus
similar to languages such as Haskell and OCaml. We also extend the declarative
specification with an explicit rules for deducing when a type is principal,
permitting us to give a complete declarative specification for a rich type
system with significant type inference. We also give a set of algorithmic
typing rules, and prove that it is sound and complete with respect to the
declarative system. The proof requires a number of technical innovations,
including proving soundness and completeness in a mutually recursive fashion.

Dataflow matrix machines are selfreferential generalized recurrent neural
nets. The selfreferential mechanism is provided via a stream of matrices
defining the connectivity and weights of the network in question. A natural
question is: what should play the role of untyped lambdacalculus for this
programming architecture? The proposed answer is a discipline of programming
with only one kind of streams, namely the streams of appropriately shaped
matrices. This yields Pure Dataflow Matrix Machines which are networks of
transformers of streams of matrices capable of defining a pure dataflow matrix
machine.

We consider a programming language based on the lamplighter group that uses
only composition and iteration as control structures. We derive generating
functions and counting formulas for this language and special subsets of it,
establishing lower and upper bounds on the growth rate of semantically distinct
programs. Finally, we show how to sample random programs and analyze the
distribution of runtimes induced by such sampling.

Choreographic Programming is a programming paradigm for building concurrent
programs that are deadlockfree by construction, as a result of programming
communications declaratively and then synthesising process implementations
automatically. Despite strong interest on choreographies, a foundational model
that explains which computations can be performed with the hallmark constructs
of choreographies is still missing.
In this work, we introduce Core Choreographies (CC), a model that includes
only the core primitives of choreographic programming. Every computable
function can be implemented as a choreography in CC, from which we can
synthesise a process implementation where independent computations run in
parallel. We discuss the design of CC and argue that it constitutes a canonical
model for choreographic programming.

We present a new approach for building sourcetosource transformations that
can run on multiple programming languages, based on a new way of representing
programs called incremental parametric syntax. We implement this approach in
Haskell in our Cubix system, and construct incremental parametric syntaxes for
C, Java, JavaScript, Lua, and Python. We demonstrate a wholeprogram
refactoring tool that runs on all of them, along with three smaller
transformations that each run on several. Our evaluation shows that (1) once a
transformation is written, little work is required to configure it for a new
language (2) transformations built this way output readable code which preserve
the structure of the original, according to participants in our human study,
and (3) our transformations can still handle language cornercases, as
validated on compiler test suites.

The memory model for RISCV, a newly developed open source ISA, has not been
finalized yet and thus, offers an opportunity to evaluate existing memory
models. We believe RISCV should not adopt the memory models of POWER or ARM,
because their axiomatic and operational definitions are too complicated. We
propose two new weak memory models: WMM and WMMS, which balance definitional
simplicity and implementation flexibility differently. Both allow all
instruction reorderings except overtaking of loads by a store. We show that
this restriction has little impact on performance and it considerably
simplifies operational definitions. It also rules out the outofthinair
problem that plagues many definitions. WMM is simple (it is similar to the
Alpha memory model), but it disallows behaviors arising due to shared store
buffers and shared writethrough caches (which are seen in POWER processors).
WMMS, on the other hand, is more complex and allows these behaviors. We give
the operational definitions of both models using Instantaneous Instruction
Execution (I2E), which has been used in the definitions of SC and TSO. We also
show how both models can be implemented using conventional cachecoherent
memory systems and outoforder processors, and encompasses the behaviors of
most known optimizations.

Structured reversible flowchart languages is a class of imperative reversible
programming languages allowing for a simple diagrammatic representation of
control flow built from a limited set of control flow structures. This class
includes the reversible programming language Janus (without recursion), as well
as more recently developed reversible programming languages such as RCORE and
RWHILE.
In the present paper, we develop a categorical foundation for this class of
languages based on inverse categories with joins. We generalize the notion of
extensivity of restriction categories to one that may be accommodated by
inverse categories, and use the resulting decisions to give a reversible
representation of predicates and assertions. This leads to a categorical
semantics for structured reversible flowcharts, which we show to be
computationally sound and adequate, as well as equationally fully abstract with
respect to the operational semantics under certain conditions.

Being able to soundly estimate roundoff errors of finiteprecision
computations is important for many applications in embedded systems and
scientific computing. Due to the discrepancy between continuous reals and
discrete finiteprecision values, automated static analysis tools are highly
valuable to estimate roundoff errors. The results, however, are only as correct
as the implementations of the static analysis tools. This paper presents a
formally verified and modular tool which fully automatically checks the
correctness of finiteprecision roundoff error bounds encoded in a certificate.
We present implementations of certificate generation and checking for both Coq
and HOL4 and evaluate it on a number of examples from the literature. The
experiments use both inlogic evaluation of Coq and HOL4, and execution of
extracted code outside of the logics: we benchmark Coq extracted unverified
OCaml code and a CakeMLgenerated verified binary.

Dataflow matrix machines arise naturally in the context of synchronous
dataflow programming with linear streams. They can be viewed as a rather
powerful generalization of recurrent neural networks. Similarly to recurrent
neural networks, large classes of dataflow matrix machines are described by
matrices of numbers, and therefore dataflow matrix machines can be synthesized
by computing their matrices. At the same time, the evidence is fairly strong
that dataflow matrix machines have sufficient expressive power to be a
convenient generalpurpose programming platform. Because of the network nature
of this platform, programming patterns often correspond to patterns of
connectivity in the generalized recurrent neural networks understood as
programs. This paper explores a variety of such programming patterns.

We introduce Dynamic SOS as a framework for describing semantics of
programming languages that include dynamic software upgrades, for upgrading
software code during runtime. Dynamic SOS (DSOS) is built on top of the
Modular SOS of P. Mosses, with an underlying category theory formalization. The
idea of Dynamic SOS is to bring out the essential differences between dynamic
upgrade constructs and program execution constructs. The important feature of
Modular SOS (MSOS) that we exploit in DSOS is the sharp separation of the
program execution code from the additional (data) structures needed at
runtime. In DSOS we aim to achieve the same modularity and decoupling for
dynamic software upgrades. This is partly motivated by the long term goal of
having machinecheckable proofs for general results like type safety.
We exemplify Dynamic SOS on two languages supporting dynamic software
upgrades, namely the Clike Proteus, which supports updating of variables,
functions, records, or types at specific program points, and Creol, which
supports dynamic class upgrades in the setting of concurrent objects. Existing
type analyses for software upgrades can be done on top of DSOS too, as we
illustrate for Proteus.
As a side result we define of a general encapsulating construction on Modular
SOS useful in situations where a form of encapsulation of the execution is
needed. We use encapsulation in the Creol setting of concurrent objectoriented
programming with active objects and asynchronous method calls.

Programming a parallel computing system that consists of several thousands or
even up to a million message passing processing units may ask for a language
that supports waiting for and sending messages over hardware channels. As
programs are looked upon as state machines, the language provides syntax to
implement a main event driven loop. The language presented herewith surely will
not serve as a generic programming language for any arbitrary task. Its main
purpose is to allow for a prototypical implementation of a dynamic software
system as a proof of concept.

We describe the LoopInvGen tool for generating loop invariants that can
provably guarantee correctness of a program with respect to a given
specification. LoopInvGen is an efficient implementation of the inference
technique originally proposed in our earlier work on PIE
(https://doi.org/10.1145/2908080.2908099).
In contrast to existing techniques, LoopInvGen is not restricted to a fixed
set of features  atomic predicates that are composed together to build
complex loop invariants. Instead, we start with no initial features, and use
program synthesis techniques to grow the set on demand. This not only enables a
less onerous and more expressive approach, but also appears to be significantly
faster than the existing tools over the SyGuSCOMP 2017 benchmarks from the INV
track.

Modern networks achieve robustness and scalability by maintaining states on
their nodes. These nodes are referred to as middleboxes and are essential for
network functionality. However, the presence of middleboxes drastically
complicates the task of network verification. Previous work showed that the
problem is undecidable in general and EXPSPACEcomplete when abstracting away
the order of packet arrival.
We describe a new algorithm for conservatively checking isolation properties
of stateful networks. The asymptotic complexity of the algorithm is polynomial
in the size of the network, albeit being exponential in the maximal number of
queries of the local state that a middlebox can do, which is often small.
Our algorithm is sound, i.e., it can never miss a violation of safety but may
fail to verify some properties. The algorithm performs onthe fly abstract
interpretation by (1) abstracting away the order of packet processing and the
number of times each packet arrives, (2) abstracting away correlations between
states of different middleboxes and channel contents, and (3) representing
middlebox states by their effect on each packet separately, rather than taking
into account the entire state space. We show that the abstractions do not lose
precision when middleboxes may reset in any state. This is encouraging since
many real middleboxes reset, e.g., after some session timeout is reached or due
to hardware failure.