Leon documentation¶
Contents:
- Introduction
- Getting Started
- Installing Leon
- Tutorial: Sorting
- Warm-up: Max
- Sorting Two Elements
- Interactive Exploration of Program Space
- Defining Lists and Their Properties
- Insertion into Sorted List
- Being Sorted is Not Enough
- Using Size in Specification
- Using Content in Specification
- Sorting Specification and Running It
- Synthesizing Sort
- Going back and Synthesizing Insertion
- Repairing an Incorrect Function
- Pure Scala
- Leon Library
- XLang
- Verification
- Resource Verification
- Why Verify Resource Bounds?
- Proving Abstract Bounds on Resources
- Importing Inferred Bounds
- Finding Counter-examples for Concrete Bounds
- Using Correctness Properties to Establish Bounds
- Resources Supported
- Dependency on Termination
- Running from Command Line
- Common Pitfalls
- Support for Higher-order Functions and Memoization
- Limitations
- References
- Contributors
- Proving Theorems
- Isabelle
- Limitations of Verification
- Synthesis
- Repair
- Safe C Code
- Command Line Options
- Frequently Asked Questions
- References