Are there examples (code) of using Aneris?
Closed this issue · 4 comments
Hi creators of Aneris. I am interested in this project and would like to play with it. There are several examples mentioned in the paper such as the "Add" client-server protocol. Do you mind sharing the source code (aneris program, spec, and proof) of such examples?
Thank you.
The Coq development from the ESOP paper is available on iris-project.org. There is also an artifact for our POPL 2022 paper. We are working on making all the developments available on GitHub (together with all the examples, newest version of the project, etc) very soon.
Much appreciated.
I am not very experienced with Iris and am studying it. If you don't mind, will you be so kind to show me how the calculator example (one server adding two ints) is proved with this GitHub version of Aneris? I notice that the esop examples are developed with an old version and I'm trying to redo it, but I'm having trouble proceeding.
The repository has now been updated and contains multiple example usages and case studies. For an introductory example, check out the ping_pong folder in aneris/examples. If you have questions, don't hesitate to send me an e-mail at gregersen@cs.au.dk.