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.

Conference Day
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
14:00
30m
Talk
Methodology for Specification and Verification of High-Level Properties with MetAcsl
FormaliSE 2021
Virgile RoblesCEA List, Software Reliability and Security Lab, Nikolai KosmatovCEA List, Virgile PrevostoCEA Tech List, Louis RillingDGA Maîtrise de l'Information, Pascale Le GallCentraleSupelec
Pre-print
14:30
30m
Talk
How much Specification is Enough? Mutation Analysis for Software Contracts
FormaliSE 2021
Alexander KnüppelTU Braunschweig, Leon SchaerTU Braunschweig, Ina SchaeferTU Braunschweig

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