Verifying real-world software with contracts for concurrency

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

1 Citation (Scopus)
5 Downloads (Pure)

Abstract

In this paper we present Contracts for Concurrency. A contract for concurrency specifies the protocol to access the services provided by a software module or library. A program that respects a (well-defined and complete) contract for a module is safe from high-level atomicity violations with respect to that module. On the other hand, violations of a contract may denote errors in the program, and the application of contracts for concurrency to some real-world open source software packages did uncover a few latent bugs.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationCham
PublisherSpringer
Pages70-73
Number of pages4
ISBN (Electronic)978-3-030-03427-6
ISBN (Print)978-3-030-03426-9
DOIs
Publication statusPublished - 1 Jan 2018
Event8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018 - Limassol, Cyprus
Duration: 5 Nov 20189 Nov 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume11247 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018
CountryCyprus
CityLimassol
Period5/11/189/11/18

Fingerprint

Concurrency
Software
Module
Atomicity
Open Source Software
Software Package
Software packages
Well-defined
Denote
Network protocols

Cite this

Lourenço, J. M. (2018). Verifying real-world software with contracts for concurrency. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings (pp. 70-73). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11247 LNCS). Cham: Springer. https://doi.org/10.1007/978-3-030-03427-6_9
Lourenço, João M. / Verifying real-world software with contracts for concurrency. Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Cham : Springer, 2018. pp. 70-73 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{44b9e5c6dfd441728d22ae97df0c1580,
title = "Verifying real-world software with contracts for concurrency",
abstract = "In this paper we present Contracts for Concurrency. A contract for concurrency specifies the protocol to access the services provided by a software module or library. A program that respects a (well-defined and complete) contract for a module is safe from high-level atomicity violations with respect to that module. On the other hand, violations of a contract may denote errors in the program, and the application of contracts for concurrency to some real-world open source software packages did uncover a few latent bugs.",
author = "Louren{\cc}o, {Jo{\~a}o M.}",
note = "NOVA LINCS (UID/CEC/ 04516/2013) (FCT/MEC) in the framework of the HiPsTr research project (02/SAICT/2017– 032456)",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-030-03427-6_9",
language = "English",
isbn = "978-3-030-03426-9",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "70--73",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings",

}

Lourenço, JM 2018, Verifying real-world software with contracts for concurrency. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11247 LNCS, Springer, Cham, pp. 70-73, 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03427-6_9

Verifying real-world software with contracts for concurrency. / Lourenço, João M.

Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Cham : Springer, 2018. p. 70-73 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11247 LNCS).

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

TY - GEN

T1 - Verifying real-world software with contracts for concurrency

AU - Lourenço, João M.

N1 - NOVA LINCS (UID/CEC/ 04516/2013) (FCT/MEC) in the framework of the HiPsTr research project (02/SAICT/2017– 032456)

PY - 2018/1/1

Y1 - 2018/1/1

N2 - In this paper we present Contracts for Concurrency. A contract for concurrency specifies the protocol to access the services provided by a software module or library. A program that respects a (well-defined and complete) contract for a module is safe from high-level atomicity violations with respect to that module. On the other hand, violations of a contract may denote errors in the program, and the application of contracts for concurrency to some real-world open source software packages did uncover a few latent bugs.

AB - In this paper we present Contracts for Concurrency. A contract for concurrency specifies the protocol to access the services provided by a software module or library. A program that respects a (well-defined and complete) contract for a module is safe from high-level atomicity violations with respect to that module. On the other hand, violations of a contract may denote errors in the program, and the application of contracts for concurrency to some real-world open source software packages did uncover a few latent bugs.

UR - http://www.scopus.com/inward/record.url?scp=85056462952&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-03427-6_9

DO - 10.1007/978-3-030-03427-6_9

M3 - Conference contribution

SN - 978-3-030-03426-9

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 70

EP - 73

BT - Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

CY - Cham

ER -

Lourenço JM. Verifying real-world software with contracts for concurrency. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. Cham: Springer. 2018. p. 70-73. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-03427-6_9