Publication result detail

2LS: Arrays and Loop Unwinding (Competition Contribution)

MALÍK, V.; NEČAS, F.; SCHRAMMEL, P.; VOJNAR, T.

Original Title

2LS: Arrays and Loop Unwinding (Competition Contribution)

English Title

2LS: Arrays and Loop Unwinding (Competition Contribution)

Type

Paper in proceedings (conference paper)

Original Abstract

2LS is a C program analyser built upon the CPROVER infrastructure that can verify and refute program assertions, memory safety, and termination. Until now, one of the main drawbacks of 2LS was its inability to verify most programs with arrays. This paper introduces a new abstract domain in 2LS for reasoning about the contents of arrays. In addition, we introduce an improved approach to loop unwinding, a crucial component of the 2LS' verification algorithm, which particularly enables finding proofs and counterexamples for programs working with dynamic memory.

English abstract

2LS is a C program analyser built upon the CPROVER infrastructure that can verify and refute program assertions, memory safety, and termination. Until now, one of the main drawbacks of 2LS was its inability to verify most programs with arrays. This paper introduces a new abstract domain in 2LS for reasoning about the contents of arrays. In addition, we introduce an improved approach to loop unwinding, a crucial component of the 2LS' verification algorithm, which particularly enables finding proofs and counterexamples for programs working with dynamic memory.

Keywords

program analysis, formal verification, invariant inference, loop invariants, abstract interpretation, k-induction, loop unwinding, array abstract domain, array contents analysis

Key words in English

program analysis, formal verification, invariant inference, loop invariants, abstract interpretation, k-induction, loop unwinding, array abstract domain, array contents analysis

Authors

MALÍK, V.; NEČAS, F.; SCHRAMMEL, P.; VOJNAR, T.

RIV year

2024

Released

20.04.2023

Publisher

Springer International Publishing

Location

Paris

ISBN

978-3-031-30819-2

Book

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

Edition

Lecture Notes in Computer Science

Volume

13994

Pages from

529

Pages to

534

Pages count

6

URL

https://link.springer.com/content/pdf/10.1007/978-3-031-30820-8_31.pdf?pdf=inline%20link

BibTex

@inproceedings{BUT187453,
  author="MALÍK, V. and NEČAS, F. and SCHRAMMEL, P. and VOJNAR, T.",
  title="2LS: Arrays and Loop Unwinding (Competition Contribution)",
  booktitle="Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2",
  year="2023",
  series="Lecture Notes in Computer Science",
  volume="13994",
  pages="529--534",
  publisher="Springer International Publishing",
  address="Paris",
  doi="10.1007/978-3-031-30820-8\{_}31",
  isbn="978-3-031-30819-2",
  url="https://link.springer.com/content/pdf/10.1007/978-3-031-30820-8_31.pdf?pdf=inline%20link"
}