AEminium Project at Madeira

 

AEminium aims at the implementation of a framework in which programmers can write programs that are concurrent by default. Instead of writing sequential code from which a runtime execution engine infers concurrency, programmers express dependency information that is used by a compile-time checker to verify correctness condition and by the run-time system to enable concurrent execution. This dependency information is provided by users in a combined form of access permissions and typestates.


The paper Concurrency by Default: Using Permission to Express Dataflow in Stateful Programs provides an overview of AEminium. You can reach the paper here and some slides here.


The AEminium team at Madeira is led by Néstor Cataño. Our research spans on 3 axis. Néstor Cataño and Ijaz Ahmed work on the definition of Generation Access Permission (GAP) algorithm. Néstor Cataño and Radu Siminiceanu work on a model-checking based framework to verify AEminium specifications in isolation. Néstor Cataño, Camilo Rueda, and Carlos Olarte work on an abstract interpretation based framework to check AEminium specifications that make use of integer arithmetic operations.


The Plural Tool is the predecessor tool of AEminium. We are currently carrying out a case study on the use of Plural in the specification of a Multi-Task Threaded Server (MTTS) application provided by our industrial partner Novabase. You can find here a report describing the MTTS application.


AEminium is a multi-disciplinary group that involves faculty from several universities, Paulo Marques and Bruno Cabral work at The University of Coimbra, Néstor Cataño at The University of Madeira, and Jonathan Aldrich and Roberto Bocchino at Carnegie Mellon University in Pittsburgh.