From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation

Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov

Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic a…