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 Nov (GMT-05:00) Guadalajara, Mexico City, Monterrey change
|15:30 - 16:00|
|16:00 - 16:30|
|16:30 - 16:55|
|16:55 - 17:00|