Leon
From MaRDI portal
Cited in
(19)- Reasoning about algebraic data types with abstractions
- OptiML
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- Datatypes with shared selectors
- Loop verification with invariants and contracts
- GNATprove
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Model finding for recursive functions in SMT
- Translating Scala programs to Isabelle/HOL. System description
- TreatJS
- RADA
- Synthesis of recursive ADT transformations from reusable templates
- Guardol
- TRANSIT
- Reasoning with finite sets and cardinality constraints in SMT
- Verifying and synthesizing software with recursive functions (invited contribution)
- LMS-Verify: abstraction without regret for verified systems programming
- HolBA
- Theory exploration powered by deductive synthesis
This page was built for software: Leon
