PV3 ⊧ Foresterchecks user-specified property for a C program

Application domain/field

• Shape analysis
• Forest automata (FAs)
• Model checking
• Reachability analysis
• Symbolic execution
• Heap

Type of tool

Model checker?

Expected input

• Program
• LTL properties to check
• Output file for the witness

Format:

• Program: C code
• Properties: .prp file, as used in SV-COMP
• Output file for witness: filename to which the witness will be written, passed as parameter

Expected output

TRUE, FALSE or UNKNOWN. It will also generate a violation/correctness witness as an automaton in GraphML.

Comments

License: GPLv3