SPARK by Example: an introduction to formal verification through the standard C++ library
This paper presents SPARK by Example, a guide for people wanting to get involved in formal verification of SPARK programs. SPARK by Example is inspired by ACSL by Example, a similar effort for C/ACSL programs, and provides users detailed specification, implementation and proof of classic algorithms (array manipulation, sorting, heap etc). A comparison between ACSL and SPARK is done in the light of proof performance and ease of use.
Mon 5 NovDisplayed time zone: Guadalajara, Mexico City, Monterrey change
15:30 - 17:00
|SPARK by Example: an introduction to formal verification through the standard C++ library|
|Soundness of a Dataflow Analysis for Memory Monitoring|
|Minimal Specifications for Detecting Security Vulnerabilities|
|6:30PM HILT Banquet at Legal Seafoods, Park Plaza, preceded by SIGAda EC meeting from 5:15 to 6:15PM|