Model Counting for Complex Data Structures

FILIERI, ANTONIO; FRIAS, MARCELO FABIAN; PASAREANU, CORINA; VISSER, WILLEM

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: ISBN 978-3-319-23403-8; Año: 2015 p. 222 - 241

0302-9743

We extend recent approaches for calculating the probability of pro- gram behaviors, to allow model counting for complex data structures with nu- meric fields. We use symbolic execution with lazy initialization to compute the input structures leading to the occurrence of a target event, while keeping a sym- bolic representation of the constraints on the numeric data. Off-the-shelf model counting tools are used to count the solutions for numerical constraints and field bounds encoding data structure invariants are used to reduce the search space. The technique is implemented in the Symbolic PathFinder tool and evaluated on several complex data structures. Results show that the technique is much faster than an enumeration-based method that uses the Korat tool and also highlight the benefits of using the field bounds to speed up the analysis.