Result 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.
Type
conference paper
Language
English
Authors
Malík Viktor, Ing., Ph.D.
Martiček Štefan, Ing.
Schrammel Peter
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
SRIVAS, M.
WAHLANG, J.
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.

Keywords

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

URL
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
ISBN
978-3-319-89962-6
Publisher
Springer International Publishing
Place
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"
}
Files
Projects
Bezpečné a spolehlivé počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-17-4014, start: 2017-03-01, end: 2020-02-29, completed
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, start: 2016-01-01, end: 2020-12-31, completed
ROBUST - veRificatiOn and Bug hUnting for advanced SofTware, GACR, Standardní projekty, GA17-12465S, start: 2017-01-01, end: 2019-12-31, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top