Zeno: An automated theorem prover for functional programs

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

• Will Sonnex (University of Cambridge)
• Tuesday 11 October 2011, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact William Denman.

Zeno is a new tool for verifying simple properties of Haskell programs through induction and other techniques, which outputs completed proofs to Isabelle. In a comparison with the rippling based tool IsaPlanner and the industrial strength tool ACL2s, using a test suite from the IsaPlanner website, we found that Zeno could prove, in a timely manner, strictly more properties than either. In this talk I will run through an example proof in Zeno and discuss the heuristics we apply to select proof steps and control the search space, along with an interactive demo. You can try our tool out online at http://tryzeno.org

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.