Repositório Colecção:https://hdl.handle.net/1822/213122024-03-28T17:23:35Z2024-03-28T17:23:35ZBounded version vectorsAlmeida, José BacelarAlmeida, Paulo SérgioBaquero, Carloshttps://hdl.handle.net/1822/353122018-04-04T15:06:06Z2015-05-27T15:28:32ZTítulo: Bounded version vectors
Autor: Almeida, José Bacelar; Almeida, Paulo Sérgio; Baquero, Carlos
Resumo: Version vectors play a central role in update tracking under optimistic distributed systems, allowing the detection of obsolete or inconsistent versions of replicated data. Version vectors do not have a bounded representation; they are based on integer counters that grow indefinitely as updates occur. Existing approaches to this problem are scarce; the mechanisms proposed are either unbounded or operate only under specific settings. This paper examines version vectors as a mechanism for data causality tracking and clarifies their role with respect to vector clocks. Then, it introduces bounded stamps and proves them to be a correct alternative to integer counters in version vectors. The resulting mechanism, bounded version vectors, represents the first bounded solution to data causality tracking between replicas subject to local updates and pairwise symmetrical synchronization.
<b>Tipo</b>: bookPart2015-05-27T15:28:32ZSABS : Spark ABStraction - A TutorialMiraldo, Victor Cacciarihttps://hdl.handle.net/1822/352312015-05-20T14:40:20Z2015-05-20T14:40:20ZTítulo: SABS : Spark ABStraction - A Tutorial
Autor: Miraldo, Victor Cacciari
Resumo: 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.
<b>Tipo</b>: report2015-05-20T14:40:20ZExperimenting with Predicate AbstractionMiraldo, Victor Cacciarihttps://hdl.handle.net/1822/352302015-05-20T14:44:28Z2015-05-20T14:38:27ZTítulo: Experimenting with Predicate Abstraction
Autor: Miraldo, Victor Cacciari
Resumo: Predicate 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 generate the model. In this report we explain how we have extended the implementation of one such technique, that produces the most precise ex- istential abstraction of a program, and we establish a common framework for both this direct technique and a second one, based on cartesian ab- straction by weakest precondition calculations. This report a product of
the research grant BI22012 PTDC/EIA-CCO/117590/2010 UMINHO,
in the scope of the AVIACC project, supervised by Professors Jorge
Sousa Pinto and Maria João Frade.
<b>Tipo</b>: report2015-05-20T14:38:27ZProgramming from Galois connection : principles and applicationsMu, Shin-ChengOliveira, José Nuno Fonsecahttps://hdl.handle.net/1822/337882017-01-26T14:06:24Z2015-02-11T11:49:46ZTítulo: Programming from Galois connection : principles and applications
Autor: Mu, Shin-Cheng; Oliveira, José Nuno Fonseca
Resumo: Problem statements often resort to superlatives such as in eg. “. . . the smallest such number”, “. . . the best approximation”, “. . . the longest such list” which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part).
This paper introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution being sought.
The framework encompasses re-factoring of results previously developed by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with.
Descrição: "Technical Report No. TR-IIS-10-009"
<b>Tipo</b>: report2015-02-11T11:49:46ZCalculating fault propagation in functional programsMurta, Daniel R.Oliveira, José Nuno Fonsecahttps://hdl.handle.net/1822/259752013-11-07T01:07:06Z2013-11-06T14:42:31ZTítulo: Calculating fault propagation in functional programs
Autor: Murta, Daniel R.; Oliveira, José Nuno Fonseca
Resumo: The production of safety critical software is bound to a number of safety and certification standards in which estimating the risk of failure plays a central role. Yet risk estimation seems to live outside most programmers’ core practice, involving simulation techniques and worst case analysis performed a posteriori.
In this paper we propose that risk be constructively handled in functional programming by writing programs which choose between expected and faulty be- haviour and by reasoning about them in a linear algebra extension to the standard algebra of programming.
In particular, the paper calculates propagation of faults across standard program transformation techniques known as tupling and fusion, enabling the fault of the whole to be expressed in terms of the faults of its parts.
Descrição: Techn. Report TR-HASLab:01:2013
<b>Tipo</b>: report2013-11-06T14:42:31Z