User Tools

Site Tools


2ls_for_program_analysis

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
2ls_for_program_analysis [2017/07/15 12:15]
kroening
2ls_for_program_analysis [2017/11/04 17:38] (current)
schram
Line 1: Line 1:
 ====== 2LS for Program Analysis ====== ====== 2LS for Program Analysis ======
  
-2LS ("​tools"​) for program analysis is a CPROVER-based framework. +**[[https://www.github.com/​diffblue/​2ls|2LS is now on github!!!]]**
- +
-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) **2**nd order **L**ogic **S**olving 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 ===== +
- +
-Download using ''​%%git clone http://github.com/​diffblue/​2ls;​ cd 2ls; git checkout 2ls-%%''​x.y +
- +
-  * ''​http://​github.com/​diffblue/​2ls/​releases/​tag/​2ls-0.5''​ (01/2017) +
-  * ''​http://​github.com/​diffblue/​2ls/​releases/​tag/​2ls-0.4''​ (08/2016) +
-  * ''​http://​svn.cprover.org/​svn/​deltacheck/​releases/​2ls-0.3''​ (08/2015) +
-  * ''​http://​svn.cprover.org/​svn/​deltacheck/​releases/​2ls-0.2''​ (06/2015) +
-  * ''​http://​svn.cprover.org/​svn/​deltacheck/​releases/​2ls-0.1''​ (11/2014) +
- +
-=== Software Verification Competition Contributions === +
-  * ''​http://​github.com/​diffblue/​2ls/​releases/​tag/​2ls-0.5-sv-comp-2017''​ (01/2017)  +
-  * ''​http://​svn.cprover.org/​svn/​deltacheck/​releases/​2ls-0.3-sv-comp-2016''​ (11/2015) [[http://​www.cprover.org/​2LS/​2ls-sv-comp-2016.pdf|Follow these instructions]]. +
- +
- +
-===== 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 ===== +
- +
-  * TACAS'​16 [[http://​dl.acm.org/​citation.cfm?​id=2945506|2LS for Program Analysis]] +
-  ​SAS'15 [[http://​link.springer.com/​chapter/​10.1007%2F978-3-662-48288-9_9|Safety Verification and Refutation by k-Invariants and k-Induction]] +
-  ​ASE'15 [[http://​dl.acm.org/​citation.cfm?​id=2916211|Synthesising Interprocedural Bit-Precise Termination Proofs]] [[http://​www.cs.ox.ac.uk/​people/​peter.schrammel/​2ls/​ase15-experimental_results_log.txt|Experimental log]][[http://​www.cs.ox.ac.uk/​people/​peter.schrammel/​2ls/​ase15-additional-material.tgz|Additional material]][[http://​www.cprover.org/​termination/​modular|Website]] +
- +
- +
-===== 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/11/04 17:38 by schram