Synthesis of ranking functions using extremal counterexamples
We present a complete method for synthesizing lexicographic linear ranking functions (and thus proving termination), supported by inductive invariants, in the case where the transition relation of the program includes disjunctions and existentials (large block encoding of control flow).
Previous work would either synthesize a ranking function at every basic block head, not just loop headers, which reduces the scope of programs that may be proved to be terminating, or expand large block transitions including tests into (exponentially many) elementary transitions, prior to computing the ranking function, resulting in a very large global constraint system. In contrast, our algorithm incrementally refines a global linear constraint system according to extremal counterexamples: only constraints that exclude spurious solutions are included.
Experiments show marked performance and scalability improvements compared to other systems.
Wed 17 Jun
|16:00 - 16:25|
Nuno MachadoINESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Brandon LuciaCarnegie Mellon University, Luís RodriguesUniversidade de Lisboa, Instituto Superior Técnico, INESC-IDMedia Attached
|16:25 - 16:50|
Venkatesh SrinivasanUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.Media Attached
|16:50 - 17:15|
Laure GonnordUniversity of Lyon & LIP, France, David MonniauxCNRS, VERIMAG, Gabriel RadanneUniversité Denis Diderot Paris 7, PPSMedia Attached
|17:15 - 17:40|