4 ms·
Very cool project with a great name! If you haven't looked at it already, you may be interested in Arthur Charguéraud's work on program verification using cha
by fmap 10y ago
Very cool project with a great name!
If you haven't looked at it already, you may be interested in Arthur Charguéraud's work on program verification using characteristic formulas (http://www.chargueraud.org/softs/cfml http://www.chargueraud.org/softs/cfml). CFML is a similar tool for ocaml verification using Coq.
- derkha 10y agoI have heard of it, it features a nice application of Separation Logic. Though not needing that kind of logic at all does feel even better! There is also an extension of an extension of CFML to asymptotic complexity analysis, after which I may model my own analysis: http://gallium.inria.fr/blog/formally-verified-complexity-with-cfml-part-1/ http://gallium.inria.fr/blog/formally-verified-complexity-wi...