Software Verification in Ada/SPARK
Aus International Center for Computational Logic
Software Verification in Ada/SPARK
Vortrag von Marcos Cramer
- Veranstaltungsort: APB 2026
- Beginn: 16. Oktober 2025 um 11:00
- Ende: 16. Oktober 2025 um 12:00
- Forschungsgruppe: Wissensbasierte Systeme
- Event series: Research Seminar Logic and AI
- iCal
Formal software verification seeks to establish logical properties of programs with mathematical rigor, rather than relying solely on empirical testing. Ada/SPARK provides a verification-oriented programming environment in which contracts (preconditions, postconditions, invariants) serve as logical specifications embedded in the code. These contracts enable modular reasoning about subprograms and allow the GNATprove tool to discharge proofs of safety properties, functional correctness and termination. I will outline this verification
workflow, illustrate typical classes of provable properties and discuss current industrial applications.
