SABS : Spark ABStraction - A Tutorial

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 technique...

Full description

Bibliographic Details
Main Author: Miraldo, Victor Cacciari (author)
Format: report
Language:eng
Published: 2014
Subjects:
Program Verification
Predicate Abstraction
Ciências Naturais::Ciências da Computação e da Informação
Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática
Online Access:http://hdl.handle.net/1822/35231
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/35231
Description
Summary: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.

Similar Items