PV2 POROUSgenerates invariants for given affine functions

Invariant-synthesis tool It computes -semi-linear invariants for points and -linear targets on systems defined by one-dimensional affine functions.

Application domain/field

Type of tool

Invariant synthesizer

Expected input

Format:

Own format, described in the repository

Expected output

Generated invariant (union of -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

Links

Last commit date

25 August 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_8 (CAV '21)

Last publication date

15 July 2021

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.