Skip to content

Research at St Andrews

A formally verified SMT approach to true concurrency

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 linearly-ordered 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.
Close

Details

Original languageEnglish
Title of host publicationProceedings of the 35th Italian Conference on Computational Logic - CILC 2020, Rende, Italy, October 13-15, 2020
EditorsFrancesco Calimeri, Simona Perri, Ester Zumpano
Pages357-371
Publication statusPublished - 24 Oct 2020

Publication series

NameCEUR Workshop Proceedings
ISSN (Electronic)1613-0073

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Correct composition in the presence of behavioural conflicts and dephasing

    Kuster Filipe Bowles, J. & Caminati, M. B., 1 Jan 2020, In: Science of Computer Programming. 185, 22 p., 102323.

    Research output: Contribution to journalArticlepeer-review

  2. A framework for automated conflict detection and resolution in medical guidelines

    Bowles, J., Caminati, M. B., Cha, S. & Mendoza, J., 1 Aug 2019, In: Science of Computer Programming. 182, p. 42-63 22 p.

    Research output: Contribution to journalArticlepeer-review

  3. An integrated approach to a combinatorial optimisation problem

    Kuster Filipe Bowles, J. & Caminati, M. B., 2019, Integrated Formal Methods: 15th International Conference, IFM 2019, Bergen, Norway, December 2–6, 2019, Proceedings. Ahrendt, W. & Tapia Tarifa, S. L. (eds.). LNCS ed. Cham: Springer, p. 284-302 19 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 11918).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Balancing prescriptions with constraint solvers

    Bowles, J. K. F. & Caminati, M. B., 2019, Automated Reasoning for Systems Biology and Medicine. Liò, P. & Zuliani, P. (eds.). Cham: Springer, p. 243-267 25 p. (Computational Biology; vol. 30).

    Research output: Chapter in Book/Report/Conference proceedingChapter

  5. Formalization and Automation of Quality Assurance Processes in Radiation Oncology

    Munbodh, R., Zaveri, H., Caminati, M. & Bowles, J., 31 Jul 2018, In: Medical Physics. 45, 6, p. E274-E274 1 p.

    Research output: Contribution to journalAbstractpeer-review

ID: 270618454

Top