Software Verification in Ada/SPARK
From International Center for Computational Logic
Software Verification in Ada/SPARK
Talk by Marcos Cramer
- Location: APB 2026
- Start: 16. October 2025 at 11:00 am
- End: 16. October 2025 at 12:00 pm
- Research group: Knowledge-Based Systems
- 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.
