X-by-Construction: call for expressions of interest

by Maurice ter Beek, Dec. 9, 2017

Deadline: January 15th 2018


A track at ISoLA 2018
8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation
5-9 November 2018
Limassol, Cyprus



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 advocates a step-wise 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 the purpose of validating the C-by-C process rather than to find bugs. 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 2016 track "Correctness-by-Construction and Post-hoc Verification: Friends or Foes?" which focussed on the combination of post-hoc verification with C-by-C, we decided to organise an "X-by-Construction" (X-by-C) track at ISoLA 2018, with the aim of bringing together researchers and practitioners that are interested in C-by-C and the promise of X-by-C. 

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

* People working on system-of-systems, who address modelling and verification (correctness, but also non-functional properties concerning security, reliability, resilience, energy consumption, performance and sustainability) of networks of interacting legacy and new software systems, and who are interested in applying X-by-C techniques in this domain in order to prove non-functional properties of systems-of-systems by construction (from their constituent systems satisfying these properties).

* People working on quantitative modelling and analysis (e.g. through probabilistic or real-time systems and probabilistic or statistical model checking) in particular in the specific setting of dynamic, adaptive or (runtime) reconfigurable systems with variability. These people work on lifting successful formal methods and verification tools from single systems to families of systems, i.e., modelling and analysis techniques that need to cope with the complexity of systems stemming from behaviour, variability, and randomness — and which focus not only on correctness but also on non-functional properties concerning safety, security, performance or dependability properties. As such, they may be interested in applying X-by-C techniques in this domain to prove non-functional properties of families of systems by construction (from their individual family members satisfying these properties).

* People working on generative software development, who are concerned with the automatic generation of software from specifications given in either general formal languages or domain-specific languages, leading to families of related software (systems). Also in this setting, the emphasis so far has typically been on functional correctness, but the restricted scope of the specifications — especially for domain-specific languages — may offer a suitable ground for reasoning about non-functional properties, and for using X-by-C techniques to guarantee such properties.

* People working on systems security, privacy and algorithmic transparency and accountability, who care about more than correctness. The application of X-by-C techniques could provide security guarantees from the outset when designing critical systems. It could also enforce transparency when developing algorithms for automated decision-making, in particular those based on data analytics — thus reducing algorithmic bias by avoiding opaque algorithms.


At this stage, we invite researchers and practitioners for expressions of interests, with a short abstract, by January 15th. Depending on the number and topic coverage of the expressions received, we will make a selection of contributors to invite for submitting a full paper to the X-by-Construction track.


Expression of interest: January 15, 2018

Invitation of selected authors: January 19, 2018

Paper submission: Early Spring, 2018

Notification of acceptance: Late Spring, 2018

Camera-ready version: Early Summer, 2018

Early registration: Late Summer, 2018

Symposium ISoLA 2018: November 5-9, 2018


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).


Following a keynote, there will be 3-4 sessions according to the ISoLA schedule, with three to four invited presentations of 20 minutes and 30 minutes for a general discussion. The sessions will be structured according to the different viewpoints or application fields from which the speakers approach X-by-C.


Erik Poll (Radboud University Nijmegen, The Netherlands)


Maurice H. ter Beek (ISTI-CNR, Italy) 

Loek Cleophas (TU Eindhoven, The Netherlands) 

Ina Schaefer (TU Braunschweig, Germany) 

Bruce W. Watson (Stellenbosch University, South Africa) 

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