3 ms·
I don't know details. GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions t
by xentropy 6y ago
I 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