Verification for Dummies: SMT and Induction
- Adrien Champion firstname.lastname@example.org
- This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
These posts broadly discusses induction as a formal verification technique, which here really means formal program verification. I will use concrete, runnable examples whenever possible. Some of them can run directly in a browser, while others require to run small easy-to-retrieve tools locally. Such is the case for pretty much all examples dealing directly with induction.
The next chapters discuss the following notions:
- formal logics and formal frameworks;
- SMT-solving: modern, low-level verification building blocks;
- declarative transition systems;
- transition system unrolling;
- BMC and induction proofs over transition systems;
- candidate strengthening.
The approach presented here is far from being the only one when it comes to program verification. It happens to be relatively simple to understand, and I believe that familiarity with the notions discussed here makes understanding other approaches significantly easier.
This book thus hopes to serve both as a relatively deep dive into the specific technique of SMT-based induction, as well as an example of the technical challenges inherent to both developing and using automated proof engines.
Some chapters contain a few pieces of Rust code. Usually to provide a runnable version of a system under discussion, or to serve as example of actual code that we want to encode and verify. Some notions of Rust could definitely help in places, but this is not mandatory (probably).
Read more here: https://ocamlpro.github.io/verification_for_dummies/
OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust.
We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, TryOCaml, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch.
Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our Alt-Ergo Users'). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: email@example.com.