Publication Details

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

MALÍK Viktor, MARTIČEK Štefan, SCHRAMMEL Peter, SRIVAS Mandayam, VOJNAR Tomáš and WAHLANG Johanan. 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, vol. 10806. Thessaloniki: Springer International Publishing, 2018, pp. 417-421. ISBN 978-3-319-89962-6. Available from: https://link.springer.com/chapter/10.1007/978-3-319-89963-3_24
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. (DITS FIT BUT)
Martiček Štefan, Ing. (FIT BUT)
Schrammel Peter, Dr. (US)
Srivas Mandayam (CMI)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Wahlang Johanan (CMI)
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
Conference
European Joint Conferences on Theory and Practice of Software, Thessaloniki, GR
ISBN
978-3-319-89962-6
Publisher
Springer International Publishing
Place
Thessaloniki, GR
DOI
10.1007/978-3-319-89963-3_24
UT WoS
000445822600024
EID Scopus
2-s2.0-85045834337
BibTeX 
@INPROCEEDINGS{FITPUB11892,
   author = "Viktor Mal\'{i}k and \v{S}tefan Marti\v{c}ek and Peter Schrammel and Mandayam Srivas and Tom\'{a}\v{s} Vojnar and Johanan Wahlang",
   title = "2LS: Memory Safety and Non-termination (Competition Contribution)",
   pages = "417--421",
   booktitle = "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,
   year = 2018,
   location = "Thessaloniki, GR",
   publisher = "Springer International Publishing",
   ISBN = "978-3-319-89962-6",
   doi = "10.1007/978-3-319-89963-3\_24",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11892"
}
Back to top