PV2 ⊧ NIS (Numerical Invariant Synthesizer)synthesises inductive invariants for a SyGuS problem

Application domain/field

• Synthesis
• Invariant synthesis
• Numerical programs
• Data-driven synthesis

Type of tool

Synthesis tool

Expected input

Transition system and a property?

Format:

SyGuS language

Expected output

An inductive invariant I such that the program can be proven correct, otherwise an error.

Internals

Uses Z3 for solving SMT queries and APRON for abstract domains. Uses ICE-DT, a learning approach tailed for invariant synthesis that uses decision trees.