Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
MALÍK, V. MARTIČEK, Š. SCHRAMMEL, P. VOJNAR, T. SRIVAS, M. WAHLANG, J.
Originální název
2LS: Memory Safety and Non-termination (Competition Contribution)
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
verification, termination, non-termination, shape analysis, invariant synthesis
Autoři
MALÍK, V.; MARTIČEK, Š.; SCHRAMMEL, P.; VOJNAR, T.; SRIVAS, M.; WAHLANG, J.
Vydáno
14. 4. 2018
Nakladatel
Springer International Publishing
Místo
Thessaloniki
ISBN
978-3-319-89962-6
Kniha
Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2
Edice
Lecture Notes in Computer Science
Strany od
417
Strany do
421
Strany počet
5
URL
https://link.springer.com/chapter/10.1007/978-3-319-89963-3_24
BibTex
@inproceedings{BUT155119, author="MALÍK, V. and MARTIČEK, Š. and SCHRAMMEL, P. and VOJNAR, T. and SRIVAS, M. and WAHLANG, J.", title="2LS: Memory Safety and Non-termination (Competition Contribution)", booktitle="Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2", year="2018", series="Lecture Notes in Computer Science", volume="10806", pages="417--421", publisher="Springer International Publishing", address="Thessaloniki", doi="10.1007/978-3-319-89963-3\{_}24", isbn="978-3-319-89962-6", url="https://link.springer.com/chapter/10.1007/978-3-319-89963-3_24" }