X-by-Construction: Correctness meets Probability

A track at ISoLA 2020

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

26-30 October 2020
Rhodes, Greece

Motivation | Aim and topics of interest | Important dates | Submission | Publication and special issues | Confirmed speakers | Track chairs | ISoLA 2020

Extended paper submission deadline: May 31, 2020


Correctness-by-Construction (C-by-C) approaches the development of software (systems) as a true form of Engineering, with a capital ‘E’. C-by-C advertises a stepwise refinement process from specification to code, ideally by C-by-C design tools that automatically generate error-free software (system) implementations from rigorous and unambiguous specifications of requirements. Afterwards, testing only serves to validate the C-by-C process rather than to find bugs. (Of course, bugs might still be present outside the boundaries of the verified system: in libraries, compilers, hardware, the C-by-C design tools themselves, etc.).

A lot of progress has been made in this domain, implying it is time to look further than correctness and investigate a move from C-by-C to X-by-C, i.e. by considering also non-functional properties. X-by-C is thus concerned with a step-wise refinement process from specification to code that automatically generates software (system) implementations that by-construction satisfy specific non-functional properties concerning security, dependability, reliability or resource/energy consumption, etc.


Building on the highly successful ISoLA 2018 track “X-by-Construction” (X-by-C) with a particular emphasis on security-by-construction, we again aim to bring together researchers and practitioners that are interested in C-by-C and X-by-C. In line with the growing attention to fault-tolerance (thanks to increasingly common failures in hardware and software) and the increasing use of machine learning techniques in modern software systems — in both of these contexts, guaranteed properties are hard to establish — we want to particularly emphasise X-by-C in the setting of probabilistic properties.

We therefore invite researchers and practitioners from (at least) the following communities to share their views on (moving from C-by-C to) X-by-C:


Please submit your paper here


Paper submission (extended) May 4, 2020 May 31, 2020
Notification of acceptance June 29, 2020
Camera-ready version August 2, 2020
Early registration September 1, 2020
Symposium ISoLA 2020 October 26-30, 2020


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 or to Thematic Sections in the International Journal on Software Tools for Technology Transfer (STTT).


Keynote speakers

Annabelle McIver / Carroll Morgan (Macquarie U & UNSW, Sydney, Australia)

Invited speakers

Christel Baier (TU Dresden, Germany)
Marius Bozga (U Grenoble Alpes, France)
Uli Fahrenberg (LIX, Palaiseau, France)
Manfred Jaeger (Aalborg U, Denmark)
Joost-Pieter Katoen (RWTH Aachen, Germany)
Bettina Könighofer (TU Graz, Austria)
Tatjana Petrov (University of Konstanz, Germany)
Mirco Tribastone (IMT Lucca, Italy)


Maurice H. ter Beek ISTI-CNR, Pisa, Italy
Loek Cleophas TU Eindhoven, The Netherlands
Axel Legay UC Louvain, Belgium
Ina Schaefer TU Braunschweig, Germany
Bruce W. Watson Stellenbosch University, South Africa

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