ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Tue 9 Apr 2019 10:30 - 11:00 at JUPITER - Software Verification I Chair(s): Wil van der Aalst

Correctness-by-Construction (CbC) is an approach to incrementally create formally correct programs guided by pre- and postcondition specifications. A program is created using refinement rules that guarantee the resulting implementation is correct with respect to the specification. Although CbC leads to code with a low defect rate, it is not widespread, also because appropriate tool support is missing. To close the gap, we provide tool support for CbC-based program development. We present CorC, a graphical and textual IDE to create programs in a simple while-language following the CbC approach. Starting with a specification, our open source tool supports CbC developers to refine a program by a sequence of refinement steps and to verify the correctness of these refinement steps using the theorem prover KeY. We evaluated the tool with a set of standard examples on CbC where we reveal errors in the provided specification. The evaluation also shows that our tool reduce the verification time in comparison to post-hoc verification.

Tue 9 Apr

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

10:30 - 12:30
Software Verification IFASE at JUPITER
Chair(s): Wil van der Aalst RWTH Aachen
10:30
30m
Talk
Tool Support for Correctness-by-Construction
FASE
Tobias Runge TU Braunschweig, Ina Schaefer Technische Universität Braunschweig, Loek Cleophas Eindhoven University of Technology (TU/e) and Stellenbosch University (SU), Thomas Thüm University of Ulm, Derrick Kourie Stellenbosch University, Bruce W Watson
Link to publication
11:00
30m
Talk
Automatic Modeling for Opaque Code in JavaScript Static Analysis
FASE
Joonyoung Park , Alexander Jordan Oracle Labs, Australia, Sukyoung Ryu KAIST, South Korea
Link to publication
11:30
30m
Talk
SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language
FASE
Min Zhang East China Normal University, Fu Song , Frederic Mallet Université Côte d'Azur, France, Xiaohong Chen
Link to publication
12:00
30m
Talk
A Hybrid Dynamic Logic for Event/Data-based SystemsBest paper nomination
FASE
Rolf Hennicker Ludwig Maximilians University Munich, Germany, Alexandre Madeira , Alexander Knapp
Link to publication