P. Cousot & R. Cousot, Static Analysis of Embedded Software: Problems and Perspectives

Patrick Cousot & Radhia Cousot.
Verification of Embedded Software: Problems and Perspectives.
EMSOFT 2001: First Workshop on Embedded Software , October, 8^th - 10^th, 2001, Lake Tahoe, California, U.S.A., Thomas A. Henzinger and Christoph M. Kirsch (Eds.), Lecture Notes in Computer Science 2211, pp. 97—113. © Springer.
Abstract: Computer aided formal methods have been very successful for the verification or at least enhanced debugging of hardware. The cost of correction of a hardware bug is huge enough to justify high investments in alternatives to testing such as correctness verification. This is not the case for software for which bugs are a quite common situation which can be easily handled through online updates. However in the area of embedded software, errors are hardly tolerable. Such embedded software is often safety-critical, so that a software failure might create a safety hazard in the equipment and put human life in danger. Thus embedded software verification is a research area of growing importance. Present day software verification technology can certainly be useful but is yet too limited to cope with the formidable challenge of complete software verification. We survey some of the problems to be solved and envision possible pragmatic solutions.
The paper is available two formats:
- Published regular version (17p) : A4 paper .pdf (263 Ko) for viewing in color with Acrobate Reader and compressed PostScript .ps.gz (946 Ko) for viewing with Ghostview or printing;
- The electronic version (22p) has an extended bibliography: A4 paper .pdf (326 Ko) for viewing with Acrobate Reader and compressed PostScript .ps.gz (955 Ko) for viewing with Ghostview or printing.
Slides of the 25mn EMSOFT'2001 presentation are available in various formats:
- A4 landscape .pdf.gz (173 Ko) for viewing with Acrobate Reader and compressed PostScript .ps.gz (1.1 Mo) for viewing with Ghostview or printing;
- 4 slides per A4 landscape sheet for printing in color .ps.gz (375 Ko).

\bibitem{CousotCousot-EMSOFT01}
P{.} Cousot and R{.} Cousot.
\newblock Verification of Embedded Software: Problems and Perspectives,
invited paper.
\newblock In Proc.  \emph{First International Workshop on Embedded
Software, EMSOFT 2001}, T.A{.} Henzinger and C.M{.} Kirsch (Eds.).  Lecture
Notes in Computer Science, Vol{.} 2211, pages 97--113.  Springer, 2001.

@incollection{CousotCousot-EMSOFT01,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Verification of Embedded Software: Problems and Perspectives, invited paper},
   booktitle = {Proc. \emph{First Int.\ Workshop on Embedded Software, 
                EMSOFT 2001}},
   editor =    {Henzinger, T.A{.} and Kirsch, C.M{.}},
   year =      {2001},
   series =    {Lecture Notes in Computer Science},
   volume =    2211,
   pages =    {97--113},
   publisher = {Springer},
}