< retour aux publications

Proving Parameterized Systems: the use of a widening operator and pseudo-pipelines in polyhedral logic

Auteur(s) : D. Cachera, K. Morin-Allory

ISRN: TIMA-RR--05/04-01--FR

We propose proof techniques and tools for the formal verification of regular parameterized systems. These systems are expressed in the polyhedral model, which combines affine recurrence equations with index sets of polyhedral shape. We extend a previously defined proof system based on a polyhedral logic with the detection of pseudo-pipelines, that are particular patterns in the variable definitions generalizing the notion of pipeline. The combination of pseudo-pipeline detection with the use of a simple widening operator greatly improves the effectiveness of our proof techniques.