2LS for program analysis

Schrammel, Peter and Kroening, Daniel (2016) 2LS for program analysis. In: Tools and algorithms for the construction and analysis of systems. Lecture Notes in Computer Science, 9636 . Springer Berlin Heidelberg, Berlin, pp. 905-907. ISBN 9783662496732

[img] PDF - Accepted Version
Restricted to SRO admin only

Download (165kB)

Abstract

2LS is a program analysis tool for C programs built upon the CPROVER infrastructure. 2LS is bit-precise and it can verify and refute program assertions. 2LS implements invariant generation techniques, incremental bounded model checking and incremental k-induction. The competition submission uses an algorithm combining all three techniques, called kIkI (k-invariants and k-induction). As a back end, the competition submission of 2LS uses Glucose 4.0.

Item Type: Book Section
Additional Information: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
Keywords: 2LS, software verification, program analysis
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Q Science > QA Mathematics > QA0076 Computer software
Depositing User: Peter Schrammel
Date Deposited: 09 May 2016 11:53
Last Modified: 09 May 2016 11:53
URI: http://sro.sussex.ac.uk/id/eprint/60811

View download statistics for this item

📧 Request an update