Advances in Verification

A post conference workshop of FSTTCS 2020.
Date: December 18, 2020

The subject of verification is well studied and has been successfully deployed in practice. As a result, several fundamental techniques have evolved over the years. This workshop aims to discuss some of the classical concepts in verification, with a focus on recent advances.


Title: Stateless Model Checking under the Release-Acquire Semantics

Speaker: Parosh Aziz Abdulla

Abstract: Program verification methodologies need to consider new challenges for which we currently lack solutions. The principal reason is that such methods are often conducted under the fundamental assumption of strong (or sequential) consistency (SC) where all components are strongly synchronized so that they all have a uniform view of the global state of the system. However, nowadays, most parallel software runs on platforms that do not guarantee SC. More precisely, to satisfy demands on efficiency and energy saving, such platforms implement optimizations that lead to the relaxation of the inter-component synchronization, hence offering only weak consistency guarantees. Weakly consistent platforms are found at all levels of system design, e.g., multiprocessor architectures, Cache protocols, Language level concurrency, and distributed data stores.

To illustrate the types of challenges that may arise, and the solutions that we can provide, I will consider the Release-Acquire (RA) fragment of the C11 language. RA is a useful and well-behaved fragment of the C11 memory model, which strikes a good balance between performance and programmability. In RA, all writes are release accesses, while all reads are acquire accesses. I will explain how classical stateless model checking algorithms, based on partial order reductions, that have been developed to work under the SC semantics can be adapted so that they can be applied to a concurrent program running under the RA semantics.

The lecture will present the ideas at a high level so that it can be followed by non-experts.

Title: Introduction to Monitorability

Speaker: Karoliina Lehtinen

Abstract: The idea of runtime monitoring is to observe the executions of a system in order to derive information on its correctness. By analysing executions rather than the system itself, it avoids the state-explosion problem associated with exhaustive verification techniques such as model-checking. The cost of lower complexity is limited expressivity: while model-checking will always provide a definite answer to the question “does the system satisfy the specification”, runtime verification provides no such firm guarantees. However, depending on the specification, runtime monitoring can provide a range of weaker guarantees. The study of monitorability seeks to understand the trade-offs between the complexity of specifications and guarantees given by runtime monitoring.

This tutorial provides a gentle introduction to monitorability, mostly from a formal language perspective. The aim is to understand what "Is this property monitorable?" might mean, and how parameters such as computational resources, the domain and prior knowledge might affect the answer.

Title: Automata Learning; Recent applications and advances

Speaker: Joshua Moerman

Abstract: Automata Learning is a successful technique to automatically infer a state machine from a system. The inferred model can be used for analysis, such as model checking or equivalence checking. This enables researchers and engineers to analyse black box systems. After I discuss the basic algorithms, I will give an overview of recent applications. These applications show the succes but also the troubles of applying automata learning in industrial case studies. Based on these applications, learning algorithms have been improved and extended to cope with time, data, and other additional structures. So I will survey some of these extensions as well.

Title: Parallel and Symbolic Algorithms for Model Checking

Speaker: Jaco van de Pol

Abstract: Model checking is a successful method for checking properties of concurrent, reactive systems. Since it is based on exhaustive search, scaling the method to industrial systems has been a challenge since its conception. Research has focused on clever data structures and algorithms to reduce the size of the state space and its representation; on smart search heuristics to reveal potential bugs and counterexamples early; and on high-performance computing to deploy the brute force processing power of clusters of compute-servers. The main challenge is to combine a brute force approach with clever algorithms: brute force alone (when implemented carefully) can bring a linear speedup in the number of processors. This is great, since it reduces model-checking times from days to minutes. On the other hand, proper algorithms and data structures can lead to exponential gains. Therefore, the parallelization bonus is only real if we manage to speedup the clever algorithms. This talk will provide an overview of some solutions that we have adopted in the high-performance model checker LTSmin. After introducing the basic model checking algorithm, a number of extensions will be discussed, based on parallel graph algorithms and parallel symbolic algorithms. We will also point out some of the obstacles for achieving the ideal speedup, and how we tried to overcome them.


Speaker IST CET Chair
Parosh Aziz Abdulla 13:30 - 14:30 9:00 - 10:00 K Narayan Kumar
Break 14:30 - 15:00 10:00 - 10:30
Karoliina Lehtinen 15:00 - 16:00 10:30 - 11:30 R Ramanujam
Long Break 16:00 - 17:30 11:30 - 13:00
Joshua Moerman 17:30 - 18:30 13:00 - 14:00 Madhavan Mukund
Break 18:30 - 19:00 14:00 - 14:30
Jaco van de Pol 19:00 - 20:00 14:30 - 15:30 Deepak D'Souza




B Srivathsan

Chennai Mathematical Institute

Prakash Saivasan

Institute of Mathematical Sciences