In this course, we will focus on sequential and parallel SAT solving techniques. We will first describe the main components of Conflict Driven Clause Learning (CDCL) architecture used in most SAT solvers (conflict analysis, restarts, heuristics...). After that, we will present different approaches used to solve SAT in a parallel environment with a special attention to shared clauses. Finally, we will focus on SAT encoding and on incremental SAT solving where the SAT solver is used as an oracle to solve computationally more challenging problems. This course will also contain practical sessions.

Fault-tolerant distributed systems have been widely used and studied for the past 25 years. Solutions for agreement like problems, e.g., consensus, state machine replication, are developed and deployed over large networks by commercial products, e.g., Apache Zookeeper, Cassandra. However, the automated verification techniques have received much less attention in the academic or industrial community.

In this lecture we will identify the new challenges posed by fault-tolerance to automated techniques and we will discuss some of the existing solutions. The lecture will mainly focus on verification techniques designed for distributed protocols, with few pointers to extensions of these techniques to large scale implementations of these protocols.

The lecture focuses of verification techniques for consensus and replicated state machine. The lecture presents a formalization of communication-closure, a property of distributed systems that facilitates formal reasoning. We define a semantic reduction of the execution space, based on communication-closure, that preserves an important class of properties, including consensus. Concretely, the reduction shows that an asynchronous set of executions is equivalent to a synchronous set of executions. Verification techniques based on SMT-solvers are applied only to synchronous executions, which have much simple proof arguments.

Theories of linear arithmetic over R, Q, Z, and N are at the core of computational logic. Arising as generalizations of their existential conjunctive fragments, linear programming and integer programming, they occur in many contexts in computer science both in theory and practice. Reducing domain-specific constraints to a linear arithmetic theory is a standard and powerful problem-solving technique. Arithmetic theories are a fascinating object to study, as they lie at the interface of geometry, algorithmics, and logic.

This course gives an introduction to logical theories of linear arithmetic and their applications, such as the first-order linear theory of the reals and Presburger arithmetic, its analogue over the natural numbers. In the first part of the course, we will explore the theory behind linear arithmetic theories and mainly focus on paradigms for deciding such theories based on quantifier elimination, finite-state automata, generating sets and generating functions. In the second part of the course we will look at concrete applications of linear arithmetic theories in software verification, e.g., for finding bugs in concurrent programs and other infinite-state systems.

We are very happy that Leslie Lamport, Turing Award 2013, will be present for a discussion at VTSA 2021. We ask every applicant to watch his talk "If you're Not Writing a Program Don't Use a Programming Language" and think about one question that he/she would like to ask during this discussion with Leslie Lamport. Please provide this question in your application letter.

Fault-tolerant distributed consensus has been a central problem in the study of the principles of distributed computing for over forty years: each component in an unreliable distributed system has an input value and the component should eventually agree to output the same value, selected from the inputs. As individual components may fail, devising correct solutions is hard, error-prone, and for many systems impossible.

Due to the considerable cost of consensus solutions, the classic application domains were typically limited to safety critical systems, where for instance, out of four components at most one is assumed to fail and the others should maintain operational and in agreement. Recently we observed a renaissance of consensus in the scope of blockchains: For instance, Tendermint/Cosmos is a modern implementation that uses consensus for state machine replication, and scales to hundreds of components in adversarial environments.

I will discuss how distributed systems are modeled, I will show classical definitions of consensus and related problems, and describe solutions to the problems, and how one proves them correct by hand.

Understanding the intricacies of these issues is crucial for computer-aided verification of consensus algorithms and implementations, which is a flourishing research line these days. I will present some methods for the verification of abstract algorithms based on the threshold automata framework.