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 MARIA
Ultimo
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. © 1992
Articolo in rivista - Articolo scientifico
Ada; Indexed variables; Program testing; Program verification; Symbolic execution; Computer Science (all)
English
197
216
20
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].
Coen Porisini, A; DE PAOLI, F
File in questo prodotto:
File 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.

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