I worked on Arcade.PLC on two occasions: during my bachelor’s thesis, and my time as research associate at Embedded Software.
Arcade.PLC is both a tool and a framework for formal verification of industrial control software, featuring procedures for static analysis, automated test generation and model checking.
It started out as explicit state-space exploration based on abstract interpretation, which is what I’ve been integrating abstractions into during my bachelor’s thesis, but was extended with various SMT-based methods during my PhD.
In contrast to general purpose verifier backends, it is tailored to aid in the analysis of issues specific to the domain of industrial control.
For some properties, like the analysis of restart-behaviour, it even is the only tool in existence.
I was involved in parsing & compiling source code to intermediate representations, and all parts of the verification pipeline:
- preprocessing & optimisation in the front end,
- translation and formalisation of semantics in the middle end, and
- the actual analysis of formal models in the back end.