Detail výsledku

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

MALÍK, V.; MARTIČEK, Š.; SCHRAMMEL, P.; VOJNAR, T.; SRIVAS, M.; WAHLANG, J. 2LS: Memory Safety and Non-termination (Competition Contribution). In Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2. Lecture Notes in Computer Science. Thessaloniki: Springer International Publishing, 2018. p. 417-421. ISBN: 978-3-319-89962-6.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Malík Viktor, Ing., Ph.D.
Martiček Štefan, Ing.
Schrammel Peter
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
SRIVAS, M.
WAHLANG, J.
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

URL
Rok
2018
Strany
417–421
Sborník
Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2
Řada
Lecture Notes in Computer Science
Svazek
10806
Konference
European Joint Conferences on Theory and Practice of Software
ISBN
978-3-319-89962-6
Vydavatel
Springer International Publishing
Místo
Thessaloniki
DOI
10.1007/978-3-319-89963-3_24
UT WoS
000445822600024
EID Scopus
2-s2.0-85045834337
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"
}
Soubory
Projekty
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, zahájení: 2017-03-01, ukončení: 2020-02-29, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, zahájení: 2017-01-01, ukončení: 2019-12-31, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru