Detail publikace

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

MALÍK, V. MARTIČEK, Š. SCHRAMMEL, P. VOJNAR, T. SRIVAS, M. WAHLANG, J.

Originální název

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

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální 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

Autoři

MALÍK, V.; MARTIČEK, Š.; SCHRAMMEL, P.; VOJNAR, T.; SRIVAS, M.; WAHLANG, J.

Vydáno

14. 4. 2018

Nakladatel

Springer International Publishing

Místo

Thessaloniki

ISBN

978-3-319-89962-6

Kniha

Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2

Edice

Lecture Notes in Computer Science

Strany od

417

Strany do

421

Strany počet

5

URL

https://link.springer.com/chapter/10.1007/978-3-319-89963-3_24

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"
}