Automated functional program verification using fixpoint fusion

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

• Will Sonnex, Université de Cambridge
• Friday 18 October 2013, 15:15-16:15
• Room GC22, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room GC22, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.