Modelling Program Verification Tools for Software Engineers

Sophie Lathouwers; Vadim Zaytsev

doi:10.1145/3550355.3552426

Modelling Program Verification Tools for Software Engineers

Sophie Lathouwers, Vadim Zaytsev

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

143 Downloads (Pure)

Abstract

In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools, and present a concise megamodel to distinguish these tools. We also present a data set of almost 400 program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links, and more. The categorisation enables software engineers to find suitable tools, investigate similar alternatives and compare them. We also identify trends for each level in our megamodel based on the categorisation. Our data set, publicly available at https://doi.org/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements.

Original language	English
Title of host publication	MODELS '22
Subtitle of host publication	Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems
Place of Publication	New York, NY, USA
Publisher	Association for Computing Machinery
Pages	98–108
Number of pages	11
ISBN (Print)	978-1-4503-9466-6
DOIs	https://doi.org/10.1145/3550355.3552426
Publication status	Published - 24 Oct 2022
Event	25th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2022 - Montreal, Canada Duration: 23 Oct 2022 → 28 Oct 2022 Conference number: 25

Conference

Conference	25th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2022
Abbreviated title	MODELS 2022
Country/Territory	Canada
City	Montreal
Period	23/10/22 → 28/10/22

Keywords

Megamodelling
Program verification
Formal methods

Access to Document

10.1145/3550355.3552426

Modelling-Program-Verification-Tools-for-Software-EngineersAccepted author version, 757 KB
ArticleFinal published version, 754 KB

Cite this

@inproceedings{882cd47daad646299a63149738e91369,

title = "Modelling Program Verification Tools for Software Engineers",

abstract = "In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools, and present a concise megamodel to distinguish these tools. We also present a data set of almost 400 program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links, and more. The categorisation enables software engineers to find suitable tools, investigate similar alternatives and compare them. We also identify trends for each level in our megamodel based on the categorisation. Our data set, publicly available at https://doi.org/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements.",

keywords = "Megamodelling, Program verification, Formal methods",

author = "Sophie Lathouwers and Vadim Zaytsev",

note = "Publisher Copyright: {\textcopyright} 2022 ACM.; 25th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2022, MODELS 2022 ; Conference date: 23-10-2022 Through 28-10-2022",

year = "2022",

month = oct,

day = "24",

doi = "10.1145/3550355.3552426",

language = "English",

isbn = "978-1-4503-9466-6",

pages = "98–108",

booktitle = "MODELS '22",

publisher = "Association for Computing Machinery",

address = "United States",

}

Lathouwers, S & Zaytsev, V 2022, Modelling Program Verification Tools for Software Engineers. in MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems. Association for Computing Machinery, New York, NY, USA, pp. 98–108, 25th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2022, Montreal, Canada, 23/10/22. https://doi.org/10.1145/3550355.3552426

Modelling Program Verification Tools for Software Engineers. / Lathouwers, Sophie; Zaytsev, Vadim.
MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems. New York, NY, USA: Association for Computing Machinery, 2022. p. 98–108.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Modelling Program Verification Tools for Software Engineers

AU - Lathouwers, Sophie

AU - Zaytsev, Vadim

N1 - Conference code: 25

PY - 2022/10/24

Y1 - 2022/10/24

N2 - In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools, and present a concise megamodel to distinguish these tools. We also present a data set of almost 400 program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links, and more. The categorisation enables software engineers to find suitable tools, investigate similar alternatives and compare them. We also identify trends for each level in our megamodel based on the categorisation. Our data set, publicly available at https://doi.org/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements.

AB - In software engineering, models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the domain of program verification tools, and present a concise megamodel to distinguish these tools. We also present a data set of almost 400 program verification tools. This data set includes the category of verification tool according to our megamodel, practical information such as input/output format, repository links, and more. The categorisation enables software engineers to find suitable tools, investigate similar alternatives and compare them. We also identify trends for each level in our megamodel based on the categorisation. Our data set, publicly available at https://doi.org/10.4121/20347950, can be used by software engineers to enter the world of program verification and find a verification tool based on their requirements.

KW - Megamodelling

KW - Program verification

KW - Formal methods

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

U2 - 10.1145/3550355.3552426

DO - 10.1145/3550355.3552426

M3 - Conference contribution

SN - 978-1-4503-9466-6

SP - 98

EP - 108

BT - MODELS '22

PB - Association for Computing Machinery

CY - New York, NY, USA

T2 - 25th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2022

Y2 - 23 October 2022 through 28 October 2022

ER -

Modelling Program Verification Tools for Software Engineers

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

ProVerB: Dataset of Tools and Formats for Program Verification

Cite this

Modelling Program Verification Tools for Software Engineers

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Datasets

ProVerB: Dataset of Tools and Formats for Program Verification

Cite this