Merge requests · Why3 / why3 · GitLab

Mentions légales du service

New front-end language: Coma

!1095 · created Jul 01, 2024 by PATAULT Paul
- Closed
updated Jul 03, 2024
Recognize both 8.19 and 8.20 as supported versions of Coq.

!1100 · created Jul 04, 2024 by Guillaume Melquiond 1.8.0
component: provers
- Merged
updated Jul 04, 2024
Resolve "Forward propagation strategy bug"

!1096 · created Jul 01, 2024 by BONNOT Paul
updated Jul 05, 2024
new example: search in a two-dimensional grid

!1101 · created Jul 06, 2024 by Jean-Christophe Filliâtre
- Merged
updated Jul 06, 2024
Improve the RAC execution log in the incomplete case

!1102 · created Jul 09, 2024 by Matteo Manighetti
ProofInUse/AdaCore
- Merged
- 3
updated Jul 11, 2024
Remove redondancy of bv_size definition in mach.bv.

!1104 · created Jul 15, 2024 by Jacques-Henri Jourdan
- Merged
updated Jul 15, 2024
Register main function of why3 commands instead of directly executing them

!1105 · created Jul 16, 2024 by Matteo Manighetti 1.8.0
component: tools
- Merged
- 2
updated Jul 25, 2024
Draft: Resolve "examples/multiprecision fails to compile"

!1107 · created Aug 09, 2024 by Gérald Point
component: examples
- Closed
updated Aug 09, 2024
no need for FPa for these proofs

!1110 · created Sep 02, 2024 by MARCHE Claude
- Merged
updated Sep 02, 2024
compute a list length as a 63-bit integer

!1111 · created Sep 02, 2024 by MARCHE Claude
- Merged
- 2
updated Sep 02, 2024
List length via peano

!1112 · created Sep 02, 2024 by MARCHE Claude
- Merged
- 2
updated Sep 03, 2024
New front-end language: Coma

!1098 · created Jul 03, 2024 by PATAULT Paul
- Merged
updated Sep 04, 2024
new example: Knuth's bubble sort

!1114 · created Sep 05, 2024 by Jean-Christophe Filliâtre
- Merged
updated Sep 05, 2024
Draft: Verifythis 2024 solutions

!1048 · created Apr 12, 2024 by Jean-Christophe Filliâtre
- Closed
updated Sep 12, 2024
new examples: verifythis 2024 solutions to challenges 0 and 1

!1115 · created Sep 12, 2024 by Jean-Christophe Filliâtre
- Merged
updated Sep 12, 2024
Resolve "Call_provers.analyze_result defaults to unknown"

!1109 · created Aug 28, 2024 by Matteo Manighetti 1.7.3
Décysif ProofInUse/AdaCore
- Merged
- 14
updated Sep 16, 2024
Augment documentation of extraction to C

!1117 · created Sep 13, 2024 by MARCHE Claude 1.8.0
ProofInUse/MERCE
- Merged
updated Sep 17, 2024
Resolve "Driver Alt-Ergo FPA should not use the AE builtin for abs on reals"

!1120 · created Sep 16, 2024 by MARCHE Claude 1.7.3
Décysif
- Merged
updated Sep 17, 2024
Add BVConverter_XX_256 to stdlib.bv

!1118 · created Sep 16, 2024 by Jacques-Henri Jourdan 1.8.0
- Merged
- 3
updated Sep 17, 2024
coma: fix wrong levels in `factorize` and missing negations in `t_neg`

!1123 · created Sep 17, 2024 by Andrei Paskevich
- Merged
updated Sep 17, 2024

Prev
1
…
51
52
53
54
55
56
57
58
59
…
61
Next