From f1f2354db2c365d724a0109e4a4711dd8cac3790 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Thu, 21 Aug 2025 15:49:03 -0600 Subject: [PATCH] Add Why3, close #16 --- tools/sat-smt/why3.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tools/sat-smt/why3.md diff --git a/tools/sat-smt/why3.md b/tools/sat-smt/why3.md new file mode 100644 index 0000000..18885f4 --- /dev/null +++ b/tools/sat-smt/why3.md @@ -0,0 +1,21 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Why3' +subtitle = 'Theorem Prover' +links = [ + { title = "Homepage", url = "https://www.why3.org/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://why3.gitlabpages.inria.fr/releases/", icon = 'fa-brands fa-gitlab' }, + { title = "Playground", url = "https://www.why3.org/try/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver', 'Theorem Prover', 'SAT Solver'] +developers = ['Toccata', 'Inria', 'Universite Paris-Saclay', 'CNRS', 'Laboratoire Methodes Formelles'] +licenses = ['MIT'] +inputs = ['WhyML'] +interfaces = ['CLI', 'Online'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = ['deMoura2008'] ++++ + +Why3 is a platform for deductive program verification. \ No newline at end of file