PV0 ⊧ LEGION

Application domain/field

• Model checking
• Bounded model checking
• Sequential programs
• Termination

Type of tool

Bounded model checker

Expected input

Program (with an entry-point procedure called main) Property? (unclear, possibly assertions in the program)

Format:

Boogie program

Expected output

Whether the program is safe, unsafe (with counterexample trace) or undecided

Internals

The verification question that they focus on is whether there exists a terminating execution of P. In other words, whether there is any execution of main that reaches its return statement. If no such execution exists, then the program is considered safe. They require the program to not contain any loops or recursive procedure calls. Such calls must be unrolled to a pre-determined depth before starting verification. Uses Z3 to solve SMT queries.