We will show how tools for software verification such as SMT solver and theorem prover based verfiers (where the inductive argument necessary for the proof is either provided by the end-user or by refinement of the specification such as code contracts) or static analyzers (where the inductive argument necessary for the proof is computed directly (e.g. by elimination) or iteratively with convergence acceleration by widening/narrowing) can be constructed by systematic abstraction of their transition-based or structural operational semantics thus leading to verified verification tools. As an application, we will consider the construction of static analyzers for proving program safety properties. Examples such as ASTRÉE (www.astree.ens.fr/) and the MSR static checker (cccheck) will be rapidly overviewed.
\bibitem{Cousot-LASER2011} Patrick Cousot. \newblock Abstract interpretation based tool construction for software verification. \newblock 8th LASER Summer School on Software Engineering, Tools for Practical Software Verification. \newblock September 4-10, 2011 - Elba Island, Italy. @unpublished{Cousot-LASER2011, author = "Patrick Cousot", title = "Abstract interpretation based tool construction for software verification", booktitle = "8th LASER Summer School on Software Engineering, Tools for Practical Software Verification", address = "Elba Island, Italy", month = {September 4--10, }, year = 2011, }
Saturday, 10-Sep-2011 11:19:06 CEST