• Stars
    star
    162
  • Rank 223,871 (Top 5 %)
  • Language
    Scala
  • License
    Other
  • Created over 11 years ago
  • Updated about 1 month ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

The Leon system for verification, synthesis, repair

Leon 3.0 Build Status

Getting Started

To build Leon you will need JDK, scala, sbt, and some external solver binaries. On Linux, it should already work out of the box.

To get started, see the documentation chapters, such as

For change log, see CHANGELOG.md

The Stainless/Inox Stack

Leon verification has recently been split off into

  • Inox a backend solving layer, and
  • Stainless a Scala frontend that supports contract-checking and termination proving.

Leon remains (for now) the main project for synthesis and repair as well as resource bounds inference. However, developpment of verification-related features will most likely be confined to the Stainless/Inox front.

More Repositories

1

stainless

Verification framework and tool for higher-order Scala programs
HTML
347
star
2

ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Scala
117
star
3

inox

Solver for higher-order functional programs
Scala
87
star
4

scallion

LL(1) parser combinators in Scala
Scala
54
star
5

smart

Verification and Generation of Smart Contracts using Stainless and Scala
HTML
35
star
6

treenet

Recursive Neural Networks for PyTorch
Python
31
star
7

lisa

Proof assistant based on first-order logic and set theory
Scala
29
star
8

bolts

Bolts: Stainless Verified Scala Examples
Scala
15
star
9

nugget

Neural-Network Guided Expression Transformation
Python
13
star
10

jahob

Jahob Verification System
C
11
star
11

comfusy

Implementation of the "Complete Functional Synthesis" approach described in the eponymous PLDI 2010 paper.
Scala
11
star
12

silex

Lexing library for Scala
Scala
10
star
13

welder

Interactive Theorem Proving based on Inox
Scala
10
star
14

SystemFR

System FR: Formalized Foundations for Stainless
Coq
9
star
15

scallion-proofs

Proofs of correctness for Scallion (https://github.com/epfl-lara/scallion)
Coq
9
star
16

rust-stainless

An experimental Rust frontend for Stainless
Rust
6
star
17

StainlessFit

Stainless directly built on System FR, with standalone front-end
Scala
5
star
18

verified-2048

A 2048 clone verified by Stainless
Scala
4
star
19

stainless-actors

Actor System library for Stainless which runs on Akka
Scala
4
star
20

asplos2022tutorial

ASPLOS 2022 Tutorial on Stainless
C
4
star
21

OCBSL

A minimal algorithm to decide the word problem in Orthocomplemented Bisemilattices, in Scala.
Scala
4
star
22

fit-code

TypeScript
3
star
23

verifythis2020

VerifyThis2020 Challenge in Stainless
Scala
2
star
24

silex-proofs

Proofs on lexing with derivatives and zippers
Coq
2
star
25

cs550

Scala
2
star
26

lattices-algorithms

This repository contains two algorithms for the word problem and normalization problem of Ortholattices and Orthocomplemented Bisemilattices
Scala
2
star
27

muscat

A unit testing framework for concurrent Scala programs
Scala
2
star
28

grammar-web

An online tutoring system for context-free grammars
Scala
2
star
29

compiler2024-labs-public

Scala
2
star
30

leon-web

Web-interface for Leon
Scala
2
star
31

stainless-project.g8

Giter8 template for Stainless-enabled projects
Scala
2
star
32

GrammarComparison

A System for Analyzing and Comparing Context-Free Grammars
Scala
2
star
33

scala-native-stainless-sample

Scala
1
star
34

Deep_Learning_On_Code_With_A_Graph_Vocabulary

Code to reproduce the experiments in the paper Deep Learning On Code With A Graph Vocabulary
Python
1
star
35

funprog-lambda

Scala
1
star
36

STIX-showcase

Scala
1
star
37

verified-lambda

A verified lambda interpreter
Scala
1
star