Encontrados 3 documentos, a visualizar página 1 de 1
A bounded model checker for SPARK programs
Lourenço, Cláudio Filipe Belo da SilvaDissertação de mestrado em Engenharia de Informática ; Formal verification of software has been an active topic in the area of computer science. Several techniques to verify software are now available, and many tools have been created over the years for different languages and using different techniques. However, for SPARK, a programming language broadly used in critical systems, only deductive verification to...
Experimenting with predicate abstraction
Miraldo, Victor Cacciari; Frade, M. J.; Lourenço, Cláudio; Pinto, Jorge SousaPredicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may differ based on (i) the set of predicates used; or (ii) the algorithmic technique employed to gen- erate the model. In this paper we explain how we have implemented...
SPARK-BMC : checking SPARK code for bugs
Lourenço, Cláudio; Miraldo, Victor Cacciari; Frade, M. J.; Pinto, Jorge SousaThe 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 the existing tools for SPARK.
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||