Write a Blog >>
FormaliSE 2021
Tue 18 - Fri 21 May 2021
co-located with ICSE 2021
Tue 18 May 2021 14:00 - 14:30 at FormaliSE Room - Property and contract specification

Specification and formal verification of high-level properties (such as security properties, like data integrity or confidentiality) over a large software product remains an important challenge for the industrial practice. Recent work proposed meta, a plugin of the Frama-C verification platform, that allows the user to specify high-level properties for C programs and transform them into assertions that can then be verified by classic deductive verification. This paper presents a methodology of specification and verification of a wide range of high-level properties with meta and illustrates it on several examples. The goal is to provide verification practitioners with detailed methodological guidelines for common patterns of properties in order to facilitate their everyday work and to avoid some frequent pitfalls. The illustrating examples are inspired by very frequent kinds of properties and illustrated on two use cases. One of them – on the real-life code of the bootloader module of the secure storage device Wookey – was fully verified using the described approach, demonstrating its capacity to scale to real-life code. The other one – on a microkernel of an OS – was added to illustrate other common kinds of properties, where the description of the system was intentionally left as generic as possible.

Tue 18 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:00
Property and contract specificationFormaliSE 2021 at FormaliSE Room
Methodology for Specification and Verification of High-Level Properties with MetAcsl
FormaliSE 2021
Virgile Robles CEA List, Software Reliability and Security Lab, Nikolai Kosmatov CEA List, Virgile Prevosto CEA Tech List, Louis Rilling DGA Maîtrise de l'Information, Pascale Le Gall CentraleSupelec
Pre-print Media Attached
How much Specification is Enough? Mutation Analysis for Software Contracts
FormaliSE 2021
Alexander Knüppel TU Braunschweig, Leon Schaer TU Braunschweig, Ina Schaefer TU Braunschweig
Media Attached

Information for Participants
Tue 18 May 2021 14:00 - 15:00 at FormaliSE Room - Property and contract specification
Info for room FormaliSE Room:

Go directly to this room on Clowdr