Publication detail

2LS: Heap Analysis and Memory Safety (Competition Contribution)

MALÍK, V. SCHRAMMEL, P. VOJNAR, T.

Original Title

2LS: Heap Analysis and Memory Safety (Competition Contribution)

Type

conference paper

Language

English

Original Abstract

2LS is a framework for analysis of sequential C programs based on the CPROVER infrastructure and template-based synthesis techniques for checking both safety and termination. The paper presents the main improvements done in 2LS since 2018, which concern mainly the way 2LS handles dynamically allocated objects and structures as well as combinations of abstract domains.

Keywords

software verification, bounded model checking, abstract interpretation, shape analysis, value analysis

Authors

MALÍK, V.; SCHRAMMEL, P.; VOJNAR, T.

Released

17. 4. 2020

Publisher

Springer International Publishing

Location

Dublin

ISBN

978-3-030-45236-0

Book

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

Edition

Lecture Notes in Computer Science

Pages from

368

Pages to

372

Pages count

5

URL

https://link.springer.com/chapter/10.1007%2F978-3-030-45237-7_22

BibTex

@inproceedings{BUT168128,
  author="Viktor {Malík} and Peter {Schrammel} and Tomáš {Vojnar}",
  title="2LS: Heap Analysis and Memory Safety (Competition Contribution)",
  booktitle="Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2",
  year="2020",
  series="Lecture Notes in Computer Science",
  volume="12079",
  pages="368--372",
  publisher="Springer International Publishing",
  address="Dublin",
  doi="10.1007/978-3-030-45237-7\{_}22",
  isbn="978-3-030-45236-0",
  url="https://link.springer.com/chapter/10.1007%2F978-3-030-45237-7_22"
}