Lectures

See the schedule here

Day 1: SAT Solving

Daniel Leberre

Abstract TBA

Bio:Dr. Leberre is professor in Lens, where he works on SAT solving and beyond with the SAT4j SAT solver in Java.

Kristin Yvonne Rozier

Abstract TBA

Bio:Dr. Rozier is working in Iowa State University. She works on various formal tools like MLTL that is used by the NASA Lunar Gateway Vehicle System Manager.

Katalin Fazekas

Abstract TBA

Bio:Dr. Fazekas is doing research at the TU Wien, after doing her PhD in Linz and doing a Research Fellow at the Simons Instute. One of her topics of research are deeper integration of SMT and SAT solving by providing external control.

Armin Biere

Abstract TBA

Bio:Prof. Dr. Armin Biere is now in Freiburg after spending many years in Linz. He is very famous for his work on SAT solvers. As Karem Sakallah mentioned in a talk: The SAT Competition is a simple game. Many people submit a solver and at the end, Armin wins. He is also very active on Twitter, Mastodon, and various other social networks.

Day 2: SMT Solving

Haniel Barbosa

Abstract Satisfiability Modulo Theories (SMT) is the problem of determining the satisfiability of a first-order formula in a logical theory of interest. Typical theories include various forms of arithmetic and of various data types such as arrays, bit-vectors, strings, and so on. SMT solvers are highly efficient and versatile systems specialized for this problem, widely used as backend engines in many application domains. However, when an application does not entirely fit the predefined theories, quantifiers may be used to provide new axioms to complement them. SMT solvers generally rely on various instantiation techniques to handle quantifiers, increasingly reducing quantified problems to ground ones so that the efficient theory procedures can be leveraged. This lecture will cover the state of the art in instantiation techniques in SMT solving, detailing and motivating different techniques and showing how they complement each other.

Bio:Prof. Barbosa is one of the main developers of SMT solvers: during his PhD he worked on veriT in Nancy, during his postdoc in Iowa on CVC4, and now he works on cvc5, the successor of CVC4 (except for the writing of the solver name).

Alberto Griggio

Abstract TBA

SummaryThis lecture gives an overview of the most used techniques for quantifier-free SMT solving, focusing on the CDCL(T) architecture and some important theory solvers.

Bio:Prof. Griggio is one of the developers of the SMT solver MathSAT, but is also involved in projects beyond SMT like the model checker nuXmv.

Philipp Rümmer

Abstract TBA

Summary

Bio:Prof. Rümmer from the University of Regensburg is not one the main contributors for support of strings within SMT solvers, but he also works on many applications.

Michael (Mike) Whalen

Abstract TBA

Summary

Bio:He is working in of the big companies that uses SMT solver, although you might not expect: Amazon ("one billion SMT queries a day"). He works on SAT and SMT solving.

Automated Reasoning and Using Proofs

Michael Rawson

Abstract TBA

Summary An taste of theorem proving: what it is (not). First-order theorem proving. Challenges and approaches. The popular saturation paradigm. An outline of the superposition calculus. A sketch of Vampire.

Bio:Dr. Rawson is one of the Vampire maintainers, so he moved from Manchester to work in Vienna now. When he is not attacking other solvers at yearly CASC competitions, he works on adding ML to automated reasoning.

André Platzer

Title Logic of Autonomous Dynamical Systems

Abstract This course highlights some of the most fascinating aspects of the logic of dynamical systems which constitute the foundation for developing cyber-physical systems (CPS) such as robots, cars and aircraft with the mathematical rigor that their safety-critical nature demands. Differential dynamic logic (dL) provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. In dL, properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics. In addition to providing a strong theoretical foundation for CPS, differential dynamic logics as implemented in the KeYmaera X prover have been instrumental in verifying many applications, including the Federal Aviation Administration's Airborne Collision Avoidance System ACAS X, a train control system for the Federal Railroad Administration, automotive systems, mobile robot navigation, and a surgical robotic system for skull-base surgery. dL is the foundation to provable safety transfer from models to CPS implementations and is also the key ingredient behind autonomous dynamical systems for Safe AI in CPS. References: André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. DOI:10.1007/978-3-319-63588-0 André Platzer. Logics of dynamical systems. LICS, 2012: 13-24. DOI:10.1109/LICS.2012.13

Bio:Prof. Dr. Platzer works at the KIT in Karlsruhe, where he is the Alexander von Humboldt Professor for cyber-physical systems, after being in Carnegie Mellon University for several years.

Stephan Schulz

Abstract TBA

Bio:Prof. Dr. Schulz is a professor in Stuttgart. He is very famous for his E prover, where each version is named after some tea.

Chantal Keller

TitleProof checking in a verified way

Abstract TBA

Summary In a first part, I will present proof checking of automated solvers inside proof assistants: interest, history, approaches, results, ... The second part will be an interactive tutorial focusing on reusing SMTCoq's certified proof checker for checking one's proofs

Bio:Dr. Keller is Associate Professor in Paris (Université Paris-Saclay), where she works on various formalization in Coq or tools like SMTCoq that replays proof of SMT solvers in Coq to make sure that the proofs are correct.

Day 4: Applications and Usage

Carsten Fuhs

Abstract TBA

Bio:He is a senior lecturers in London, where he works a term rewriting including higher order, sometimes creating benchmarks for SAT/SMT/AR.

Jakob Nordström

Abstract TBA

Bio:Sitting between Lund and Copenhagen, he is interested in proof complexity and he is one of the authors of the veriPB proof format, one of the few formats accepted at the SAT Competition.