University of Sussex
Browse
978-3-319-89963-3.pdf (18.68 MB)

2LS: memory safety and non-termination (competition contribution)

Download (18.68 MB)
conference contribution
posted on 2023-06-20, 14:17 authored by Viktor Malik, Štefan Marticek, Peter Schrammel, Mandayam Srivas, Tomáš Vojnar, Johanan Wahlang
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 year's version are improved handling of heap-allocated data structures using a template domain for shape analysis and two approaches to prove program non-termination.

History

Publication status

  • Published

File Version

  • Published version

Journal

Tools and Algorithms for the Construction and Analysis of Systems (TACAS)

Publisher

Springer

Volume

10806

Page range

417-421

Event name

24th International Conference , TACAS 2018

Event location

Thessaloniki, Greece

Event type

conference

Event date

April 14-20, 2018

ISBN

9783319899633

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Notes

Held as part of the European Joint Conferences on Theory and Practice of Software

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2018-05-22

First Open Access (FOA) Date

2018-05-22

First Compliant Deposit (FCD) Date

2018-05-19

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC