2LS ("tools") is a verification tool for C programs. It is built upon the CPROVER framework (cprover.org), which supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio. It allows verifying array bounds (buffer overflows), pointer safety, exceptions, user-specified assertions, and termination properties. The analysis is performed by template-based predicate synthesis and abstraction refinements techniques.
4-clause BSD license, see LICENSE file.
2LS reduces program analysis problems expressed in second order logic such as invariant or ranking function inference to synthesis problems over templates. Hence, it reduces (an existential fragment of) 2nd order Logic Solving to quantifier elimination in first order logic.
The current tool has following capabilities:
- function-modular interprocedural analysis of C code based on summaries
- summary and invariant inference using generic templates
- combined k-induction and invariant inference
- incremental bounded model checking
- function-modular termination analysis
- non-termination analysis
Download using git clone https://github.com/diffblue/2ls; cd 2ls; git checkout 2ls-x.y
- 2LS 0.10 (01/2023)
- 2LS 0.9 (03/2020)
- 2LS 0.8 (11/2019)
- 2LS 0.7 (08/2018)
- 2LS 0.6 (12/2017)
- 2LS 0.5 (01/2017)
- 2LS 0.4 (08/2016)
- 2LS 0.3 (08/2015)
- 2LS 0.2 (06/2015)
- 2LS 0.1 (11/2014)
Software Verification Competition Contributions
- SV-COMP 2023 (01/2023)
- SV-COMP 2022 (01/2022)
- SV-COMP 2021 (12/2020)
- SV-COMP 2020 (03/2020)
- SV-COMP 2019 (12/2018)
- SV-COMP 2018 (12/2017)
- SV-COMP 2017 (01/2017)
- SV-COMP 2016 (11/2015) Follow these instructions
cd 2ls; ./install.sh
Run src/2ls/2ls
The default abstract domain are intervals. If no options are given a context-insensitive interprocedural analysis is performed. For context-sensitivity, add --context-sensitive.
Other analyses include:
- BMC: --inline --havoc --unwind n
- Incremental BMC: --incremental-bmc
- Incremental k-induction: --havoc --k-induction
- Incremental k-induction and k-invariants (kIkI): --k-induction
- Intraprocedural abstract interpretation with property checks: --inline
- Necessary preconditions: --preconditions
- Sufficient preconditions: --preconditions --sufficient
Currently the following abstract domains are available:
- Intervals (default): --intervals
- Zones: --zones
- Octagons --octagons
- Equalities/disequalities: --equalities
- The abstract domain consisting of the Top element: --havoc
Since release 0.6:
- Heap abstract domain: --heap
Since release 0.7:
- Heap abstract domain with intervals or zones: --heap-[intervals|zones]
- Heap abstract domain with intervals or zones and loop paths: --heap-[intervals|zones] --sympath
Since release 0.10:
- Array abstract domain: --arrays
Is supported by release 0.1 and >=0.3.
- Universal termination: --termination
- Context-sensitive universal termination: --termination --context-sensitive
- Sufficient preconditions for termination --termination --context-sensitive --preconditions
Since release 0.6:
- Nontermination analysis: --non-termination
- ACDL solver (ATVA'17 Lifting CDCL to Template-Based Abstract Domains for Program Verification)
- array domain
- disjunctive domains
- custom template specifications
- modular refinement
- template refinement
- thread-modular analysis
- FMCAD'18 Template-Based Verification of Heap-Manipulating Programs
- TACAS'18 2LS: Memory Safety and Non-Termination
- TOPLAS 40(1) 2018 Bit-Precise Procedure-Modular Termination Analysis
- ATVA'17 Compositional Refutation Techniques
- ATVA'17 Lifting CDCL to Template-Based Abstract Domains for Program Verification
- TACAS'16 2LS for Program Analysis
- SAS'15 Safety Verification and Refutation by k-Invariants and k-Induction
- ASE'15 Synthesising Interprocedural Bit-Precise Termination Proofs Experimental log Additional material Website
- Björn Wachter
- Cristina David
- Daniel Kroening
- Frantisek Necas
- Hongyi Chen
- Madhukar Kumar
- Martin Brain
- Martin Hruska
- Peter Schrammel
- Rajdeep Mukherjee
- Samuel Bücheli
- Saurabh Joshi
- Stefan Marticek
- Viktor Malik