Skip to main content
Conference ProceedingsOPEN ACCESS

2LS for program analysis

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2016) 9636 905-907
DOI: 10.1007/978-3-662-49674-9_56
25Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

This article is free to access.

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.

Cite

CITATION STYLE

APA

Schrammel, P., & Kroening, D. (2016). 2LS for program analysis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 905–907). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_56

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free