Using symbolic execution for verifying safety-critical systems

Alberto Coen-Porisini, Giovanni Denaro, Carlo Ghezzi, Mauro Pezzè

Abstract

Safety critical systems require to be highly reliable and thus special care is taken when verifying them in order to increase the confidence in their behavior. This paper addresses the problem of formal verification of safety critical systems by providing empirical evidence of the practical applicability of symbolic execution and of its usefulness for checking safety-related properties. In this paper, symbolic execution is used for building an operational model of the software on which safety properties, expressed by means of a Path Description Language (PDL), can be assessed.

BibTeX

@inproceedings{CoenPorisini-al:FSE01,
  author    = {Alberto Coen{-}Porisini and
               Giovanni Denaro and
               Carlo Ghezzi and
               Mauro Pezz{\`{e}}},
  title     = {Using symbolic execution for verifying safety-critical systems},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {142--151},
  publisher = {{ACM}},
  year      = {2001},
}

Using symbolic execution for verifying safety-critical systems

Abstract

Related papers