Hi everyone,
We are pleased to share with you Verification for Dummies: SMT and Induction, a complete and detailed series of blogposts written by Adrien Champion about Induction as a formal verification technique.
The subject is treated with many concrete and executable examples. All examples can be (and should be) launched locally by readers thanks to small and easy to find tools. Modification and experimentation are strongly encouraged!
Take a look at all the notions covered:
- introduction to 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.
We hope you enjoy reading and we look forward to your feedback!