Title: Speeding Up Symbolic Execution Using Tight Field Bounds
Speaker: Nicolas Rosner, Assistant Professor, Buenos Aires Institute of Technology (ITBA) and Assistant Researcher at Argentina’s National Scientific Research Council (CONICET)
Date: Tuesday, May 3, 2016
Time: 1:00pm
Location: NIA, Room 101
Sponsor: Cesar Munoz, NASA/LaRC
Host: Mariano Moscato, NIA
Abstract: Lazy Initialization (LI) allows symbolic execution to effectively deal with nonprimitive inputs, such as heap-allocated data structures, thanks to a significant reduction in spurious and redundant symbolic structures.
In this talk we first describe Bounded Lazy Initialization (BLI), which improves on LI by taking advantage of precomputed relational bounds on the interpretation of class fields (as inferred from the class invariant) in order to reduce the number of spurious structures even further.
We then present BLISS, a technique that refines the search for valid structures during the symbolic execution process. BLISS builds upon BLI, extending it with field bound refinement and satisfiability checks. Field bounds are refined while a symbolic structure is concretized, avoiding cases that, due to the concrete part of the heap and the field bounds, can be deemed redundant. BLISS reduces the time required by LI by up to 4 orders of magnitude for the most complex data structures. Moreover, BLISS reduces the number of partially symbolic structures obtained by exploring program paths by over 50%, with reductions of over 90% in some cases.
Finally, we present DSPF, a distributed version of the BLISS technique that exploits tight field bounds as the basis for a problem splitting scheme. We show promising results using our distributed prototype, based on MPI and Symbolic PathFinder.
Bio: Nicolás Rosner is Assistant Professor at the Buenos Aires Institute of Technology (ITBA) and Assistant Researcher at Argentina’s National Scientific Research Council (CONICET). He completed his PhD in Computer Science at the University of Buenos Aires (UBA) in 2015.
Dr. Rosner’s research interests focus on lightweight formal methods for verification and testing of software artifacts. Most of his recent work is centered on bounded exhaustive analysis techniques for automated verification of properties over declarative models, verification of Java code with declarative contracts, and test suite generation. He is also interested in devising problem partitioning schemes in order to leverage commodity hardware (e.g., idle labs and clusters) towards improving the scalability of those techniques.