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,...

ver descrição completa

Detalhes bibliográficos
Autor principal: Cruz, Daniela da (author)
Outros Autores: Frade, M. J. (author), Pinto, Jorge Sousa (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2012
Assuntos:
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
Texto completo:http://hdl.handle.net/1822/30966
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/30966

Texto Completo

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

Registos relacionados