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., DITS (FIT)
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