Generalized symbolic execution for model checking and testing

Sarfraz Khurshid, Corina S. Păsăreanu, Willem Visser
[ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 22 April 2021

Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Warsaw, Poland
Berlin, Heidelberg
Pages 553-568
Note(s): lazy initialization, Java PathFinder, Omega library, symbolic execution, separation logic
Papers: xie:popl:2005, engler:issta:2007, calcagno:popl:2009

Introduced the idea of lazy initialization to allow pointer-manipulating programs to be verified using symbolic execution without having to construct a data structure for the program to symbolically execute.

As the name suggests, instead of constructing an input data structure first and then symbolically executing the code, the data structure is constructed on demand: each dereference of an uninitialized pointer either constructs a fresh object or chooses one of the previously constructed objects that the pointer could potentially refer to.

This approach was used as the basis of xie:popl:2005 and engler:issta:2007 except that I think both of them just created a fresh object and did not consider previously initialized objects at the cost of ignoring possible structure sharing or cycles.

I think it is also similar to the biabduction technique used in calcagno:popl:2009 (again, with restrictions on sharing based on separation logic).

The implementation technique is also interesting: unlike most approaches (e.g., xie:popl:2005) that build the solver, etc into their tools, they use a preprocessor that replaces all concrete variables and operations with symbolic variables and operations. The only thing they need is a model checker capable of forking execution and backtracking.

Lazy initialization of symbolic values

  • Compositional shape analysis by means of bi-abduction [calcagno:popl:2009]
  • Under-constrained execution: Making automatic code destruction easy and scalable [engler:issta:2007]
  • Practical, low-effort equivalence verification of real code [ramos:cav:2011]
  • Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]
  • Scalable error detection using boolean satisfiability [xie:popl:2005]