Extract, model, refine: improved modelling of program verification tools through data enrichment.
Saved in:
| Title: | Extract, model, refine: improved modelling of program verification tools through data enrichment. |
|---|---|
| Authors: | Lathouwers, Sophie1 (AUTHOR) sophie.lathouwers@gmail.com, Liu, Yujie1 (AUTHOR) yujie.liu.public@gmail.com, Zaytsev, Vadim1 (AUTHOR) vadim@grammarware.net |
| Source: | Software & Systems Modeling. Aug2025, Vol. 24 Issue 4, p1293-1313. 21p. |
| Subjects: | Software verification, Software engineering, Statistical reliability, Software development tools, Software frameworks, Automation software, Information storage & retrieval systems, Acquisition of data |
| 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 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 practical information, such as last commit date, is kept up to date through the use of APIs. Moreover, part of the data extraction has been automated to make it easier to expand the data set. The categorisation enables software engineers to find suitable tools, investigate alternatives and compare tools. We also identify trends for each level in our megamodel. 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. This paper is an extended version of https://doi.org/10.1145/3550355.3552426. [ABSTRACT FROM AUTHOR] |
| Copyright of Software & Systems Modeling is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
|
Full text is not displayed to guests.
Login for full access.
|
|
| FullText | Links: – Type: pdflink Text: Availability: 1 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 186986136 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Extract, model, refine: improved modelling of program verification tools through data enrichment. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Lathouwers%2C+Sophie%22">Lathouwers, Sophie</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> sophie.lathouwers@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Liu%2C+Yujie%22">Liu, Yujie</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> yujie.liu.public@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Zaytsev%2C+Vadim%22">Zaytsev, Vadim</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> vadim@grammarware.net</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Software+%26+Systems+Modeling%22">Software & Systems Modeling</searchLink>. Aug2025, Vol. 24 Issue 4, p1293-1313. 21p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Software+engineering%22">Software engineering</searchLink><br /><searchLink fieldCode="DE" term="%22Statistical+reliability%22">Statistical reliability</searchLink><br /><searchLink fieldCode="DE" term="%22Software+development+tools%22">Software development tools</searchLink><br /><searchLink fieldCode="DE" term="%22Software+frameworks%22">Software frameworks</searchLink><br /><searchLink fieldCode="DE" term="%22Automation+software%22">Automation software</searchLink><br /><searchLink fieldCode="DE" term="%22Information+storage+%26+retrieval+systems%22">Information storage & retrieval systems</searchLink><br /><searchLink fieldCode="DE" term="%22Acquisition+of+data%22">Acquisition of data</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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 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 practical information, such as last commit date, is kept up to date through the use of APIs. Moreover, part of the data extraction has been automated to make it easier to expand the data set. The categorisation enables software engineers to find suitable tools, investigate alternatives and compare tools. We also identify trends for each level in our megamodel. 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. This paper is an extended version of https://doi.org/10.1145/3550355.3552426. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Software & Systems Modeling is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=186986136 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10270-024-01232-7 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 21 StartPage: 1293 Subjects: – SubjectFull: Software verification Type: general – SubjectFull: Software engineering Type: general – SubjectFull: Statistical reliability Type: general – SubjectFull: Software development tools Type: general – SubjectFull: Software frameworks Type: general – SubjectFull: Automation software Type: general – SubjectFull: Information storage & retrieval systems Type: general – SubjectFull: Acquisition of data Type: general Titles: – TitleFull: Extract, model, refine: improved modelling of program verification tools through data enrichment. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Lathouwers, Sophie – PersonEntity: Name: NameFull: Liu, Yujie – PersonEntity: Name: NameFull: Zaytsev, Vadim IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 08 Text: Aug2025 Type: published Y: 2025 Identifiers: – Type: issn-print Value: 16191366 Numbering: – Type: volume Value: 24 – Type: issue Value: 4 Titles: – TitleFull: Software & Systems Modeling Type: main |
| ResultId | 1 |
