Merge requests · Why3 / why3 · GitLab

Mentions légales du service

Add algorithms for computational real operations

!139 · created May 07, 2019 by François Bobot
- 5
updated Dec 06, 2024
[WIP] use Dune 0 of 4 checklist items completed

!229 · created Sep 19, 2019 by François Bobot 1.9.0
component: build system
- 12
- 1
updated Sep 18, 2024
[WIP] Add a cache to the call of provers

!231 · created Sep 20, 2019 by François Bobot
To be discussed
- 6
updated Sep 24, 2019
WIP: Add well_formed for type invariant

!283 · created Nov 27, 2019 by DAILLER Sylvain
[WIP] Résoudre les problèmes de performance avec Patricia Tree hashconsé

!327 · created Feb 28, 2020 by François Bobot
- 1
WIP: Resolve "Sequence literals"

!371 · created Apr 22, 2020 by Claudio Belo Lourenco
To be discussed component: core component: syntax
updated Jun 26, 2020
Draft: Simplify euclidean to computer division

!479 · created Feb 06, 2021 by François Bobot
- 1
updated Mar 07, 2023
Draft: Predicate `list.Sorted.sorted` recursively-defined.

!571 · created Sep 03, 2021 by Mario Pereira
- 6
updated Sep 08, 2021
Draft: Add support for Odoc

!592 · created Sep 24, 2021 by Guillaume Melquiond
component: build system component: documentation
- 1
updated Sep 03, 2022
[Env] Generalize env with resolver

!674 · created May 09, 2022 by François Bobot
- 2
updated May 09, 2022
Draft: Resolve "rac prover should be executed on a task before transformation compute"

!743 · created Oct 04, 2022 by MARCHE Claude
ProofInUse/AdaCore ProofInUse/TrustInSoft To be discussed
updated Aug 29, 2023
Loc: enumerate columns starting from 1, not from 0

!760 · created Oct 26, 2022 by Andrei Paskevich
To be discussed
- 11
- 1
updated Jan 11, 2023
micro-Python: global variables and logic functions

!775 · created Nov 17, 2022 by Jean-Christophe Filliâtre
updated Nov 17, 2022
Resolve "Support for ADT in Alt-Ergo"

!786 · created Dec 06, 2022 by BONNOT Paul 1.9.0
Décysif ProofInUse/OCamlPro ProofInUse/TrustInSoft
- 9
updated Dec 06, 2024
Try to use nicer name when compiling pattern

!790 · created Jan 09, 2023 by François Bobot
SMTLIB theory of sequences

!803 · created Jan 31, 2023 by Jacques-Henri Jourdan
- 15
updated Mar 22, 2023
Draft: [whyconf] lookup for external prover config

!811 · created Feb 15, 2023 by Loïc Correnson
updated Jun 27, 2023
Draft: Resolve "Counterexamples for labels bug"

!814 · created Feb 20, 2023 by MOREAU Solene
ProofInUse/AdaCore ProofInUse/TrustInSoft component: counterexample
- 1
updated Feb 21, 2023
Draft: Resolve "keep less unused symbols"

!859 · created Apr 18, 2023 by MARCHE Claude
Hackathon component: counterexample
updated Oct 22, 2024
Draft: Resolve "CE: variables in concrete terms should be denoted by idents instead of strings"

!863 · created Apr 21, 2023 by MARCHE Claude
ProofInUse/TrustInSoft
updated Aug 29, 2023

Prev
1
2
Next