Software

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.

MeT

MeT is a Cloud-enabled framework that can be used alone or in conjunction with OpenStack for the automatic and heterogeneous reconfiguration of HBase. MeT is an workload aware system that provides automatic elasticity for the HBase NoSQL database. MeT not only adds and removes nodes automatically and according to system load, but also reconfigures them according to the observed workloads. As a result, it achieves a significant increase in overall system performance.

MHS2

MHS2 is a heuristic-based approximation algorithm for solving the minimal hitting set/set cover problem.

Modelery - Models Refinery

An online repository for software artifacts (mainly models).

PVSio-web prototyping and analysis tool

PVSio-web is a graphical environment that transforms the animation capabilities of the standard PVS theorem proving system with a sophisticated graphical front-end allowing interactive (human-computer) systems modelling and prototyping. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analysing commercial medical devices, and has been used to create training material for device developers and device users.

PVSIOWeb

This is a prototyping toolkit based on the Prototyping Verification System (PVS), that supports the development of prototypes by defining their appearance, using displays and buttons and their model, using a EmuChart with states and transitions between the states. The model can also be exported to different model languages.

SafeCloud Photos

SafeCloud Photos is a revolutionary photography app that not only allows you to take beautiful photos but also guarantees that they stay private at all times.

SmellSheet Detective

SmellSheet Detective is a tool to find bad smells in spreadsheets.

Symbiosis

A tool that automatically isolates concurrency bugs.

UBlog Benchmark

UBlog is a performance evaluation toolkit that mimics the usage of the Twitter social network. The workload may be used with both key-value stores and relational databases. 

uCat - Use Case Analysis Tool

A tool which supports the rapid prototyping of software, based in user requirements. 

VooDooM

VooDooM transforms VDM-SL datatype specifications to obtain an equivalent relational representation. This relational representation can be exported as VDM-SL datatypes or translated to SQL table definitions.