PV4 ⊧ 2LScan generate properties within certain conditions

2LS is a C program analyser built upon the CProver infrastructure

Application domain/field

• Assertion checking
• Invariant generation
• Bounded model checking
• Incremental k-induction
• Abstract interpretation
• Static analysis

Type of tool

Model checker?? / Program analyser

Expected input

• C program
• Optionally: Assertions in the program

Format:

.c file

Expected output

PASS, FAIL or UNKNOWN?

Internals

• The name seems to be derived from the fact that it takes program analysis problems expressed in second order logic. So, it reduces (an existential fragment of) 2nd order logic to quantifier elimination in first order logic.
• 2LS can verify array bounds (buffer overflows), pointer safety, exceptions, user-specified assertions, and (non-)termination properties.
• There are many different options to specify the kind of analyses that you want to do. Some analyses that it supports include: bounded model checking, k-induction, non-termination analysis and function-modular termination analysis.