Publication Details

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.
Czech title
2LS: analýza bezpečnosti práce s pamětí a neukončitelnosti (příspěvek do soutěže)
Type
conference paper
Language
English
Authors
Malík Viktor, Ing., Ph.D. (DITS)
Martiček Štefan, Ing.
Schrammel Peter
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
SRIVAS, M.
WAHLANG, J.
URL
Keywords

verification, termination, non-termination, shape analysis, invariant synthesis

Abstract

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.

Published
2018
Pages
417–421
Proceedings
Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2
Series
Lecture Notes in Computer Science
Volume
10806
ISBN
978-3-319-89962-6
Publisher
Springer International Publishing
Place
Thessaloniki
DOI
UT WoS
000445822600024
EID Scopus
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"
}
Files
Back to top