POPEYE: Specification Synthesis from Tests

Introduction

POPEYE is a tool that automatically infers useful invariants/specifications for (higher-order) programs. POPEYE finds invariants/specifications from program samples and represents invariants/specifications into refinement types.

POPEYE is not dedicated to higher-order functional programs. It can infer and verify useful properties for array programs (with side-effects).

A recent extension of POPEYE is able to prove the safety properties of over 200 loop programs and a suite of recursive programs (collected from relate tools), using numeric invariants.

Another extension of POPEYE, which we call DOrder, can automatically infer expressive and useful shape specifications for functional data structures (e.g. AVL tree or Redblack tree) beyond the scope of competing tools. For example, it can infer and verify that a transform function which encodes an input tree to an output list preserves the in-order relation of the tree in the forward-order relation of the list.

POPEYE is still under very active development. Our next effort is to enable POPEYE to verify imperative heap-manipulating program using Separation Logic.


The source code and benchmarks of POPEYE is available from github.


zhu103 At my university