Istituto di Scienza e Tecnologie dell'Informazione     
Levi G., Pegna A. Top-down fixed point semantics and symbolic execution. Internal note IEI-B77-22, 1977.
The alm of this paper is setting a formal framework for reasoning about the semantic defined by a symbolic Interpreter . The paper considerss a slmple recursive language, for which a bottom-up and a top-down fixed-point semantics are given and shown to be equivalent. The transformation whose fixed-point is the top-down denotation is proven to be exactly the evaluation rule of the symbol Interpreter. An informal discussio on standard programming languages leads to the conjecture that the transformation of the top-down fixed-point semantics be equivalent to the evaluation rule of the symbolic Interpreter extended with a set of simplification rules defined by an axiomation of the language primitive data types. The above results can be considered a first step in proving the validity of the "symbolic execution" approach to program analysis.

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional