Automated Verification of Go Programs via Bounded Model Checking. / Dilley, Nicolas; Lange, Julien.

In: IEEE/ACM International Conference on Automated Software Engineering, 08.07.2021.

Research output: Contribution to journalConference articlepeer-review

Forthcoming

Standard

Automated Verification of Go Programs via Bounded Model Checking. / Dilley, Nicolas; Lange, Julien.

In: IEEE/ACM International Conference on Automated Software Engineering, 08.07.2021.

Research output: Contribution to journalConference articlepeer-review

Harvard

Dilley, N & Lange, J 2021, 'Automated Verification of Go Programs via Bounded Model Checking', IEEE/ACM International Conference on Automated Software Engineering.

APA

Dilley, N., & Lange, J. (Accepted/In press). Automated Verification of Go Programs via Bounded Model Checking. IEEE/ACM International Conference on Automated Software Engineering.

Vancouver

Dilley N, Lange J. Automated Verification of Go Programs via Bounded Model Checking. IEEE/ACM International Conference on Automated Software Engineering. 2021 Jul 8.

Author

Dilley, Nicolas ; Lange, Julien. / Automated Verification of Go Programs via Bounded Model Checking. In: IEEE/ACM International Conference on Automated Software Engineering. 2021.

BibTeX

@article{3ac5987837d04b1cb6e2329aad975360,
title = "Automated Verification of Go Programs via Bounded Model Checking",
abstract = "The Go programming language offers a wide range of primitives to coordinate lightweight threads, e.g., channels, waitgroups, and mutexes — all of which may cause concurrency bugs. Static checkers that guarantee the absence of bugs are essential to help programmers avoid these costly errors before their code is executed. However existing tools either miss too many bugs or cannot handle large programs. To address these limitations, we propose a static checker for Go programs which relies on performing bounded model checking of their concurrent behaviours. In contrast to previous works, our approach deals with large codebases, supports programs that have statically unknown parameters, and is extensible to additional concurrency primitives. Our work includes a detailed presentation of the extraction algorithm from Go programs to models, an algorithm to automatically check programs with statically unknown parameters, and a large scale evaluation of our approach. The latter shows that our approach outperforms the state-of-the-art.",
author = "Nicolas Dilley and Julien Lange",
note = "Artifact: https://github.com/nicolasdilley/gomela-ase21",
year = "2021",
month = jul,
day = "8",
language = "English",
journal = "IEEE/ACM International Conference on Automated Software Engineering",

}

RIS

TY - JOUR

T1 - Automated Verification of Go Programs via Bounded Model Checking

AU - Dilley, Nicolas

AU - Lange, Julien

N1 - Artifact: https://github.com/nicolasdilley/gomela-ase21

PY - 2021/7/8

Y1 - 2021/7/8

N2 - The Go programming language offers a wide range of primitives to coordinate lightweight threads, e.g., channels, waitgroups, and mutexes — all of which may cause concurrency bugs. Static checkers that guarantee the absence of bugs are essential to help programmers avoid these costly errors before their code is executed. However existing tools either miss too many bugs or cannot handle large programs. To address these limitations, we propose a static checker for Go programs which relies on performing bounded model checking of their concurrent behaviours. In contrast to previous works, our approach deals with large codebases, supports programs that have statically unknown parameters, and is extensible to additional concurrency primitives. Our work includes a detailed presentation of the extraction algorithm from Go programs to models, an algorithm to automatically check programs with statically unknown parameters, and a large scale evaluation of our approach. The latter shows that our approach outperforms the state-of-the-art.

AB - The Go programming language offers a wide range of primitives to coordinate lightweight threads, e.g., channels, waitgroups, and mutexes — all of which may cause concurrency bugs. Static checkers that guarantee the absence of bugs are essential to help programmers avoid these costly errors before their code is executed. However existing tools either miss too many bugs or cannot handle large programs. To address these limitations, we propose a static checker for Go programs which relies on performing bounded model checking of their concurrent behaviours. In contrast to previous works, our approach deals with large codebases, supports programs that have statically unknown parameters, and is extensible to additional concurrency primitives. Our work includes a detailed presentation of the extraction algorithm from Go programs to models, an algorithm to automatically check programs with statically unknown parameters, and a large scale evaluation of our approach. The latter shows that our approach outperforms the state-of-the-art.

M3 - Conference article

JO - IEEE/ACM International Conference on Automated Software Engineering

JF - IEEE/ACM International Conference on Automated Software Engineering

ER -