<html><head><!-- Cousot-Tsinghua-Software-Day-2012-03-15.shtml -->
<title>P. Cousot. Automatic Large-Scale Software Verification by Abstract Interpretation</title>

<meta name="Keyword"
content="Abstract Interpretation, Static analysis, Astree, Astreea, Validation, Verification">
</head>

<body>
<hr>

<ul>
	 <li> <strong>Patrick Cousot.<br>
	 <a href="COUSOTtalks/Cousot-Tsinghua-Software-Day-2012-03-15.shtml">Automatic Large-Scale Software Verification by Abstract Interpretation</A>.<br>
	 </strong>      
    Invited Talk, <A href="http://formes.asia/tsd/">Tsinghua Software Day (TSD 2012)</A>, Tsinghua University, Beijing, China.
	 March 15<SUP>th</SUP>, 2012.
	 
	 <p>
	 </p>

	 
	 </li>
	 <li><em>Abstract:</em> <br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Abstract interpretation is a theory of abstraction and constructive approximation of
the mathematical structures used in the formal description of programming languages
and the inference or verification of undecidable program properties.
<BR>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Developed in the late seventies with Radhia Cousot, it has since then been
considerably applied to many aspects of programming, from syntax, to semantics, and
proof methods where abstractions are sound and complete but incomputable to fully
automatic, sound but incomplete approximate abstractions to solve undecidable
problems such as static analysis of infinite state software systems, contract
inference, type inference, termination inference, model-checking, abstraction
refinement, program transformation (including watermarking), combination of decision
procedures, security, malware detection, etc.
<BR>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;This last decade, abstract interpretation has been very successful in program
verification for mission- and safety-critical systems. An example is Astr&eacute;e
(<a href="http://www.astree.ens.fr">www.astree.ens.fr</A>) which is a static analyzer to verify the absence of runtime
errors in structured, very large C programs with complex memory usages, and involving
complex boolean as well as floating-point computations (which are handled precisely
and safely by taking all possible rounding errors into account), but without
recursion or dynamic memory allocation. Astr&eacute;e targets embedded applications as found
in earth transportation, nuclear energy, medical instrumentation, aeronautics and
space flight, in particular synchronous control/command such as electric flight
control or more recently asynchronous systems as found in the automotive industry.
Astr&eacute;e is industrialized by AbsInt (<a href="http://www.absint.com/astree/index.htm">www.absint.com/astree</A>).


<P></P>
	 
	 </li>
	 <li><em>Slides of the 55&nbsp;mn presentation</em> (to be used with <a
		  href="http://get.adobe.com/reader/">Acrobat
		  Reader</a>): <a 
		  href="../publications.www/slides-public/Cousot-Tsinghua-2012-03-14--4-1.pdf">.pdf</a>.</li>

	 <p>
	 </p>


</li>
	 <li><em>Bibliographic reference:</em>

<pre>
\bibitem{Cousot-Tsinghua-Software-Day-2012-03-15}
P. Cousot.
\newblock Automatic Large-Scale Software Verification by Abstract Interpretation.
\newblock \emph{Invited talk}, Tsinghua Software Day,  Tsinghua University, 
Beijing, China. 15 March 2012.

@inProceedings{Cousot-Tsinghua-Software-Day-2012-03-15,
   author =    {P{.} Cousot},
   title =     {Automatic Large-Scale Software Verification by Abstract Interpretation},
   booktitle = {Tsinghua Software Day},
   address =   { Tsinghua University, Beijing, China},
   month =     {15 March},
   year =      {2012},
}
</pre>
<p>
</p>

</ul>
</body>
<hr>
<b><a href=copyright.shtml#copyrightnotice">Copyright notice</a></b><BR>
<br><b>Last modified:</b>
<!--#echo var="LAST_MODIFIED" -->
<hr>


</html>