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.

Coen, A., Denaro, G., Ghezzi, C., Pezze', M. (2001). Using symbolic execution for verifying safety-critical systems. In Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (pp.142-151) [10.1145/503209.503230].

Using symbolic execution for verifying safety-critical systems

DENARO, GIOVANNI;PEZZE', MAURO
2001

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.
paper
symbolic execution, software verification, safety critical systems
English
Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering
1-58113-390-1
Coen, A., Denaro, G., Ghezzi, C., Pezze', M. (2001). Using symbolic execution for verifying safety-critical systems. In Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (pp.142-151) [10.1145/503209.503230].
Coen, A; Denaro, G; Ghezzi, C; Pezze', M
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/19909
Citazioni
  • Scopus 66
  • ???jsp.display-item.citation.isi??? ND
Social impact