Laura Kovács (Vienna University of Technology)

First-order theorem proving and Vampire (slides)

ABSTRACT:

First-order theorem proving is undergoing a rapid development thanks to its successful use in program analysis and verification, security analysis, symbolic computation, theorem proving in mathematics, and other related areas. Breakthrough results in all areas of theorem proving have been obtained, including improvements in theory, implementation, and the development of powerful theorem proving tools. However, recent developments are not always easily accessible to non-specialists. This tutorial aims to address this by introducing the audience to first-order theorem proving. The workhorse used for a demonstration of concepts discussed at the tutorial will be our award-winning theorem prover Vampire.

The tutorial will be split in two lectures. The first lecture immediately helps the audience place the work in context by introducing them to an application of theorem proving in Vampire for validating mathematical theorems. The second lectures focuses on the core concepts of automating first-order theorem proving in first-order logic with equality. We will discuss the resolution and superposition calculus, introduce the saturation principle, present various algorithms implementing redundancy elimination, and demonstrate how these concepts are implemented in Vampire.

Sidney de Carvalho Nogueira (Universidade Federal Rural de Pernambuco, Brazil)

An introduction to CSP (slides)

ABSTRACT:

This tutorial overviews the notation of the CSP formal method, its semantics, and sample applications. We use the machine-readable version of CSP (CSPM) and the FDR tool through this tutorial.

CSP (Communicating Sequential Processes) is a process algebra mainly used to model and verify the behavior of concurrent systems. Systems are modeled as processes synchronizing and exchanging data through communication channels. Besides the modeling capabilities, CSP has a set of semantic models that allow one to check refinement between processes and reason about safety and liveness properties. In this tutorial, we use the CSPM notation to illustrate how to model and verify sample systems using the Failures-Divergence Refinement (FDR) tool, one of the main tools for CSP. Such a tool is very efficient in automatically checking whether a CSP process refines another CSP process and verifying properties such as deadlock and livelock freedom of systems specified in CSP. We illustrate the usage of the main concepts of this tutorial using practical examples.