![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Tuesday 11 October 2011, 13:00-14:00
Zeno: An automated theorem prover for functional programs
- đ¤ Speaker: Will Sonnex (University of Cambridge)
- đ Date & Time: Tuesday 11 October 2011, 13:00 - 14:00
- đ Venue: Computer Laboratory, William Gates Building, Room SS03
Abstract
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
Series This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- 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
- Martin's interesting talks
- School of Technology
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.