Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 11:30 - 12:00 at Sala III - Decision Procedures Chair(s): Kedar Namjoshi

We present Dryad_dec, a decidable logic that allows reasoning about tree data-structures with measurements. This logic supports user-defined recursive measure functions based on Max or Sum, and recursive predicates based on these measure functions, such as AVL trees or red-black trees. We prove that the logic’s satisfiability is decidable. The crux of the decidability proof is a small model property which allows us to reduce the satisfiability of Dryad_dec to quantifier-free linear arithmetic theory which can be solved efficiently using SMT solvers. We also show that Dryad_dec can encode a variety of verification and synthesis problems, including natural proof verification conditions for functional correctness of recursive tree-manipulating programs, legality conditions for fusing tree traversals, synthesis conditions for conditional linear-integer arithmetic functions. We developed the decision procedure and successfully solved 220+ Dryad_dec formulae raised from these application scenarios, including verifying functional correctness of programs manipulating AVL trees, red-black trees and treaps, checking the fusibility of height-based mutually recursive tree traversals, and counterexample-guided synthesis from linear integer arithmetic specifications. To our knowledge, Dryad_dec is the first decidable logic that can solve such a wide variety of problems requiring flexible combination of measure-related, data-related and shape-related properties for trees.

slides (vmcai.ppsx)2.78MiB

Mon 14 Jan

VMCAI-2019
11:00 - 12:30: VMCAI 2019 - Decision Procedures at Sala III
Chair(s): Kedar NamjoshiBell Labs, Nokia
VMCAI-201911:00 - 11:30
Talk
Jochen HoenickeUniversität Freiburg, Tanja SchindlerUniversity of Freiburg
VMCAI-201911:30 - 12:00
Talk
Xiaokang QiuPurdue University, Yanjun WangPurdue University
File Attached
VMCAI-201912:00 - 12:30
Talk
Charlie MurphyPrinceton University, Zachary KincaidPrinceton University
File Attached