SPARK-BMC: checking SPARK code for bugs
The standard SPARK deductive verification tools, based on contracts, are not practical in early stages when the idea is only bug catching. We discuss the implementation of a bounded model checker for SPARK, focusing on specific challenges of this language. Our tool is fully automatic, complementing...
| Autor principal: | |
|---|---|
| Outros Autores: | , , |
| Formato: | conferenceObject |
| Idioma: | eng |
| Publicado em: |
2013
|
| Assuntos: | |
| Texto completo: | http://hdl.handle.net/1822/26411 |
| País: | Portugal |
| Oai: | oai:repositorium.sdum.uminho.pt:1822/26411 |