3 ms·
Does anyone know of any good resources explaining how a theorem prover like Coq is actually used to prove safety properties of software? All the resources I’ve
by Pelayu 2y ago
Does anyone know of any good resources explaining how a theorem prover like Coq is actually used to prove safety properties of software? All the resources I’ve found thus far have been more in the pure mathematics domain, and not so much about applying it to software.
- lheck 2y agoColleagues of mine are using it to verify concurrent programs: https://iris-project.org/tutorial-material.html https://iris-project.org/tutorial-material.html
- SubjectToChange 2y agoSoftware Foundations is quite a comprehensive series on program verification.