A bounded model checker for SPARK programs

This paper discusses the design and implementation of a bounded model checker for SPARK code, and provides a proof of concept of the utility and practicality of bounded verification for SPARK.

Detalhes bibliográficos
Autor principal:	Lourenço, Cláudio Belo (author)
Outros Autores:	Frade, M. J. (author), Pinto, Jorge Sousa (author)
Formato:	conferencePaper
Idioma:	eng
Publicado em:	2014
Assuntos:	Bounded model checking of software SPARK Ciências Naturais::Ciências da Computação e da Informação Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática Science & Technology
Texto completo:	http://hdl.handle.net/1822/35223
País:	Portugal
Oai:	oai:repositorium.sdum.uminho.pt:1822/35223

Descrição
Resumo:	This paper discusses the design and implementation of a bounded model checker for SPARK code, and provides a proof of concept of the utility and practicality of bounded verification for SPARK.