This program is tentative and subject to change.
Software specifications often come in the form of contracts, detailing in particular pre- and postconditions of functions, libraries or modules. Research on contracts often centers around questions of contract inference or contract validation. In this paper, we study the less investigated aspect of quality of contracts. More specifically, we define the concept of redundancy for preconditions and propose three techniques with differing efficiency and effectiveness for detecting redundant preconditions. All three techniques are implemented within a software verification tool, and we present results of an experimental valuation on a dataset of more than 60 C programs. The results confirm differences in precision and resource consumption of the techniques but also reveal unexpected outcomes about the completeness of the most precise, predicate analysis based technique.
This program is tentative and subject to change.
Sun 27 AprDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:30 | |||
16:00 30mTalk | Specifying Distributed Hash Tables with Allen Temporal Logic Research Track Nuno Policarpo Instituto Superior Técnico, University of Lisbon, José Fragoso Santos INESC-ID/Instituto Superior Técnico, Portugal , Alcino Cunha University of Minho; INESC TEC, João Leitão NOVA LINCS & FCT, NOVA University of Lisbon, Pedro Ákos Costa NOVA LINCS & DI-FCT-UNL | ||
16:30 30mTalk | Temporal Logics Meet Real-World Software Requirements: A Reality Check Research Track Roman Bögli University of Bern, Atefeh Rohani University of Bern, Thomas Studer University of Bern, Christos Tsigkanos University of Athens, Greece, Timo Kehrer University of Bern | ||
17:00 30mTalk | Detecting Redundant Preconditions Research Track Nicola Thoben University of Oldenburg, Heike Wehrheim Carl von Ossietzky Universität Oldenburg / University of Oldenburg |