The scope of this post is limited to formal verification of algorithms and protocols.
To save docker images to my repo,
docker pull official/imagename
docker image tag official/imagename:latest myusername/imagename:latest
docker push myusername/imagename:latest
TLA+
Check the correctness of a specification.
Not tied to a specific implementation or tests of an implementation.
Not tied to a specific implementation or tests of an implementation.
Jepsen
"Jepsen is a Clojure library. A test is a Clojure program which uses the Jepsen library to set up a distributed system, run a bunch of operations against that system, and verify that the history of those operations makes sense."
For distributed systems, introduce {partitions, added resources, removed resources, delays, clock skew} and other noises, run operations, and then compare against expected results.
Stateright
"Stateright is a Rust actor library that aims to solve this problem by providing an embedded model checker, a UI for exploring system behavior (demo), and a lightweight actor runtime. It also features a linearizability tester that can be run within the model checker for more exhaustive test coverage than similar solutions such as Jepsen."
F*
Can generate C, as well as parser/generators.
Not explicitly temporal (whereas TLA+ is explicitly about temporal actions), but F* could be used for temporal models.
Why3
https://why3.lri.fr/
Z3
written by the same developer as SMV after the developer moved to Microsoft
https://github.com/z3prover/z3/pkgs/container/z3
Coq
constructive dependent type theory
Lean
"Simple formally verified compiler in Lean" by Ericson (2021)
SMV
CMU's SMV --> Cadence SMV --> nuSMV
https://swmath.org/software/7795
http://mcmil.net/smv.html
https://www.cs.cmu.edu/~modelcheck/smv.html
https://sws.cs.ru.nl/publications/papers/biniam/smv/
https://web.cs.wpi.edu/~kfisler/Courses/525V/S02/Readings/smv-cadence.pdf
https://nusmv.fbk.eu/
https://en.wikipedia.org/wiki/NuSMV
Isabelle/HOL
simple type theory
Alloy
Cryptol
Spin and Promela
P
Event B
"a modelling method for formalising and developing systems whose components can be modelled as discrete transition systems. An evolution of the (classical) B-method, Event-B is now centred around the general notion of events, which are also found in other formal methods such as Action Systems, TLA and UNITY."
An Introduction to the Event-B Modelling Method
Translating B to TLA+ for Validation with TLC
https://www3.hhu.de/stups/downloads/pdf/HansenLeuschel_TLC4B_techreport.pdf
https://www.sciencedirect.com/science/article/pii/S0167642316300235
classical B for software development
No comments:
Post a Comment