PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Levi G., Sirovich F. Procedural axiomatization in program verification. Internal note IEI-B77-04, 1977.
 
 
Abstract
(English)
The goal of the paper is to emphasize the connection between specification languages and program verification techniques, such as Floyd's Inductive assertions and Topor's virtual programs, which are based on symbolic execution. The paper claims the opportunity of having an "executable" specification language, i.e. of having a procedural representation of both the assertions, and the simplification rules and axioms. The parer describes a predicate logic functional specification language with an efficient symbolic interpreter. The interpreter can deterministically execute axioms which express functions as well as function properties, thus reducing most of the burden of theorem proving.
Subject Specification languages
Symbolic execution
Program verification
Predicate logic programming


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