SPARK by Example: an introduction to formal verification through the standard C++ library (HILT 2018 - Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems)

Sun 4 - Fri 9 November 2018 Boston, Massachusetts, United States

Who

Léo Creuse, Joffrey Huguet, Christophe Garion, Jerome Hugues

Track

HILT 2018

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

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

Abstract

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.

Léo Creuse

ISAE

Joffrey Huguet

ISAE

Christophe GarionPresenter

ISAE-SUPAERO

France

Jerome Hugues

ISAE

France

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Mon 5 Nov
Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 17:00	IIIHILT at Franklin Chair(s): Peter Chapin Vermont Technical College

15:30 30m Short-paper		SPARK by Example: an introduction to formal verification through the standard C++ library HILT Léo Creuse ISAE, Joffrey Huguet ISAE, P: Christophe Garion ISAE-SUPAERO, Jerome Hugues ISAE
16:00 30m Short-paper		Soundness of a Dataflow Analysis for Memory Monitoring HILT P: Dara Ly CEA LIST, Nikolai Kosmatov CEA List, Frederic Loulergue Northern Arizona University, Julien Signoles CEA LIST
16:30 25m Short-paper		Minimal Specifications for Detecting Security Vulnerabilities HILT P: Andrew Berns University of Northern Iowa, James Curbow University of Northern Iowa, Joshua Hilliard University of Northern Iowa, Sheriff Jorkeh University of Northern Iowa, Miho Sanders University of Northern Iowa
16:55 5m Social Event		6:30PM HILT Banquet at Legal Seafoods, Park Plaza, preceded by SIGAda EC meeting from 5:15 to 6:15PM HILT