Campus Event Calendar
Event Entry
What and Who
Static Software Analysis, in the Large
Patrick Cousot
ENS, Paris
SWS Distinguished Lecture Series - Spring
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 26 August 2008
16:00
60 Minutes
E1 5
019
Saarbrücken
Abstract
Static software analysis has known brilliant successes in the small,
by proving complex program properties of programs of a few dozen or
hundreds of
lines, either by systematic exploration of the state space or by
interactive
deductive methods. To scale up is a definite problem. Very few static
analyzers are able to scale up to millions of lines without sacrificing
soundness and/or precision. Unsound static analysis may be useful for
bug finding but is less useless in safety critical applications where the
absence of bugs, at least of some categories of common bugs, should be
formally verified.
After recalling the basic principles of abstract interpretation
including the notions of abstraction, approximation, soundness,
completeness,
false alarm, etc., we introduce the domain-specific static analyzer ASTRÉE
(www.astree.ens.fr) for proving the absence of runtime errors in safety
critical real time embedded synchronous software in the large.
The talk emphasizes soundness (no runtime error is ever omitted),
parametrization (the ability to refine abstractions by options and
analysis directives), extensibility (the easy incorporation of new
abstractions
to refine the approximation), precision (few or no false alarms for
programs in the considered application domain) and scalability (the
analyzer
scales to millions of lines).
In conclusion, present-day software engineering methodology, which is
based on the control of the design, coding and testing processes should
evolve in the near future, to incorporate a systematic control of final
software product thanks to domain-specific analyzers that scale up
Contact
Brigitta Hansen
0681 - 9325200
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
206
passcode not visible
logged in users only
Brigitta Hansen, 08/20/2008 14:42 -- Created document.