Newer
Older
Andre Maroneze
committed
---
layout: plugin
title: Pilat
description: Loop numeric invariant generator
key: specifications
distrib_mode: free
repo_url: https://github.com/Stevendeo/Pilat
---
## Overview
[Pilat](https://en.wikipedia.org/wiki/Mont_Pilat),
the Polynomial Invariant through Linear Algebra Tool, is a plug-in
for generating (polynomial) numerical invariants over the loops of the
program. Note that it is currently restricted to arithmetic variables.
## Usage
Pilat is available as an external open-source
[plug-in]({{page.repo_url}}). Once installed,
it is enabled with the `-pilat` option, which will try to generate
all polynomial invariants that may exist in the loops of the program.
Pilat finds all invariants that exist up to a certain degree. By default,
this degree is 2, but this can modified with `-pilat-degree n`.