Correctness-by-Construction and Post-hoc Verification: friends or foes?

A track at ISoLA 2016

7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation

13 October 2016
Corfu, Greece

Motivation | Aim and topics of interest | Important dates | Publication and special issues | Invited speakers and program | Track chairs | ISoLA 2016


Correctness-by-Construction (CbC) sees the development of software (systems) as a true form of Engineering, with a capital 'E'. CbC advocates a step-wise refinement process from specification to code, ideally by CbC design tools that automatically generate error-free software implementations from rigorous and unambiguous specifications of requirements. Afterwards, testing only serves the purpose of validating the CbC process rather than to find bugs. (Of course, bugs might still be present outside the boundaries of the verified system: libraries, compilers, hardware, etc.)

In Post-hoc Verification (PhV), on the other hand, formal methods and tools are applied only after the (software) system has been constructed, but not during the development process. Typically, a formal specification of (an abstraction of) the implemented system describes how it should behave, after which V&V techniques like testing, bug finding, model checking, and deductive verification are used to check whether the implementation indeed satisfies the specifications and meets the user's needs. While two independent system models that are verified against each other can provide additional assurance that the designers' intentions are correctly captured, PhV is notoriously difficult to carry out.

Recently, numerous techniques and fields of application witness initiatives that attempt to integrate elements of both ends of the spectrum, with the aim of satisfying the holy grail of improving the correctness of software systems as well as their time-to-market, and to do so at a reasonable cost (e.g., Design for Verification or Lightweight Verification).


This track aims to bring together researchers and practitioners interested in the inherent "tension" that is usually felt when one tries to balance the pros and cons of CbC versus PhV.

We therefore invite researchers and practitioners from the following communities to shed their light on CbC versus PhV:


Paper submission April 15, 2016
Notification of acceptance May 31, 2016
Camera-ready version July 15, 2016
Early registration August 22, 2016
Symposium ISoLA 2016 October 10-14, 2016


The ISoLA proceedings will appear in Springer's Lecture Notes in Computer Science (LNCS) series.


Selected contributions will be invited to Innovations in Systems and Software Engineering: A NASA Journal, to Thematic Sections in the International Journal on Software Tools for Technology Transfer (STTT) or to the newly founded LNCS Transactions on Foundations for Mastering Change (FoMaC).


 9:00 -  9:15   Track introduction

 9:15 - 10:30   Keynote by Bruce Watson (Stellenbosch University, South Africa):
       Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience?

10:30 - 11:00   Coffee break

11:00 - 11:30   Bernhard Beckert (KIT, Karlsruhe, Germany):
       Deductive Verification of Legacy Code

11:30 - 12:00   Loek Cleophas (Umeå University, Sweden):
       Correctness-by-Construction /\ Taxonomies => Deep Comprehension of Algorithm Families

12:00 - 12:30   Jetty Kleijn (Leiden University, The Netherlands):
       Conditions for Compatibility of Components: The case of masters and slaves

12:30 - 14:00   Lunch

14:00 - 14:30   Axel Legay (Inria Rennes, France):
       A Logic for Statistical Model Checking of Dynamic Software Architectures

14:30 - 15:00   Dominique Méry (Loria, Nancy, France):
       On two Friends for getting Correct Programs: Automatically Translating Event-B Specifications to Recursive Algorithms in Rodin

15:00 - 15:30   Ina Schaefer (TU Braunschweig, Germany):
       Proof-Carrying Apps: Contract-Based Deployment-Time Verification

15:30 - 16:00   Coffee break

16:00 - 16:30   Erik de Vink (TU Eindhoven, The Netherlands):
       Supervisory Controller Synthesis for Product Lines with CIF 3

16:30 - 17:00   Dirk Beyer (LMU Munich, Germany):
       Partial Verification and Intermediate Results as a Solution to Combine Automatic and Interactive Verification Techniques

17:00 - 17:30   Discussion


Maurice ter Beek ISTI-CNR, Pisa, Italy
Reiner Hähnle TU Darmstadt, Germany
Ina Schaefer TU Braunschweig, Germany

For more information, please e-mail one of the track chairs.