SABS : Spark ABStraction - A Tutorial
| Autor: | Miraldo, Victor Cacciari |
|---|---|
| Přispěvatelé: | Universidade do Minho |
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: |
Program Verification
Predicate Abstraction Ciências Naturais::Ciências da Computação e da Informação Ciências da Computação e da Informação [Ciências Naturais] Engenharia Eletrotécnica Eletrónica e Informática [Engenharia e Tecnologia] Engenharia e Tecnologia::Engenharia Eletrotécnica Eletrónica e Informática |
| Zdroj: | Repositório Científico de Acesso Aberto de Portugal Repositório Científico de Acesso Aberto de Portugal (RCAAP) instacron:RCAAP |
| Popis: | 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. This work is funded by ERDF - European Regional Development Fund through the COMPETE Programme (operational programme for competitiveness) and by National Funds through the FCT - Fundação para a Ciência e a Tecnologia (Portuguese Foundation for Science and Technology) within project FCOMP-01-0124-FEDER-020486. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|