Alt-Ergo Use Cases

1. Discharging SPARK Verification Conditions With Alt-Ergo

HTML     |      PDF

Alt-Ergo is used by AdaCore in the SPARK 2014 tool to verify programs written in the SPARK language: a verifiable subset of Ada used in the design of critical systems.