User Tools

Site Tools


2ls_for_program_analysis

2LS for Program Analysis

2LS (“tools”) for program analysis is a CPROVER-based framework.

It 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 set 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
  • function-modular termination analysis

Releases

Software Verification Competition Contributions

Getting started

Installation

  • cd 2ls; ./install.h
  • 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

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

Features in development

  • custom template specifications
  • ACDL solver
  • modular refinement
  • template refinement
  • thread-modular analysis

Publications

Contributors

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

Contact

Peter Schrammel

http://www.schrammel.it

2ls_for_program_analysis.txt · Last modified: 2017/01/12 21:10 by schram