Mon 5 Nov 2018 15:30 - 16:00 at Franklin - III Chair(s): Peter Chapin

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

hilt-2018-papers
15:30 - 17:00: HILT 2018 - III at Franklin
Chair(s): Peter ChapinVermont Technical College
hilt-2018-papers15:30 - 16:00
Short-paper
hilt-2018-papers16:00 - 16:30
Short-paper
Dara LyCEA LIST, Nikolai KosmatovCEA List, Frederic LoulergueNorthern Arizona University, Julien SignolesCEA LIST
hilt-2018-papers16:30 - 16:55
Short-paper
Andrew BernsUniversity of Northern Iowa, James CurbowUniversity of Northern Iowa, Joshua HilliardUniversity of Northern Iowa, Sheriff JorkehUniversity of Northern Iowa, Miho SandersUniversity of Northern Iowa
hilt-2018-papers16:55 - 17:00
Social Event