Held by Sorin Stratulat and Renata Bunoiu in 02 July 2020 on Google Meet
Abstract
We present an overview of our teaching materials related to Automated Reasoning and the ARC book, concerning:
- Mathematical logic
- Proofs by induction
- Static analysis of Java code using JML
- Applications
Some examples are given using the following tools:
- The SPIKE prover (https://github.com/sorinica/spike-prover/wiki)
- PVS (https://pvs.csl.sri.com/)
- COQ (https://coq.inria.fr/)
- Esc/Java (https://kindsoftware.com/products/opensource/ESCJava2/) and OpenJML (https://www.openjml.org/)