University of Cambridge > Talks.cam > Computer Laboratory Programming Research Group Seminar > Automated functional program verification using fixpoint fusion

Automated functional program verification using fixpoint fusion

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Raphael Proust.

The current state of the art in functional program verification uses automated proof by induction to check properties. This approach is used in the well established ACL2 for Common LISP , and the more recent HipSpec for Haskell.

This talk describes an alternative approach where terms within properties are simplified until the property becomes trivially true. The simplification technique we use is called “fixpoint fusion”, but also goes by the names “deforestation” and “supercompilation”. We first present applications of this process which can verify properties at the same level as ACL2 or HipSpec. We then present an extension which allows for the fully automatic simplifications “isSorted (treesort xs) => True” and “isSorted (quicksort xs) => True”, both of which it is fundamentally impossible for ACL2 or HipSpec to solve without user provided lemmas.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity