2LS: Arrays and Loop Unwinding (Competition Contribution)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F23%3APU150475" target="_blank" >RIV/00216305:26230/23:PU150475 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/content/pdf/10.1007/978-3-031-30820-8_31.pdf?pdf=inline%20link" target="_blank" >https://link.springer.com/content/pdf/10.1007/978-3-031-30820-8_31.pdf?pdf=inline%20link</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-30820-8_31" target="_blank" >10.1007/978-3-031-30820-8_31</a>

Jazyk výsledku

angličtina

Název v původním jazyce

2LS: Arrays and Loop Unwinding (Competition Contribution)

Popis výsledku v původním jazyce

2LS is a C program analyser built upon the CPROVER infrastructure that can verify and refute program assertions, memory safety, and termination. Until now, one of the main drawbacks of 2LS was its inability to verify most programs with arrays. This paper introduces a new abstract domain in 2LS for reasoning about the contents of arrays. In addition, we introduce an improved approach to loop unwinding, a crucial component of the 2LS' verification algorithm, which particularly enables finding proofs and counterexamples for programs working with dynamic memory.

Název v anglickém jazyce

2LS: Arrays and Loop Unwinding (Competition Contribution)

Popis výsledku anglicky

2LS is a C program analyser built upon the CPROVER infrastructure that can verify and refute program assertions, memory safety, and termination. Until now, one of the main drawbacks of 2LS was its inability to verify most programs with arrays. This paper introduces a new abstract domain in 2LS for reasoning about the contents of arrays. In addition, we introduce an improved approach to loop unwinding, a crucial component of the 2LS' verification algorithm, which particularly enables finding proofs and counterexamples for programs working with dynamic memory.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA23-06506S" target="_blank" >GA23-06506S: Pokročilá analýza a verifikace pro pokročilý software</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2023

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2

ISBN

978-3-031-30819-2

ISSN

—

e-ISSN

—

Počet stran výsledku

6

Strana od-do

529-534

Název nakladatele

Springer International Publishing

Místo vydání

Paris

Místo konání akce

Paris

Datum konání akce

22. 4. 2023

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—