2LS: Memory Safety and Non-termination (Competition Contribution)

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F18%3APU130811" target="_blank" >RIV/00216305:26230/18:PU130811 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-319-89963-3_24" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-319-89963-3_24</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-89963-3_24" target="_blank" >10.1007/978-3-319-89963-3_24</a>

Jazyk výsledku

angličtina

Název v původním jazyce

2LS: Memory Safety and Non-termination (Competition Contribution)

Popis výsledku v původním jazyce

2LS is a C program analyser built upon the CPROVER infrastructure. 2LS is bit-precise and it can verify and refute program assertions and termination. 2LS implements template-based synthesis techniques, e.g. to find invariants and ranking functions, and incremental loop unwinding techniques to find counterexamples and k-induction proofs. New features in this years version are improved handling of heap-allocated data structures using a template domain for shape analysis and two approaches to prove program non-termination.

Název v anglickém jazyce

2LS: Memory Safety and Non-termination (Competition Contribution)

Popis výsledku anglicky

2LS is a C program analyser built upon the CPROVER infrastructure. 2LS is bit-precise and it can verify and refute program assertions and termination. 2LS implements template-based synthesis techniques, e.g. to find invariants and ranking functions, and incremental loop unwinding techniques to find counterexamples and k-induction proofs. New features in this years version are improved handling of heap-allocated data structures using a template domain for shape analysis and two approaches to prove program non-termination.

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

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

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

Rok uplatnění

2018

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 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2

ISBN

978-3-319-89962-6

ISSN

—

e-ISSN

—

Počet stran výsledku

5

Strana od-do

417-421

Název nakladatele

Springer International Publishing

Místo vydání

Thessaloniki

Místo konání akce

Thessaloniki

Datum konání akce

14. 4. 2018

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

WRD - Celosvětová akce

Kód UT WoS článku

000445822600024