Malik, Viktor, Martiček, Štefan, Schrammel, Peter, Srivas, Mandayam, Vojnar, Tomáš and Wahlang, Johanan (2018) 2LS: memory safety and non-termination (competition contribution). 24th International Conference , TACAS 2018, Thessaloniki, Greece, April 14-20, 2018. Published in: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 10806 417-421. Springer ISBN 9783319899633
![]() |
PDF
- Published Version
Available under License Creative Commons Attribution. Download (216kB) |
![]() |
PDF
- Accepted Version
Restricted to SRO admin only Download (149kB) |
Abstract
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.
Item Type: | Conference Proceedings |
---|---|
Additional Information: | Held as part of the European Joint Conferences on Theory and Practice of Software |
Keywords: | software verification, shape analysis, termination, memory safety |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Subjects: | Q Science > QA Mathematics > QA0075 Electronic computers. Computer science |
Related URLs: | |
Depositing User: | Peter Schrammel |
Date Deposited: | 22 May 2018 09:18 |
Last Modified: | 23 May 2018 08:06 |
URI: | http://srodev.sussex.ac.uk/id/eprint/75981 |
View download statistics for this item
📧 Request an update