CONFIDENT is a toolchain for effective construction and evolution of REST APIs.

The general aim is to be able to describe, infer and statically verify component communication contracts, while also being able to generate boilerplate code for said components from their descriptions.

    • HeadREST is a RESTful API specification language, based on the Open API Specification, that has been developed in order to be able to describe behavioural properties of RESTful APIs.
    • TestTool is a tool developed to test RESTful APIs described with HeadREST using Z3Prover
    • HR-CodeGen is a tool for generating boilerplate code from HeadREST Specifications, taking advantage of the Open API Specification code generation tools

Its key ideas lie in:
– Detailing the structure of the data transferred on the different interactions
– Utilizing pre and pos-conditions to express (a) the relation between the data sent in the requests and received in the responses and (b) the state changes that occur afterwards

These ideas are then materialized in the HeadREST language, which has two fundamental concepts:
– refinement types, x:T where e, that consist of x values of type T that satisfy a property e.
– a type predicate, e in T, which returns true or false depending if the value e is or not of type T.

A definition of a type in HeadREST

Representation types help us describe the structure of the data transferred. The supported representation types are: objects, arrays, refinement types, scalar types (including integer, boolean, string and URITemplate) and any as our top type.

A specification of an operation in HeadREST

… resumo TestTool …

(Work in Progress)


Nuno Burnay



HeadREST Eclipse plugin
Update Site
Installing the Z3 binaries
        • Download the correct zip binaries for your Operative System.
        • Extract the archive and add the Z3 bin folder to your system path.
          • Unix: LD_LIBRARY_PATH environment variable
          • MAC OS X: DYLD_LIBRARY_PATH environment variable
        • Or clone the new Z3 repository and follow the instructions to compile it.
        • Add the generated folder to the system path.
Installing the Eclipse HeadREST Plugin
        • Go to the Help menu → Install New Software…
        • Type in in the work with field and press Enter;
        • Install the feature Xtext Complete SDK (confirm it is at least v2.13.0);
        • Restart Eclipse;
        • Go to the Help menu → Install New Software…
        • Type in the update site in the work with field and press Enter;
        • Select HeadREST Feature;
        • Press the Next button;
        • It takes a while for the update site to resolve the dependencies and contact the necessary update sites;
        • Trust us and accept the unsigned plugin;
        • Restart Eclipse. The installation is now complete.
Creating a HeadREST project
        • In Eclipse go to File->New…->Project. Create a new Java Project;
        • Create a .rspec file;
        • If asked, confirm to convert to a Xtext project;
        • Write your specification in the created .rspec file. Here you can find some examples.
        • Right click inside the editor and choose Validate (first option with this name in the menu);
        • Wait until Eclipse reports no more tasks in progress.

HeadREST terminal version

LD_LIBRARY_PATH=<path to folder with the libraries of Z3> java -jar headrest.jar <path to .rspec file>


Learning HeadREST

Head over to the Online tutorial to learn and practice using HeadREST with no installation on your machine.


      • F. Ferreira, T. Santos, F. Martins, A. Lopes and V. Vasconcelos. Especificação de Interfaces Aplicacionais REST. In Actas do 9º Encontro Nacional de Informática, INFORUM 2017, Aveiro, Portugal, 2017. pdf
      • Fábio Ferreira , Automatic Tests Generation for RESTful APIs , MSc Thesis, Departamento de Informática, FCUL , DI/FCUL , 2017.  pdf