Symbolic execution is a well known and powerful technique that allows to perform several activities as program testing, program formal verification, program specialization, etc. However, symbolic execution suffers from some problems which disable it to become a wide used technique. For instance, symbolic execution fails when dealing with indexed variables as arrarys, or dynamic data structures as pointers. In this paper we discuss the problem of symbolic execution of programs involving indexed variables by providing a formal definition of symbolic execution. From this starting point we present a practical technique of representing indexed variables that we argue to be more effective than other approaches found in literature. Finally, we present two examples of application of our technique. The former is an example of symbolic testing while the latter is a formal verification of a program. © 1992
Coen Porisini, A., DE PAOLI, F. (1993). Array representation in symbolic execution. COMPUTER LANGUAGES, 18(3), 197-216 [10.1016/0096-0551(93)90025-V].
Array representation in symbolic execution
DE PAOLI, FLAVIO MARIAUltimo
1993
Abstract
Symbolic execution is a well known and powerful technique that allows to perform several activities as program testing, program formal verification, program specialization, etc. However, symbolic execution suffers from some problems which disable it to become a wide used technique. For instance, symbolic execution fails when dealing with indexed variables as arrarys, or dynamic data structures as pointers. In this paper we discuss the problem of symbolic execution of programs involving indexed variables by providing a formal definition of symbolic execution. From this starting point we present a practical technique of representing indexed variables that we argue to be more effective than other approaches found in literature. Finally, we present two examples of application of our technique. The former is an example of symbolic testing while the latter is a formal verification of a program. © 1992File | Dimensione | Formato | |
---|---|---|---|
ComputerLanguages1993.pdf
Solo gestori archivio
Descrizione: Articolo principale
Dimensione
763.03 kB
Formato
Adobe PDF
|
763.03 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.