Encontrados 2 documentos, a visualizar página 1 de 1
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 | |||||||
|
|
|
|
|
|
||