Analysis of Source Code Using UPPAAL

Mitja  Kulczynski; Axel Legay; Dirk Nowotka; Danny Bøgsted Poulsen

doi:10.4204/EPTCS.338.5

Analysis of Source Code Using UPPAAL

Mitja Kulczynski, Axel Legay, Dirk Nowotka, Danny Bøgsted Poulsen

Research output: Contribution to journal › Conference article in Journal › Research › peer-review

2 Citations (Scopus)

47 Downloads (Pure)

Abstract

In recent years there has been a considerable effort in optimising formal methods for application to code. This has been driven by tools such as CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been massively expanding the realm of more traditional model checking technologies to include strategy synthesis algorithms - an aspect becoming more and more needed as software becomes increasingly parallel. Instead of reimplementing the advances made by Uppaal in this area, we suggest in this paper to develop a bridge between the source code and the engine of Uppaal. Our approach uses the widespread intermediate language LLVM and makes recent advances of the Uppaal ecosystem readily available to analysis of source code.

Original language	English
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	338
Pages (from-to)	31-38
Number of pages	8
ISSN	2075-2180
DOIs	https://doi.org/10.4204/EPTCS.338.5
Publication status	Published - 2021
Event	6th Workshop on Formal Integrated Development Environment - Duration: 24 May 2021 → 25 May 2021 https://cister-labs.pt/f-ide2021/

Workshop

Workshop	6th Workshop on Formal Integrated Development Environment
Period	24/05/2021 → 25/05/2021
Internet address	https://cister-labs.pt/f-ide2021/

Access to Document

10.4204/EPTCS.338.5Licence: CC BY 4.0

Open Access articleFinal published version, 218 KBLicence: CC BY 4.0

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@inproceedings{9823b7c7d6144585aff7dc25b5b5cc7b,

title = "Analysis of Source Code Using UPPAAL",

abstract = "In recent years there has been a considerable effort in optimising formal methods for application to code. This has been driven by tools such as CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been massively expanding the realm of more traditional model checking technologies to include strategy synthesis algorithms - an aspect becoming more and more needed as software becomes increasingly parallel. Instead of reimplementing the advances made by Uppaal in this area, we suggest in this paper to develop a bridge between the source code and the engine of Uppaal. Our approach uses the widespread intermediate language LLVM and makes recent advances of the Uppaal ecosystem readily available to analysis of source code.",

author = "Mitja Kulczynski and Axel Legay and Dirk Nowotka and Poulsen, {Danny B{\o}gsted}",

year = "2021",

doi = "10.4204/EPTCS.338.5",

language = "English",

volume = "338",

pages = "31--38",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

note = "6th Workshop on Formal Integrated Development Environment ; Conference date: 24-05-2021 Through 25-05-2021",

url = "https://cister-labs.pt/f-ide2021/",

}

TY - GEN

T1 - Analysis of Source Code Using UPPAAL

AU - Kulczynski, Mitja

AU - Legay, Axel

AU - Nowotka, Dirk

AU - Poulsen, Danny Bøgsted

PY - 2021

Y1 - 2021

N2 - In recent years there has been a considerable effort in optimising formal methods for application to code. This has been driven by tools such as CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been massively expanding the realm of more traditional model checking technologies to include strategy synthesis algorithms - an aspect becoming more and more needed as software becomes increasingly parallel. Instead of reimplementing the advances made by Uppaal in this area, we suggest in this paper to develop a bridge between the source code and the engine of Uppaal. Our approach uses the widespread intermediate language LLVM and makes recent advances of the Uppaal ecosystem readily available to analysis of source code.

AB - In recent years there has been a considerable effort in optimising formal methods for application to code. This has been driven by tools such as CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been massively expanding the realm of more traditional model checking technologies to include strategy synthesis algorithms - an aspect becoming more and more needed as software becomes increasingly parallel. Instead of reimplementing the advances made by Uppaal in this area, we suggest in this paper to develop a bridge between the source code and the engine of Uppaal. Our approach uses the widespread intermediate language LLVM and makes recent advances of the Uppaal ecosystem readily available to analysis of source code.

U2 - 10.4204/EPTCS.338.5

DO - 10.4204/EPTCS.338.5

M3 - Conference article in Journal

SN - 2075-2180

VL - 338

SP - 31

EP - 38

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 6th Workshop on Formal Integrated Development Environment

Y2 - 24 May 2021 through 25 May 2021

ER -

Analysis of Source Code Using UPPAAL

Abstract

Workshop

Access to Document

AUB Link

Fingerprint

Cite this