3 ms·
It seems like the Why3 project attempts verification of only "simple" programs without concurrency and higher-order functions. On the other hand, the Iris Proje
by rav 8y ago
It seems like the Why3 project attempts verification of only "simple" programs without concurrency and higher-order functions. On the other hand, the Iris Project is an attempt to verify higher-order concurrent programs, see e.g. https://iris-project.org/pdfs/2017-case-study-verifying-dartino-framework.pdf https://iris-project.org/pdfs/2017-case-study-verifying-dart...
- kachnuv_ocasek 8y agoIris is a separation logic, a framework for proving the properties of programs. There are many like it, Iris is just one of the recent examples. To prove statements in this logic, you have to rely on the proving facilities of the host environment, for instance Coq in your linked example. Most of the proof is then written by hand and quite tedious. The difference is that Why3 attempts to automatise as much of this workload as possible, most frequently with the help of SMT solvers.