Tutorials and Keynotes

Tutorials

Tutorials took place on September 21, 2020.

Alexander Nadel, Intel

Anytime Algorithms for MaxSAT and Beyond slides | video

Abstract Given a propositional formula F in Conjunctive Normal Form (CNF), a SAT solver decides whether it is satisfiable or not. It is often required to find a solution to a satisfiable CNF formula F, which optimizes a given Pseudo-Boolean objective function Ψ, that is, to extend SAT to optimization.

MaxSAT is a widely used extension of SAT to optimization. A MaxSAT solver can be applied to optimize a Pseudo-Boolean objective function Ψ, given a CNF formula F, whenever Ψ is a linear function.

MaxSAT has a diverse plethora of applications, including applications in computer-aided design, artificial intelligence, planning, scheduling and bioinformatics. A variety of approaches to MaxSAT have been developed over the last two decades. In this tutorial, we focus on anytime MaxSAT algorithms, where an anytime algorithm is expected to find better and better solutions,the longer it keeps running. The anytime property is crucial in industrial applications, since it allows the user to: 1) get an approximate solution even for very difficult instances, and 2) trade quality for performance by regulating the timeout.

Anytime MaxSAT solvers have been evaluated at yearly MaxSAT Evaluations since 2011 in the so-called incomplete tracks. We trace the evolvement of anytime MaxSAT algorithms over the last decade and lay out the algorithms, applied by the winners of MaxSAT Evaluation 2020.

Furthermore, we touch upon anytime algorithms for optimization problems beyond MaxSAT, such as bit-vector optimization and the problem of optimizing an arbitrary not-necessarily-linear function, given a CNF formula. Finally, we discuss challenges and future work.

Hillel Kugler, Bar-Ilan University

Formal Verification for Natural and Engineered Biological Systems slides | video

Abstract Computational modeling is now used effectively to complement experimental work in biology, allowing to identify gaps in the understanding of the biological systems studied, and to predict system behavior based on a mechanistic models. We provide an overview of several areas in biology for which formal verification has been successfully used to advance the state-of-the-art in biological modeling, highlighting examples from both natural and engineered biological systems. In natural biological systems the main goal is to understand how a system works and predict its behavior, whereas for engineered biological systems the main goal is to engineer biological systems for new purposes, e.g. for building biology-based computational devices. We compare between the challenges in applying formal verification in biology and the application to traditional hardware and software domains and outline future research directions and opportunities for formal verification experts to contribute to the field.

Armin Biere, Johannes Kepler Universität

Tutorial on Word-Level Model Checking slides | video

Abstract In SMT bit-vectors and thus word-level reasoning is common and widely used in industry. However, it took until 2019 that the hardware model checking competition used word-level benchmarks. Reasoning on the word-level opens up many possibilities for simplification and more powerful reasoning. In SMT we do see advantages due to operating on the word-level, even though, ultimately, bit-blasting and thus transforming the word-level problem into SAT is still the dominant and most important technique. For word-level model checking the situation is different. As the hardware model checking competition in 2019 has shown bit-level solvers are far superior (after bit-blasting the model through an SMT solver though). On the other hand word-level model checking shines for problems with memory modeled with arrays. In this tutorial we revisit the problem of word level model checking, also from a theoretical perspective, then give and overview on classical and more recent approaches for word-level model checking and then discuss challenges and future work.

Keynotes

Peter Schrammel, University of Sussex and Diffblue Ltd.

How testable is business software? slides | video

Abstract Most businesses rely on a significant stack of software to perform their daily operations. This software is business-critical as defects in this software have major impacts on revenue and customer satisfaction. The primary means for verification of this software is testing. We conducted a large-scale analysis of Java software packages to evaluate their testability. The results show that code in software repositories is typically split into portions of very trivial code, non-trivial code that is unit-testable, and code that cannot be unit-tested easily. This brings up interesting considerations regarding the use of test coverage metrics and design for testability, which is crucial for testing efficiency and effectiveness, but unfortunately too often an afterthought. Lack of testability is an obstacle to applying tools that perform automated verification and test generation. These tools cannot make up for poor testability of the code and have a hard time in succeeding or are not even applicable without first improving the design of the software system.

Orna Kupferman, Hebrew University of Jerusalem

From Correctness to High Quality slides | video

In the synthesis problem, we are given a specification Ψ over input and output signals, and we synthesize a system that realizes Ψ : with every sequence of input signals, the system associates a sequence of output signals so that the generated computation satisfies Ψ . The above classical formulation of the problem is Boolean. The talk surveys recent efforts to automatically synthesize reactive systems that are not only correct, but also of high quality. Indeed, designers would be willing to give up manual design only after being convinced that the automatic procedure that replaces it generates systems of comparable quality.

We distinguish between behavioral quality, which refers to the way the specification is satisfied, and costs, which refer to resources that the system consumes. For the first, we focus on the temporal logics LTL[F] and LTL[D], which extend LTL by quality operators. The satisfaction value of LTL[F] and LTL[D] formulas is a real value in [0; 1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. Essentially, LTL[F] contains propositional quality operators, like weighted-average, and LTL[D] contains discounted eventuality operators. Using LTL[F] and LTL[D], a designer can prioritize different ways to satisfy the specification and formally weight parameters such as security, maintainability, runtime, delays, and more. For the second, we distinguish between four classes of costs, induced by the following two characteristics: (1) construction vs. activity costs, and (2) physical vs. monetary costs. For example, the sensing cost of a system is physical, and we distinguish between the number of sensors in the system (construction cost) and the sensing required during its operation (activity cost).