Software Tools

At SysMA we aim at providing formal theoretical results with strong impact in practice. For this reason, we provide tool support for many of our proposed contributions.

This page collects the tools developed and maintained at SysMA, while a number of prototypes used to validate our techniques are listed here.

ERODE: Evaluation and Reduction of Ordinary Differential Equations

ERODE is a software tool for the solution and exact reduction of systems of ordinary differential equations (ODEs).

The tool implements two complementary equivalences over ODE variables: forward differential equivalence partitions ODE variables into blocks for which a self-consistent aggregate ODE system can be obtained; each aggregate ODE gives the cumulative dynamics of the sum of the original variables in the respective equivalence class. Backward differential equivalence identifies variables that have identical solutions whenever starting from the same initial conditions.

Visit the tool web page for more information.

Selected publications
Artifact Evaluated at POPL


MultiVeStA: Distributed Statistical Model Checking for Discrete Event Simulators

MultiVeStA is an efficient statistical analysis tool which can be easily integrated with existing discrete event simulators, enriching them with automated and distributed Statistical Model Checking capabilities.

MulltiVeStA has been successfully integrated with many simulators, ranging from formal languages to network or robotic simulators.

Visit the tool web page for more information.

Selected publications


DiffLQN: analysis of Layered Queueing Networks using ordinary differential equations

DiffLQN is a tool for the analysis of Layered Queueing Networks (LQNs) using ordinary differential equations.

The analysis run-time does not depend on the concurrency levels in the model, e.g. the number of cores in a processor or the multiplicity of a server task. The estimates are asymptotically exact for large enough concurrency levels.

Visit the tool  web page for more information.

Selected publications


Calcolo Età Vascolare: Vascular Age Calculation
Vascular Age

Calcolo Età Vascolare is an Android and iOS application implementing the SCORE algorithm to compute the “actual” vascular age of an individual as well as the risk of having heart attacks over the next 10 years.

The application is the first one implementing the SCORE system, and it was designed for Doctors.

Visit the tool web page for more information.