PV4 ⊧ Ultimate Automizerchecks user-specified properties and some built-in properties, e.g. memory safety, of a C program for a specified architecture

Ultimate Automizer is a software verifier that implements an automata-based approach for the verification of safety and liveness properties

Application domain/field

• Abstraction refinement
• Counterexample Guided Abstraction Refinement (CEGAR)
• Model checking
• Software model checking

Type of tool

Model checker

Expected input

• C program
• Specification file
• Architecture
• Optional: Witness file for witness validation

Format:

• Program: .c file
• Specification file: .prp file, SV-COMP format
• Architecture: 32bit or 64bit passed as an argument
• Optional witness file: .graphml file containing a violation or correctness witness

Expected output

Whether the property holds or not. It may generate a violation or correctness witness to witness.graphml.

Internals

Ultimate Automizer can analyse the reachability of error functions, memory safety, absence of overflows and termination. Built on top of Ultimate, a program analysis framework. Uses Z3, CVC4, MathSAT

Comments

License information: https://github.com/ultimate-pa/ultimate/wiki/License