Description: This project comprises of a server-side extension that provides an proxy end-point for serving service metadata & a client-side proxy in JavaScript and also a client-side task that generates a

Description: Behaviour type inference for a Java like object-oriented language. Developed at: NOVA Contacts: aravara@fct.unl.pt  Available at: http://usinfer.sourceforge.net/

Description: Conversion from/to Mungo usages to a suitable form of finite state automata with internal and external non-determinism Developed at: NOVA Contacts: aravara@fct.unl.pt, jd.mota@campus.fct.unl.pt Available at: https://jdmota.github.io/mungo-typestate-parser/

Description: TRAC is a tool for the specification and verification of coordinated multiparty distributed systems. Relying on finite-state machines (FSMs) where transition labels look like Hoare triples, TRAC can specify the

Description: Automatic program verification tool for proving temporal properties of programs, such as safety, termination, or properties specified in the logic CTL. T2 can work directly on C programs. Developed at:

Description: Test driver of RESTful API based on binary session types. The tool features a domain-specific language for OpenAPI specifications, COpenAPI, that enables the modelling of communication protocols between a

Description: SEArch, after Service Execution Architecture, is a language-independent execution infrastructure capable of performing transparent dynamic reconfiguration of software artefacts. SEArch exploits Choreographic mechanisms to specify interoperability contracts, thus providing the

Description: Allows the user to define global views in terms of global choreographies, (2) verifies realisability of the global view and identifies all possible misbehaviors that could arise from a message-passing