In contrast with other technological areas, it is very difficult to make proof systems interoperate because proof systems are generally based on different and sometimes incompatible axioms or deduction rules. One promising way to enable interoperability whenever it is possible is by representing the axioms, deduction rules and proofs of the various systems in a logical framework so that a feature that is common to several systems is encoded in the same way.

In this lecture, I will present the logical framework called the λΠ-calculus modulo rewriting and its implementation in the tool Dedukti, and the tool Lambdapi which extends Dedukti with implicit arguments and tactics. I will show how to encode various logical or type systems in Dedukti, from first-order logic used in automated theorem provers, to higher-order logic used in proof assistants HOL, Isabelle or PVS, and to advanced type systems like the calculus of constructions with a linear infinite hierarchy of type universes used in the proof assistants Coq, Agda or Lean. For automated theorem provers, I will show how one can reconstruct proofs in Dedukti from TSTP files.

Slides: [Part 1] [Part 2]

Termination of a program means that regardless of the input to the program, its computations will always come to a halt. Although this property is undecidable, fully automated techniques and tools have flourished in recent years. This is witnessed also by the International Termination and Complexity Competition (termCOMP) as well as the Termination Category of the Competition on Software Verification (SV-COMP).

In the first part of this course, we will discuss approaches to automated termination analysis in several settings. On the one hand, we consider Term Rewrite Systems (TRSs) and Integer Transition Systems (ITSs), which have concise formal definitions and capture the core of many programming languages. On the other hand, we consider program analysis techniques for practically used programming languages such as Java or Haskell. These language-specific techniques extract TRSs or ITSs (or combinations thereof) whose termination (analysed separately) implies termination of the original program.

However, termination alone is not always enough. Complexity analysis is a refinement of termination analysis that has received a lot of attention in recent years. Here questions like "given a program P, how many steps does it take in the worst case to execute P on an input of size at most n?" are addressed. Corresponding program analysis tools have been developed and deployed for a variety of settings, including TRSs, ITSs, and real-world programming languages. To the above question, tools may provide answers such as "running P on an input of size at most n needs O(n^2) many steps". In the second part of the course, we will discuss a selection of techniques that are used by such tools for automated complexity analysis. As we shall see, a number of techniques from termination analysis can be revisited to yield powerful complexity analysis techniques.

[Course Materials]

This talk 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 Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, 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

Slides: [Part 1-2] [Part 3] [Part 4]

Over the last couple of years, a number of new SMT and constraint solvers have been proposed that can check satisfiability of quantifier-free formulas over a background theory of strings and string operations. String solvers can be applied in different verification algorithms, for instance in symbolic execution to check path feasibility, in software model checking to take care of implication checks; a prime application area is security analysis for languages like JavaScript and PHP, for instance to discover vulnerability to injection attacks.

After a general introduction to the field, this lecture will focus on methods for handling constraints with complex string operations. It will present decidability results and concrete algorithms for constraints including "real-world" regular expressions; matching, extraction, concatenation; different forms of replace and replace-all operations; encoders/decoders; string length, counting, and sub-string extraction. Along the way, the lecture will cover various flavours of finite-state automata that are useful to construct solvers.

[Course Materials]

Many application problems from artificial intelligence, verification, and formal synthesis can be efficiently encoded as quantified Boolean formulas (QBFs), the extension of propositional logic with quantifiers. This extension makes the QBF decision problem PSPACE-complete (in contrast to SAT which is NP-complete).

Over the last years much progress has been made concerning the theory and practice of QBF research. In this lecture, we review the state of the art of QBF technology and show how to perform automated reasoning with QBFs. This lecture will include practical exercises.

[Course Materials]