Software

APEX: Agile Prototyping for user EXperience

Ubiquitous computing (Ubicomp) technologies are providing exciting new opportunities for enhancing physical spaces to support the needs and activities of people within them. The ability to develop such systems effectively will offer significant competitive advantage. Tools are required that will predict problems relating to use early in the design cycle. This proposal brings together a team of researchers and developers aimed at prototyping and calibrating methods and tools that facilitate the development of technology enhanced environments.

CAO domain-specific language for cryptography

Repository URL: 
http://hackage.haskell.org/package/cao-0.1

Our group maintains a domain-specific software development tool-chain for the implementation and verification of cryptographic software based on the CAO cryptographic language.

More information is available here.

CAO language

Repository URL: 
http://hackage.haskell.org/package/cao

The CAO language is aimed at writing cryptographic software in a higher abstraction level which is then transformed and compiled to the C language, while preserving the overall safety properties.

The CAO compiler is publicly available from the Hackage repository.

CIRCUS

Repository URL: 
https://www.irit.fr/recherches/ICS/softwares/circus/

It is a toolkit that enables the development and analysis of formal models. The toolkit enables task modelling and analysis (simulation), using a graphical notation. The behaviour of the system can be described in a notation based on Petri Nets. The models can be co-executed.

DataFlasks

Repository URL: 
https://github.com/fmaia/dataflasks

DataFlasks is a key-value data store built solely based on gossip-based protocols. It leverages the inherent characteristics of such protocols to be able to provide data persistence guarantees even in highly dynamic, massive scale systems.

DEDIS

DEDIS is a novel open source distributed post-processing deduplication system. Its main contribution is a novel optimistic asynchronous mechanism for eliminating duplicated data among virtual machines deployed on several remote hosts. This mechanism along with other optimizations allows achieving nearly native disk I/O throughput for virtual machines even when deduplication is being performed in the background. Additionally, DEDIS is fully distributed, allowing the system to scale, and is resilient to server crashes.

DEDISbench

Repository URL: 
https://github.com/jtpaulo/dedisbench

DEDISbench is an open source micro I/O benchmark suitable for evaluating deduplication systems by generating blocks with a realistic content distribution. The benchmark also allows running tests with different load intensities and introduces a novel hotspot access pattern for I/O requests.

Echo: Model repair and transformation

Echo is a tool for model repair and transformation based on the Alloy model finder, with support for bidirectional model transformations. It is able to both check and recover, through minimal updates, both intra- and inter-model consistency, and is built over the Eclipse Modeling Framework (EMF).

Escada Replicator

Repository URL: 
http://escada.sourceforge.net/

ESCADA is a portable and flexible database replication system that accom- modates multiple reliability, performance, and applicability tradeoffs: Target scenarios range from shared-nothing clusters to remote sites for disaster prevention. Currently supported database management systems include Apache Derby, PostgreSQL, and MySQL.

Galculator

The Galculator is a prototype of a proof assistant based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs.

It is written in the Haskell programming language resorting to many language extensions, specially GADTs (Generalized Algebraic Data Types).

GAPI

Repository URL: 
https://launchpad.net/gapi

The GORDA Architecture and Programming Interface (GAPI) allows porta- ble replication protocols to be easily implemented and reused with different database management systems. It is designed to be provided either na- tively by the database server or by a server wrapper. The included functionality supports a variety of replication protocols, both master-slave or multi-master, synchronous or asynchronous. It should also be useful to build other data management tools.

Hets

Repository URL: 
http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/ind...

A very interesting tool that integrates a number of logics for (co)algebraic specification.

I implemented in Hets hybridisation: a method to turn logics hybrid. See more details about this in my Msc. dissertation

HTAPBench

Gartner claims the ever increasing demand for real-time analytics requires the fusion of Transactional (OLTP) and Analytical (OLAP) databases, eschewing ETL processes and giving birth to the so-called Hybrid Analytical and Trans- actional Processing (HTAP) databases.

IVY Workbench

The IVY workbench is a model based tool for the analysis of interactive systems designs. The tool acts as a front end to the SMV model checker, creating an abstraction layer where models of interactive systems can be developed and analysed.


MDSheet

MDSheet is a framework for the embedding, evolution and inference of spreadsheet models. This framework offers a model-driven software development mechanism for spreadsheet users.