Invariant stream generators using automatic abstract transformers based on a decidable logic

Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli

The use of formal analysis tools on models or source code often requires the availability of auxiliary invariants about the studied system. Abstract interpretation is currently one…