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.

Bibliographic Details
Main Author: Lourenço, Cláudio Belo (author)
Other Authors: Frade, M. J. (author), Pinto, Jorge Sousa (author)
Format: conferencePaper
Language:eng
Published: 2014
Subjects:
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
Online Access:http://hdl.handle.net/1822/35223
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/35223

Internet

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

Similar Items