TY - GEN
T1 - Verification of embedded software
T2 - 1st International Workshop on Embedded Software, EMSOFT 2001
AU - Cousot, Patrick
AU - Cousot, Radhia
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2001.
PY - 2001
Y1 - 2001
N2 - 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 highlight some of the problems to be solved and envision possible abstract interpretation based static analysis solutions.
AB - 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 highlight some of the problems to be solved and envision possible abstract interpretation based static analysis solutions.
UR - http://www.scopus.com/inward/record.url?scp=84947205553&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84947205553&partnerID=8YFLogxK
U2 - 10.1007/3-540-45449-7_8
DO - 10.1007/3-540-45449-7_8
M3 - Conference contribution
AN - SCOPUS:84947205553
SN - 3540426736
SN - 9783540426738
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 97
EP - 113
BT - Embedded Software - 1st International Workshop, EMSOFT 2001, Proceedings
A2 - Henzinger, Thomas A.
A2 - Kirsch, Christoph M.
PB - Springer Verlag
Y2 - 8 October 2001 through 10 October 2001
ER -