title=Introduction aux RPCs dans Tezos : exemple d’un portefeuille (wallet) simple
authors=Fabrice Le Fessant
date=2018-11-20
category=Blockchains
tags=tezos,rpc,fr
Dans cet article technique, nous introduisons brièvement les RPCs dans Tezos à travers un exemple simple montrant comment le client Tezos
interagit avec le noeud lors d’une instruction de transfert. Les RPCs de Tezos sont des requêtes HTTP (GET ou POST) auxquelles les noeuds Tezos
répondent dans un fichier au format JSON. Elles sont la seule façon pour les wallets d’interagir avec [Read more…](/2018/11/15/an-introduction-to-tezos-rpcs-a-basic-wallet/)
title=Release de Techelson, moteur de tests pour Michelson et Liquidity
authors=Adrien Champion
date=2019-03-05
category=Blockchains
tags=techelson,fr
Nous sommes fiers d’annoncer la première release de Techelson, moteur d’exécution de tests pour Michelson. Les programmeurs Liquidity peuvent également l’utiliser.
Voir [Techelson, a test execution engine for Michelson](/2019/03/05/techelson-a-test-execution-engine-for-michelson/).
Les résultats de la compétition SMT-COMP 2019 ont été publiés au whorkshop SMT de la [22e conférence SAT](https://smt2019.galois.com/). Nous étions fiers d’y participer pour la deuxième année consécutive, surtout depuis qu’Alt-Ergo [prend en charge](/2019/02/11/whats-new-for-alt-ergo-in-2018-here-is-a-recap/) le standard [SMT-LIB 2](https://smtlib.cs.uiowa.edu/).
> Alt-Ergo est un SAT solveur open-source maintenu et distribué par OCamlPro, et financé entre autres grâce à plusieurs projets de R&D collaborative (BWare, SOPRANO, Vocal, LChip).
> Si vous êtes un utilisateur d’Alt-Ergo, songez à rejoindre le [Club des Utilisateurs d’Alt-Ergo](https://alt-ergo.ocamlpro.com/#club)! L’histoire de ce logiciel remonte à 2006, où il est né de recherches académiques conjointes entre Inria et le CNRS dans le laboratoire du LRI. Il est depuis septembre 2013 maintenu, développé et distribué par OCamlPro (voir l’historique des [versions passées](https://alt-ergo.ocamlpro.com/#releases)).
> *Si vous êtes curieux des activités d’OCamlPro dans le domaine des méthodes formelles, vous pouvez lire le court témoignage d’un [client heureux](http://ocamlpro.com/clients-partners/#mitsubishi-merce).*
@@ -23,4 +23,4 @@ Nos membres sont particulièrement intéressés par les points suivants :
– L’amélioration du support de l’arithmétique non linéaire dans Alt-Ergo
Ces fonctionnalités sont maintenant nos principales priorités. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos [articles](category/formal_methods) sur ce blog.
\ No newline at end of file
Ces fonctionnalités sont maintenant nos principales priorités. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos [articles](category/formal_methods) sur ce blog.
@@ -2,7 +2,7 @@ title=Réunion annuelle du Club des utilisateurs d’Alt-Ergo 2021
authors=OCamlPro
date=2021-04-29
category=Formal Methods
tags=alt-ergo
tags=alt-ergo,fr
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.
-[](http://creativecommons.org/licenses/by-sa/4.0/) This work is licensed under a [Creative Commons Attribution-ShareAlike 4.0 International License](http://creativecommons.org/licenses/by-sa/4.0/).
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://github.com/rust-lang/this-week-in-rust/pull/2479)[https://ocamlpro.github.io/verification_for_dummies/](https://ocamlpro.github.io/verification_for_dummies/)
