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

Design-by-contract is a light-weight formal development paradigm, in which object-oriented software is specified with so-called software contracts. Contracts are annotations in the source code that explicitly document intended functional behavior and can be used for verifying correctness of a particular implementation or as test oracles during automatic test case generation. As writing strong specifications is an expensive and error-prone activity due to lack of expertise and tool support, developers are often only willing to write simpler specifications, covering only a fraction of all functional properties. As a consequence, software quality is lowered, or even worse, potential bugs remain undetected during software verification. To give developers a sense of specification coverage, we propose a methodology that considers the degree of incomplete specifications by means of mutation analysis. We consider Java programs annotated with JML and employ the deductive program verifier KeY–2.7.0 to show that this approach is applicable to numerous open-source JML projects from the literature.

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