ABSTRACT. This tutorial provides an introduction to CPAchecker, which is a flexible and configurable framework for software verification and testing. The framework provides many abstract domains, such as predicates, constant values, intervals, BDDs, and memory graphs, and many program-analysis and model-checking algorithms, such as symbolic execution, predicate abstraction, bounded model checking, k-induction, PDR, interpolation-based model checking, and IMPACT. The software system originates from Simon Fraser University, Universität Passau, and Ludwig-Maximilians-Universität München and received many contributions from other institutions, such as Universität Paderborn, Universität Oldenburg, Technische Universität Darmstadt, and ISP\,RAS. The development history spans 17 years and more than 120 developers worldwide have contributed to its success. This tutorial presents basic use cases for CPAchecker in formal software verification, explains the main verification techniques of CPAchecker with their strengths and weaknesses, and how to use CPAchecker for test-case generation and verification-result validation.

ABSTRACT. Great minds have long dreamed of creating machines that can reason deductively and automatically and can thereby function as general-purpose problem solvers. Satisfiability modulo theories (SMT) has emerged as one pragmatic realization of this dream, providing significant expressive power without giving up automation. This tutorial is a beginner's guide to the capabilities and uses of modern SMT solvers. It includes a basic overview of SMT and its formal foundations, a catalog of the main theories used in SMT solvers, and illustrations of how to use SMT solvers to obtain models and proofs. Throughout the tutorial, many examples and exercises are provided. These are designed to be hands-on activities for the reader. They can be run using either Python or the SMT-LIB language, using either the cvc5 or the Z3 SMT solvers.

ABSTRACT. Program generation is a powerful and expressive approach to eliminating abstraction overhead and improving program performance, which has been studied and implemented in a variety of languages with different forms. In this talk we overview MacoCaml, a new design and implementation of compile-time computation for OCaml. MacoCaml features a unifying and novel combination of phase separation and quotation-based staging. We review MacoCaml’s recent developments, including a comprehensive formalism of a feature- rich macro calculus with key meta-theoretic properties, and an extension to module functors that leads to explicit phase distinction. We describe how the meta-theoretical results offer practical benefits for programmers, and conclude the talk with a few directions for future exploration.

ABSTRACT. Stream-based runtime monitoring frameworks are safety assurance tools that check the runtime behavior of a system against a formal specification. This tutorial provides a hands-on introduction to RTLola, a real-time monitoring toolkit for cyber-physical systems and networks. RTLola processes, evaluates, and aggregates streams of input data, such as sensor readings, and provides a real-time analysis in the form of comprehensive statistics and logical assessments of the system's health. RTLola has been applied successfully in the monitoring of autonomous systems such as unmanned aircraft.

The tutorial guides the reader through the development of a stream-based specification for an autonomous drone observing other flying objects in its flight path. Each section of the tutorial provides both an intuitive introduction for RTLola novices, highlighting useful language features and specification patterns, and a more in-depth explanation of technical details for the advanced reader. Finally, we discuss how runtime monitors generated from RTLola specifications can be integrated into a variety of systems.

ABSTRACT. The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable, because one can prove one method at a time to be correct relative to its contract. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.

ABSTRACT. Software development for mission-critical applications requires a level of confidence that can be achieved through the use of formal methods. For a number of industrial applications, there is a lack of high-level properties to be verified, and proof mainly replaces unit testing. This talk presents an integrated approach based on more than 20 years of industrial practice, which enables so-called "system" properties to be modelled in a formal software model. The proof of the system's safety is not carried out entirely formally, but it is entirely guided by the model. It is based on 2 principles which are illustrated by means of a demonstrative example.