Two half-day tutorials are organized on Monday October 21.
Room: Inamori-Hall
Lunch is served for those registered.
Tutorial 1 – SMT Solving for Verification
Monday 21 October 2024, 9:30-10:45 & 11:15-12:30, Room: Inamori-Hall
Speaker: Haniel Barbosa, Universidade Federal de Minas Gerais
Abstract:
This tutorial aims to give participants an overview of SMT, describe the main features of the state-of-the-art SMT solver cvc5, and walk through in-depth examples using cvc5 to demonstrate how to solve real problems with an SMT solver. We will provide a detailed description of various aspects of cvc5’s internals, including its architecture, its capacity for dealing with quantifiers, and which feedback can it provide to users when the verification attempts are successful and when they are not. We will show examples of software and hardware verification problems, and how they are encoded and handled by these features in cvc5.
Participants are expected to have only a basic knowledge of what SMT is. This tutorial will give casual users a taste of encoding complex, real-world problems in SMT and effectively using cvc5 to solve them. Participants will be left with some knowledge of what goes on inside a versatile, industrial-strength SMT solver, and some of the practical issues that arise in using them.
cvc5 is jointly developed by Stanford University, the University of Iowa, Universidade Federal de Minas Gerais, and Bar-Ilan University, and is freely available for both research and commercial use under an open-source license.
Bio: Haniel Barbosa is a tenured assistant professor in the Department of Computer Science at Universidade Federal de Minas Gerais (UFMG), in Belo Horizonte, Brazil. He fell in love with automated reasoning and its applications during his PhD at Inria Nancy, under the direction of Prof. Pascal Fontaine, and subsequently as a postdoctoral researcher at the University of Iowa. His research focuses on improving satisfiability modulo theories (SMT) solvers for formal verification and on making them more trustworthy via the production and checking of proof certificates. He is also a senior technical lead for the state-of-the-art SMT solver cvc5.
Tutorial 2 – The VeriAbs Tool Suite for Code Verification
Monday 21 October 2024, 14:00-15:15 & 15:45-17:00, Room: Inamori-Hall
Speakers: Priyanka Darke and R Venkatesh, TCS Research
Abstract:
In large real-life programs, loops, and arrays are the main challenges to scaling up verification. Overcoming this challenge requires a portfolio of specialized techniques. Accordingly, we at TCS Research have developed a portfolio of loop and array abstraction techniques to scale up verification in practice. Naturally, a collection of such techniques can verify programs from a wide variety of classes that each individual technique cannot. This collection of techniques in addition to well-known verification techniques, like bounded model checking, form the portfolio used in the VeriAbs framework.
In order to improve the likelihood that a suitable technique from the portfolio is applied to the input program, the techniques are often prioritized into a sequence, also called a verification strategy, to verify each input program. VeriAbs uses five such strategies, each defined manually using domain expertise and experimentation. One of the suitable strategies is selected for verification based on the class of the input program. This approach to program verification has shown success and won several gold medals in the Competition on Software Verification (SV-COMP) from 2019-23.
In practice defining verification strategies manually is time consuming and not extensible. Towards this, machine learning methods have been proposed recently to predict strategies automatically for each input program. It is a challenge to define useful program features that can describe a program well enough to the learner to predict a useful strategy from the given portfolio of techniques. We present novel approaches to alleviate this challenge as implemented in VeriAbsL, a tool that uses machine learning methods to predict strategies for an input program using VeriAbs’s portfolio. VeriAbsL was developed in 2023, and since then has won a silver and a gold medal at SV-COMP from 2023-24.
To summarise, in this tutorial, we present (1) a few proprietary loops and array abstraction techniques in VeriAbs’s portfolio, (2) the manually defined method of strategy selection as implemented in VeriAbs, (3) the machine learning method to strategy prediction as implemented in VeriAbsL, (4) our application of these tools to industrial software that led to better results than other state of the art software verifiers, and (5) how to use VeriAbs and VeriAbsL.