Why3 Alternatives
Similar projects and alternatives to why3
-
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
sol2
Sol3 (sol2 v3.0) - a C++ <-> Lua API wrapper with advanced features and top notch performance - is here, and it's great! Documentation:
-
why3 reviews and mentions
-
Why the C Language Will Never Stop You from Making Mistakes
With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK.
However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.
AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:
https://github.com/AdaCore/why3
And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C:
https://github.com/gcc-mirror/gcc/tree/master/gcc/config
Compare with CompCert, the formally verified C compiler:
https://github.com/AbsInt/CompCert
Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:
https://softwarefoundations.cis.upenn.edu/
Stats
AdaCore/why3 is an open source project licensed under GNU General Public License v3.0 or later which is an OSI approved license.
The primary programming language of why3 is OCaml.
Popular Comparisons
Sponsored