Precise reasoning with structured time, structured heaps, and collective operations

Despite decades of progress, static analysis tools still have great difficulty dealing with programs that combine arithmetic, loops, dynamic memory allocation, and linked data structures. In this p...