Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/35231
Título: | SABS : Spark ABStraction - A Tutorial |
Autor(es): | Miraldo, Victor Cacciari |
Palavras-chave: | Program Verification Predicate Abstraction |
Data: | Jan-2014 |
Resumo(s): | SABS is a predicate abstraction laboratory that is beeing developed at University of Minho, Portugal. Our goal is not to produce a industrial software model checker, such as SLAM [BMR01] or SATABS [CKSY05], but to have a tool to study and compare the diferent techniques (and combination of techniques) that can be used to perform the predicate abstraction of a program, in our case, a SPARK program. This document is a both a tutorial on the usage of SABS and a (small) explanation of its implementation. Some knowledge on Predicate Abstraction and Program Verification is assumed, we refer the reader to [MLPF13] for some background on the techniques implemented by SABS. |
Tipo: | Relatório |
URI: | https://hdl.handle.net/1822/35231 |
Arbitragem científica: | no |
Acesso: | Acesso aberto |
Aparece nas coleções: | HASLab - Relatórios técnicos |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
VMiraldo-tutorial.pdf | Tutorial | 227,87 kB | Adobe PDF | Ver/Abrir |