LIP6 CNRS Sorbonne Université Tremplin Carnot Interfaces
Direct Link LIP6 » Links » Das LIP6 organisiert

Séminaire APRRSS

Verification of embedded C software using static analysis by abstract interpretation


13.03.2015
Beteiligte : Antoine Miné
Sound static analysis by abstract interpretation is becoming a popular method to validate software. The Astrée project has shown that, by carefully designing specialized abstractions, a fully automated proof of absence of run-time error on selected classes of critical software becomes possible. This talk will discuss the foundational and practical aspects of designing the Astrée analyzer. The talk will also present on-going work on AstréeA, an extension of Astrée that targets concurrent embedded C software and uses thread-modular analyses to scale up to million-lines programs.
romain.demangeon (at) nulllip6.fr
 Mentions légales
Plan |