Automatically Proving Concurrent Programs Correct

of abstract interpretations in formal methods It is always very satisfying to hear about a theory, in the case at hand it is the theory of abstract interpretations, that explains it all. Even more so when the theory involves demanding mathematical concepts such as Galois connections. Patrick s the father of abstract interpretation theory and it was a pleasure to listen to his accomplished presentation. Theory alone would probably not have established his high scientific standing which is also based on the ASTREE system developed in his group. The ASTREE system is able to analyse a clearly delineated class of numerical control programs heavily using floating point computations with respect to a restricted but important set of properties via abtract interpretions. The most prominent user of ASTREE is airbus. Check the APRON website on Numerical Program Analysis http://apron.cri. ensmp.fr/. Byron Cook (MSR Cambridge) Automatically proving concurrent programs correct Byron Cook, one of t...

• Type: Conference
• Year: 2007
• Where: SEFM
• Authors: Byron Cook
• Keywords: Abstract Interpretation, ASTREE, SEFM 2007, Software Engineering, Theory