Skip to content
Static Analyzer and Verifier
C++ C Perl Makefile Shell Assembly
Branch: master
Clone or download

Latest commit

Fetching latest commit…
Cannot retrieve the latest commit at this time.

Files

Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
lib
regression
scripts
src
.gitattributes
.gitignore
.gitmodules
.travis.yml
COMPILING
LICENSE
README.md
build.sh

README.md

Build Status

About

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.

License

4-clause BSD license, see LICENSE file.

Overview

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

Releases

Download using git clone http://github.com/diffblue/2ls; cd 2ls; git checkout 2ls-x.y

Software Verification Competition Contributions

Installation

cd 2ls; ./install.sh

Run src/2ls/2ls

Command line options

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

Interprocedural Termination Analysis

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

Features in development

Publications

Contributors

  • Björn Wachter
  • Cristina David
  • Daniel Kroening
  • Hongyi Chen
  • Madhukar Kumar
  • Martin Brain
  • Martin Hruska
  • Peter Schrammel
  • Rajdeep Mukherjee
  • Samuel Bücheli
  • Saurabh Joshi
  • Stefan Marticek
  • Viktor Malik

Contact

Peter Schrammel

You can’t perform that action at this time.