# Invited Talks and Tutorials

### Invited Talks

#### The seL4 verification journey: how have the challenges and opportunities evolved

##### June Andronick

**ABSTRACT:** The formal verification journey of the seL4 microkernel is
nearing two decades, and still has an busy roadmap for the years
ahead. It started as a research project aiming for a highly
challenging problem with the potential of significant impact. Today, a
whole ecosystem of developers, researchers, adopters and supporters
are part of the seL4 community. With increasing uptake and adoption,
seL4 is evolving, supporting more platforms, architectures,
configurations, and features. This creates both opportunities and
challenges: verification is what makes seL4 unique; as the seL4 code
evolves, so must its formal proofs. With more than a million lines of
formal, machine-checked proofs, seL4 is the most highly assured OS
kernel, with proofs of an increasing number of properties (functional
correctness, binary correctness, security –integrity and
confidentiality– and system initialisation) and for an increasing
number of hardware architectures: Arm (32-bit), x86 (64-bit) and
RISC-V (64-bit), with proofs now starting for Arm (64-bit). In this
talk we will reflect on the evolution of the challenges and
opportunities the seL4 verification faced along its long, and
continuing, journey.

**BIO:** June Andronick is CEO and co-founder of Proofcraft, providing
commercial support for software verification in general and the seL4
microkernel verification in particular. She is also CEO of the seL4
Foundation, and conjoint Professor at UNSW Sydney. Her technical
expertise is in increasing the reliability of critical software
systems, by mathematically proving that the code behaves as expected
and satisfies security and safety requirements. She previously led the
Trustworthy Systems group, world-leading in the area of verified
operating systems software, known worldwide for the formal
verification of the seL4 microkernel. She was recognised in 2011 by
MIT’s Technology Review as one of the world’s top young innovators
(TR35). She holds a PhD in Computer Science from the University of
Paris-Sud, France.

#### Why do things go wrong (or right)? Applications of causal reasoning to verification

##### Hana Chockler

**ABSTRACT:** In this talk I will look at the connections between
causality and learning from one side, and verification and synthesis
from the other side. I will introduce the relevant concepts and
discuss how causality and learning can help to improve the quality of
systems and reduce the amount of human effort in designing and
verifying systems. I will (briefly) introduce the theory of actual
causality as defined by Halpern and Pearl. This theory turns out to be
extremely useful in various areas of computer science due to a good
match between the results it produces and our intuition. I will
illustrate the definitions by examples from formal verification. I
will also argue that active learning can be viewed as a type of causal
discovery. Tackling the problem of reducing the human effort from the
other direction, I will discuss ways to improve the quality of
specifications and will focus in particular on synthesis.

**BIO:** Hana Chockler is a Principal Scientist at a startup company causaLens
and a Reader (Associate Professor) in Formal Methods in the Department
of Informatics at King’s College London (KCL). Prior to joining KCL in
2013, Hana worked at IBM Research in the formal verification and
software engineering departments. Her research interests span a wide
variety of topics, including formal verification and synthesis of
hardware and software, fundamental concepts in causality and its
applications to a variety of domains, learning, and explainable AI.

### Tutorials

#### On applying Model Checking in Formal Verification

##### Håkan Hjort

**Slides**
**Video (Part 1)**
**Video (Part 2)**

**ABSTRACT:** Use of Hardware model checking in the EDA industry is wide spread
and now considered an essential part of verification. While there are many
papers, and books, about SAT, SMT and Symbolic model checking, often very little
is written about how these methods can be applied. Choices made when modeling
systems can have large impacts on applicability and scalability. There is
generally no formal semantics defined for the hardware design languages, nor for
the intermediate representations in common use. As unsatisfactory as it may be,
industry conventions and behaviour exhibited by real hardware have instead been
the guides. In this tutorial we will give an overview of some of the steps
needed to apply hardware model checking in an EDA tool. We will touch on
synthesis, hierarchy flattening, gate lowering, driver resolution, issues with
discrete/synchronous time models, feedback loops and environment constraints,
input rating and initialisation/reset.

**BIO**: Håkan Hjort has more than 20 years of industrial experience earned during his
tenure at Safelogic, Jasper Design Automation and Cadence Design Systems, doing
everything from language frontends to SAT solvers. Håkan studied Computer
Science and Engineering at Chalmers, Gothenburg, and is today a Senior Software
Architect in the System&Verification Group at Cadence, working on the formal
verification tool Jasper.

#### Verification of Distributed Protocols: Decidable Modeling and Invariant Inference

##### Oded Padon

**Slides**
**Video (Part 1)**
**Video (Part 2)**

**ABSTRACT:** Verification of distributed protocols and systems, where both the
number of nodes in the systems and the state-space of each node are unbounded,
is a long-standing research goal. In recent years, efforts around the Ivy
verification tool have pushed a strategy of modeling distributed protocols and
systems in a new way that enables decidable deductive verification, i.e., given
a candidate inductive invariant, it is possible to *automatically* check if
it is inductive, and to produce a *finite* counterexample to induction in
case it is not inductive. Complex protocols require quantifiers in both models
and their invariants, including forall-exists quantifier alternations. Still, it
is possible to obtain decidability by enforcing a stratification structure on
quantifier alternations, often achieved using modular decomposition techniques,
which are supported by Ivy. Stratified quantifiers lead not only to theoretical
decidability, but to reliably good solver performance in practice, which is in
contrast to the typical instability of SMT solvers over formulas with complex
quantification.

Reliable automation of invariant checking and finite counterexamples open the path to automating invariant inference. An invariant inference algorithm can propose a candidate invariant, automatically check it, and get a finite counterexample that can be used to inform the next candidate. For a complex protocol, this check would typically be performed thousands of times before an invariant is found, so reliable automation of invariant checking is a critical enabler. Recently, several invariant inference algorithms have been developed that can find complex quantified invariants for challenging protocols, including Paxos and some of its most intricate variants.

In the tutorial I will provide an overview of Ivy’s principles and techniques for modeling distributed protocols in a decidable fragment of first-order logic. I will then survey several recently developed invariant inference algorithms for quantified invariants, and present one such algorithm in depth: Primal-Dual Houdini. Primal-Dual Houdini is based on a new mathematical duality, and is obtained by deriving the formal dual of the well-known Houdini algorithm. As a result, Primal-Dual Houdini possesses an interesting formal symmetry between the search for proofs and for counterexamples.

**BIO**: Oded Padon is a researcher at VMware Research. Prior to joining VMware Research,
Oded was a postdoctoral scholar at Stanford University. He completed his PhD
from Tel Aviv University. Oded’s research interests include programming
languages, formal verification, distributed systems, and quantum computing. He
is a recipient of the 2020 ETAPS Doctoral Dissertation Award and the 2017 Google
PhD fellowship in programming languages.