4 ms·
Thanks for clarification. Which underlying (type) theory is used in GNATprove?
by Kototama 6y ago
Thanks for clarification. Which underlying (type) theory is used in GNATprove?
- xentropy 6y agoI don't know details. GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3). https://github.com/AdaCore/spark2014 https://github.com/AdaCore/spark2014