Verification conditions for single-assignment programs

A mechanism for generating verification conditions (VCs) for the iteration-free fragment of an imperative language is fundamental in any deductive program verification system. In this paper we revisit symbolic execution, weakest preconditions, and bounded model checking as VC-generation mechanisms,...

Full description

Bibliographic Details
Main Author: Cruz, Daniela da (author)
Other Authors: Frade, M. J. (author), Pinto, Jorge Sousa (author)
Format: conferencePaper
Language:eng
Published: 2012
Subjects:
Program verification
Deductive verification
Single-assignment form
Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática
Ciências Naturais::Ciências da Computação e da Informação
Online Access:http://hdl.handle.net/1822/30966
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/30966

Internet

http://hdl.handle.net/1822/30966

Similar Items