PV2 ⊧ POROUSgenerates invariants for given affine functions

Invariant-synthesis tool It computes $\mathbb{N}$-semi-linear invariants for points and $\mathbb{Z}$-linear targets on systems defined by one-dimensional affine functions.

Application domain/field

• Inductive invariants
• Reachability problem
• Multipath affine loops
• Invariant synthesis

Type of tool

Invariant synthesizer

Expected input

• Start point
• Target
• Collection of functions

Format:

Own format, described in the repository

Expected output

Generated invariant (union of $\mathbb{N}$-linear sets)

Internals

Tools mentioned in the CAV '21 paper: FLATA, AProVE, Büchi Automizer

Comments

License: CC Attribution-NonCommercial-ShareAlike 4.0 International License