Proving safety properties of infinite state systems by compilation into Presburger arithmetic

DOI10.1007/3-540-63141-0_15zbMath1512.68167MaRDI QIDQ6044119

Hans Olsén, Laurent Fribourg

Publication date: 17 May 2023

Published in: CONCUR '97: Concurrency Theory (Search for Journal in Brave)

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (9)

Equivalence between model-checking flat counter systems and Presburger arithmetic ⋮ Well-abstracted transition systems: Application to FIFO automata. ⋮ Applying abstract acceleration to (co-)reachability analysis of reactive programs ⋮ Tarski’s Influence on Computer Science ⋮ Counting the solutions of Presburger equations without enumerating them. ⋮ Unnamed Item ⋮ A Modular Static Analysis Approach to Affine Loop Invariants Detection ⋮ Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs ⋮ Flat Petri nets (invited talk)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the regularity of Petri net languages
• Parallel program schemata
• Composition/décomposition de réseaux de Pétri et de leurs graphes de couverture
• Reduced state space representation for unbounded vector state spaces
• Diophantine equations, Presburger arithmetic and finite automata

This page was built for publication: Proving safety properties of infinite state systems by compilation into Presburger arithmetic