[Why3-club] Formal verification of smart contracts
Jean-Christophe.Filliatre at lri.fr
Tue Aug 2 08:33:15 CEST 2016
js_of_ocaml ; see http://ocsigen.org/js_of_ocaml/
The sources of trywhy3 are in the subdirectory src/trywhy3/ of Why3
sources. In this subdirectory, you'll find a README file containing
a font, and the Alt-Ergo SMT solver are requirements).
Let us know if you have questions.
On 01/08/2016 17:16, Christian Reitwiessner wrote:
> Dear Jean-Christophe,
> thank you for the remarks! I chose to encode the restrictions of the
> virtual machine as part of the code and not as part of the conditions,
> because of the complications with the to_int projection. In the
> meantime, our project is available online, some introduction can be
> found here:
> Our main "IDE" can be found at https://ethereum.github.io/browser-solidity
> Just like "try why3" it works fully in the browser, and I would like to
> integrate the browser version of why3 together with alt-ergo directly
> into that IDE.
> cannot use it as is. Could you perhaps provide me with some pointers
> that can be better integrated into browser projects?
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club