Tool Demonstration of the FLATA Counter Automata Toolset
Marius Dorel Bozga, Radu Iosif, Filip A Konecny, Tomáš Vojnar · EPiC series in computing · 2018
We demonstrate the FLATA tool for checking reachability in counter automata using techniques which have recently been developed (such as precise acceleration of self-loops labelled by DBMs or octagons) and/or which are still under development. Apart from analysing counter automata, FLATA allows one to also reduce the given counter automata while preserving reachability of designated control locations. For demonstrating the tool, we use counter automata obtained, e.g., by translation from list manipulating programs or hardware components.