Projects per year
Abstract
Many problems related to distributed and parallel systems, such as scheduling and optimisation, are computationally hard, thereby justifying the adoption of SMT solvers. The latter provide standard arithmetic as interpreted functions, naturally leading to express concurrent executions as a linearlyordered sequentialisation (or interleaving) of events, which have an obvious correspondence with integer segments and therefore permit to take advantage of such arithmetical capabilities. However, there are alternative semantic approaches (also known as true concurrent) not imposing the extra step of interleaving events, which brings the question of how to computationally exploit SMT solvers inthese approaches. This paper presents a solution to this problem, and introduces a metric, made possible by adopting a true concurrent paradigm, which relates mutually distinct solutions of a family of distributed optimisation problems. We also contribute an original, computational definition of degree of parallelism, which we compare with the existing ones. Finally,we use theorem proving to formally certify a basic correctness property of our true concurrent approach.
Original language  English 

Title of host publication  Proceedings of the 35th Italian Conference on Computational Logic  CILC 2020, Rende, Italy, October 1315, 2020 
Editors  Francesco Calimeri, Simona Perri, Ester Zumpano 
Pages  357371 
Publication status  Published  24 Oct 2020 
Publication series
Name  CEUR Workshop Proceedings 

ISSN (Electronic)  16130073 
Fingerprint
Dive into the research topics of 'A formally verified SMT approach to true concurrency'. Together they form a unique fingerprint.Projects
 2 Finished

Rutherford Fellowship: Stochastic models to enable tailoring of medications to patients with multiple morbidities
Kuster Filipe Bowles, J. & Caminati, M. B.
15/02/18 → 13/03/22
Project: Fellowship

Automated Conflict Resolution: Automated Conflic Resolution in Clinical Pathways
1/07/15 → 15/12/18
Project: Standard