SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Mon 5 Dec 2022 11:00 - 11:30 at AMRF Auditorium - Model Checking and Verification Chair(s): Arlen Cox

Modularity is indispensable for scaling automatic verification to large programs. However, modularity also introduces challenges because it requires inferring and abstracting the behavior of functions as summaries – formulas that relate the function’s inputs and outputs. For programs manipulating memory, summaries must include the function’s frame, i.e., how the content memory is affected by the execution of the function. Since memory is often modeled with (unbounded) logical arrays, expressing frames generally requires universally quantified formulas. Such formulas significantly complicate inference and subsequent reasoning and are thus to be avoided. In this paper, we present a technique to encode the memory that is bounded explicitly, eliminating the need for quantified summaries. We build on the insight that the size of frames can be statically known. This enables replacing unbounded arrays with finite maps – a finite collection of key-value pairs. Specifically, we develop a new static analysis to infer the finite parts of a function’s frame. We then extend the theory of arrays to the theory of finite maps and show that satisfiability of Constrained Horn Clauses (CHCs) over finite maps is reducible to satisfiability of CHCs over the base theory. Finally, we propose a new encoding from imperative programs to CHCs that uses finite maps to model explicitly the finite memory passed in function calls. The result is a new verification strategy that preserves the advantages of modularity while reducing the need for quantified frames. We have implemented this approach in SeaHorn, a state-of-the-art CHC-based software model checker for LLVM. An evaluation on Linux Drivers from SV-COMP shows the effectiveness of our technique.

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Model Checking and VerificationSAS at AMRF Auditorium
Chair(s): Arlen Cox IDA
10:30
30m
Talk
Parameterized Recursive Refinement Types for Automated Program Verification
SAS
Ryoya Mukai The University of Tokyo, Naoki Kobayashi University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan
11:00
30m
Talk
Efficient Modular SMT-Based Model Checking of Pointer ProgramsVirtual
SAS
Isabel Garcia-Contreras University of Waterloo, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, inc.
11:30
30m
Talk
Case Study on Verification-Witness Validators: Where We Are and Where We Go
SAS
Dirk Beyer LMU Munich, Jan Strejcek Masaryk University
Link to publication DOI Media Attached