POROUS.md

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.

Name:

POROUS

Application domain/field:

Inductive invariants Reachability problem Multipath affine loops Invariant synthesis

Type of tool (e.g. model checker, test generator):

Invariant synthesizer

Expected input thing:

• Start point
• Target
• Collection of functions

Expected input format:

Own format, described in the repository

Expected output:

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

Internals (tools used, frameworks, techniques, paradigms, ...):

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

Comments:

License: CC Attribution-NonCommercial-ShareAlike 4.0 International License

URIs (github, websites, etc.):

Online web interface: https://porous.mpi-sws.org/ Repository: https://github.com/davidjpurser/porous-tool

Last commit date:

28 Jan 2022 (default branch) 28 Jan 2022 (last activity)

Last publication date:

15 July 2021

List of related papers:

Porous Invariants (CAV '21)

Related tools (tools mentioned or compared to in the paper):

Meta

:: PV2 :: generates invariants for given affine functions :: Source :: https://doi.org/10.1145/3550355.3552426