Séminaire APR
Verification of embedded C software using static analysis by abstract interpretation
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