POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Tue 16 Jan 2024 11:40 - 12:00 at Marconi Room - Session 6: Abstract Interpretation Chair(s): Xavier Rival

In a seminal work, Miné studied an abstract backward semantic for inferring sufficient program pre-conditions. This analysis exploits under-approximated domain operators, demonstrated by Miné for the polyhedra domain, to under-approximate Dijkstra’s liberal pre-condition. The results of the analysis, were implemented into a static analysis tool for a toy language. In this paper we address some limitations that hinder its applicability to C-like programs. In particular, we focus on two improvements: handling of user input and integer wrapping. For this, we extend the semantic and design sound and effective abstractions. Furthermore, to improve the precision, we explore an under-approximated version of the powerset construction. This in particular helps handling arbitrary union that are difficult to implement with under-approximated domains. The improved analysis is implemented and its performance is compared with other static analysis tools in SV-COMP23 using a selected subset of benchmarks.

Tue 16 Jan

Displayed time zone: London change

11:00 - 12:30
Session 6: Abstract InterpretationVMCAI at Marconi Room
Chair(s): Xavier Rival Inria; ENS; CNRS; PSL University
11:00
20m
Talk
Formal Runtime Error Detection During Development in the Automotive Industry
VMCAI
Jesko Hecking-Harbusch Bosch Research, Jochen Quante Bosch Research, Maximilian Schlund Bosch Research
Pre-print
11:20
20m
Talk
Abstract Interpretation-Based Feature Importance for Support Vector Machines
VMCAI
Abhinandan Pal University of Birmingham, Francesco Ranzato University of Padova, Caterina Urban Inria & École Normale Supérieure | Université PSL, Marco Zanella University of Padova, Italy
11:40
20m
Talk
Generation of Violation Witnesses by Under-Approximating Abstract Interpretation
VMCAI
Marco Milanese Sorbonne University, Antoine Miné Sorbonne Université
DOI Pre-print
12:00
20m
Talk
Correctness Witness Validation by Abstract Interpretation
VMCAI
Simmo Saan University of Tartu, Estonia, Michael Schwarz Technische Universität München, Julian Erhard Technical University of Munich, Helmut Seidl Technische Universität München, Sarah Tilscher Technische Universität München, Vesal Vojdani University of Tartu
DOI Pre-print