978-3-319-89963-3.pdf (18.68 MB)
2LS: memory safety and non-termination (competition contribution)
conference contribution
posted on 2023-06-20, 14:17 authored by Viktor Malik, Štefan Marticek, Peter Schrammel, Mandayam Srivas, Tomáš Vojnar, Johanan Wahlang2LS 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
SpringerExternal DOI
Volume
10806Page range
417-421Event name
24th International Conference , TACAS 2018Event location
Thessaloniki, GreeceEvent type
conferenceEvent date
April 14-20, 2018ISBN
9783319899633Series
Lecture Notes in Computer ScienceDepartment affiliated with
- Informatics Publications
Notes
Held as part of the European Joint Conferences on Theory and Practice of SoftwareFull text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2018-05-22First Open Access (FOA) Date
2018-05-22First Compliant Deposit (FCD) Date
2018-05-19Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC