Commit 07b605e6 authored by Elias2049's avatar Elias2049
Browse files

Merge branch 'master' of into CssElias

parents e382d7f8 d45ccbf8
......@@ -195,3 +195,24 @@ This proof of concept shows how functor packs can ease some complicated build sy
Packs were an old concept mainly outdated by module aliases. They were not practical as they are some sort of monolithic libraries shaped into a unique module containing sub modules. While they perfectly use the module system for its namespacing properties, their usage enforces the compiler to link an entire library even if only one module is actually used. This improvement allows programmers to define big functors, functors that are split among multiple files, resulting in what we can view as a way to implement some form of parameterized libraries.
In the second part, we will cover another aspect of the rehabilitation of packs: using packs to implement mutually recursive compilation units.
# Comments
François Bobot (25 September 2020 at 9 h 16 min):
> I believe there is a typo
module Mylib (P : P_SIG) = struct
module A = A_funct(P)
module B = A_funct(P)
> The last must be `B_funct(P)`, the next example as also the same typo.
Pierrick Couderc (25 September 2020 at 10 h 31 min):
> Indeed, thank you!
Cyrus Omar (8 February 2021 at 3 h 49 min):
> This looks very useful! Any updates on this work? I’d like to be able to use it from dune.
......@@ -2,7 +2,7 @@ title=Réunion annuelle du Club des utilisateurs d’Alt-Ergo 2021
category=Formal Methods
La troisième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu le 1er avril ! Cette réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Nous avons eu le plaisir de recevoir nos partenaires pour discuter de la feuille de route concernant les développements et les améliorations futures d’Alt-Ergo.
title=Verification for Dummies: SMT and Induction
authors=Adrien Champion
category=Formal Methods
tags=trainings,smt,formal logic
- Adrien Champion [](
- []( 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: []([](
This diff is collapsed.
This diff is collapsed.
......@@ -6,7 +6,7 @@ OCamlPro and TypeRex are either registered trademarks or trademarks of OCamlPro
All other company and product names referenced in this Web site are used for identification purposes only and may be trade names or trademarks of their respective owners.
Copyright © 2011-2020 OCamlpro SAS. All Rights Reserved.
Copyright © 2011-2021 OCamlpro SAS. All Rights Reserved.
## Privacy
This diff is collapsed.
......@@ -45,6 +45,7 @@
<li><a class="dropdown-item" href="/course_mastering_opam_ocaml_tools">Mastering OPAM &amp; OCaml
<li><a class="dropdown-item" href="">Custom Training</a></li>
<li><a class="dropdown-item" href="/course_register">Register your team</a></li>
<li class="nav-item dropdown">
(public_name server)
(modules content server blog blog_content feed error meta)
(modules content server blog blog_content feed error meta urls)
(libraries dream omd ubase markup lambdasoup ez_file ez_subst))
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment