Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

### martes 3 de marzo de 2020

10:45am Meeting room 302 (Mountain View), level 3

**Isabel García***, PhD Student**, IMDEA Software Institute*

### Modular verification of C programs

#### Abstract:

To obtain scalability, software model checkers often employ modular analysis
techniques that analyze each of the procedures in a program separately. In this
context, summaries are used to abstract the behavior of procedures, as relations
of their input/output parameters, to analyze any procedure call without inlining
or analyzing its body. One key challenge when producing summaries of
memory-manipulating programs is to solve the frame problem: determining which
memory locations are not changed by a procedure.

In SMT-based model checking, the program heap is usually modeled by logical
(unbounded) arrays. A pointer analysis is typically used as a pre-analysis to
divide the heap into multiple disjoint regions, such that each region is encoded
into an array. In general, a summary contains two arrays (input and output)
per memory region, describing all possible values before and after the call to
the procedure. A naive SMT encoding requires quantifiers to express which
elements of the output array are equal to the input array. Although some SMT
solvers can handle formulas with quantifiers, the problem is in general
undecidable and, therefore, we want to avoid them if possible.

In this talk we will show how to leverage a pointer analysis to produce an SMT
encoding that enforces the SMT solver to search only for quantifier-free
summaries. First, we use the explicit heap representation that the pointer
analysis produces to distinguish between finite and potentially infinite memory
regions accessed by a procedure. Second, we introduce a new SMT encoding that
replaces array variables with scalars if the procedure only uses a finite amount
of memory.

This is a joint work with Jorge Navas and Arie Gurfinkel.