Relations as Executable Specifications: Taming Partiality and Non-determinism Using Invariants. - Nuno Macedo 001; Hugo Pacheco 001; Alcino Cunha (RAMiCS, 2012)

Automatic Unbounded Verification of Alloy Specifications with Prover9 - Nuno Macedo 001; Alcino Cunha (CoRR, 2012)

Implementing QVT-R Bidirectional Model Transformations Using Alloy. - Nuno Macedo 001; Alcino Cunha (FASE, 2013)

Model repair and transformation with Echo. - Nuno Macedo 001; Tiago Guimarães; Alcino Cunha (ASE, 2013)

A Generic Scheme and Properties of Bidirectional Transformations. - Hugo Pacheco 001; Nuno Macedo 001; Alcino Cunha; Janis Voigtländer (CoRR, 2013)

Composing Least-change Lenses. - Nuno Macedo 001; Hugo Pacheco 001; Alcino Cunha; José Nuno Oliveira (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Towards a Framework for Multidirectional Model Transformations. - Nuno Macedo 001; Alcino Cunha; Hugo Pacheco 001 (EDBT/ICDT Workshops, 2014)

Target Oriented Relational Model Finding. - Alcino Cunha; Nuno Macedo 001; Tiago Guimarães (FASE, 2014)

Bidirectional spreadsheet formulas. - Nuno Macedo 001; Hugo Pacheco 001; Nuno Rocha Sousa; Alcino Cunha (VL/HCC, 2014)

A relational approach to bidirectional transformation - Nuno Macedo 001 (2014)

Exploring Scenario Exploration. - Nuno Macedo 001; Alcino Cunha; Tiago Guimarães (FASE, 2015)

An ORCID based synchronization framework for a national CRIS ecosystem. - João Mendes Moreira 002; Alcino Cunha; Nuno Macedo 001 (F1000Research, 2015)

A framework for quality assessment of ROS repositories. - André Santos 001; Alcino Cunha; Nuno Macedo 001; Cláudio Lourenço (IROS, 2016)

Towards a Formal Validation of ETL Patterns Behaviour. - Bruno Oliveira 001; Orlando Belo; Nuno Macedo 001 (MEDI, 2016)

Lightweight specification and analysis of dynamic systems with rich configurations. - Nuno Macedo 001; Julien Brunel; David Chemouil; Alcino Cunha; Denis Kuperberg (SIGSOFT FSE, 2016)

Alloy meets TLA+: An exploratory study. - Nuno Macedo 001; Alcino Cunha (CoRR, 2016)

Least-change bidirectional model transformation with QVT-R and ATL. - Nuno Macedo 001; Alcino Cunha (Softw. Syst. Model., 2016)

Exploiting Partial Knowledge for Efficient Model Analysis. - Nuno Macedo 001; Alcino Cunha; Eduardo Pessoa (ATVA, 2017)

Formal Verification of ROS-Based Robotic Applications Using Timed-Automata. - Raju Halder; José Proença; Nuno Macedo 001; André Santos 001 (FormaliSE@ICSE, 2017)

Mining the usage patterns of ROS primitives. - André Santos 001; Alcino Cunha; Nuno Macedo 001; Rafael Arrais; Filipe Neves dos Santos (IROS, 2017)

A Feature-Based Classification of Model Repair Approaches. - Nuno Macedo 001; Jorge Tiago; Alcino Cunha (IEEE Trans. Software Eng., 2017)

Proposition of an Action Layer for Electrum. - Julien Brunel; David Chemouil; Alcino Cunha; Thomas Hujsa; Nuno Macedo 001; Jeanne Tawa (ABZ, 2018)

The electrum analyzer: model checking relational first-order temporal specifications. - Julien Brunel; David Chemouil; Alcino Cunha; Nuno Macedo 001 (ASE, 2018)

Property-based testing for the robot operating system. - André Santos 001; Alcino Cunha; Nuno Macedo 001 (A-TEST@ESEC/SIGSOFT FSE, 2018)

Improving the Visualization of Alloy Instances. - Rui Couto; José Creissac Campos; Nuno Macedo 001; Alcino Cunha (F-IDE@FLoC, 2018)

Teaching how to program using automated assessment and functional glossy games (experience report). - José Bacelar Almeida; Alcino Cunha; Nuno Macedo 001; Hugo Pacheco 001; José Proença (Proc. ACM Program. Lang., 2018)

Static-Time Extraction and Analysis of the ROS Computation Graph. - André Santos 001; Alcino Cunha; Nuno Macedo 001 (IRC, 2019)

Simplifying the Analysis of Software Design Variants with a Colorful Alloy. - Chong Liu; Nuno Macedo 001; Alcino Cunha (SETTA, 2019)

Sharing and Learning Alloy on the Web. - Nuno Macedo 001; Alcino Cunha; José Pereira 001; Renato Carvalho; Ricardo Silva; Ana C. R. Paiva; Miguel S. Ramalho; Daniel Castro Silva (CoRR, 2019)

Simulation under Arbitrary Temporal Logic Constraints. - Julien Brunel; David Chemouil; Alcino Cunha; Nuno Macedo 001 (F-IDE@FM, 2019)

Validating Multiple Variants of an Automotive Light System with Electrum. - Alcino Cunha; Nuno Macedo 001; Chong Liu (ABZ, 2020)

Experiences on Teaching Alloy with an Automated Assessment Platform. - Nuno Macedo 001; Alcino Cunha; José Pereira 001; Renato Carvalho; Ricardo Silva; Ana C. R. Paiva; Miguel Sozinho Ramalho; Daniel Castro Silva (ABZ, 2020)

ROSY: An elegant language to teach the pure reactive nature of robot programming. - Hugo Pacheco 001; Nuno Macedo 001 (IRC, 2020)

Verification of system-wide safety properties of ROS applications. - Renato Carvalho; Alcino Cunha; Nuno Macedo 001; André Santos 001 (IROS, 2020)

Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. - Alcino Cunha; Nuno Macedo 001 (Int. J. Softw. Tools Technol. Transf., 2020)

The High-Assurance ROS Framework. - André Santos 001; Alcino Cunha; Nuno Macedo 001 (RoSE@ICSE, 2021)

Experiences on teaching alloy with an automated assessment platform. - Nuno Macedo 001; Alcino Cunha; José Pereira 004; Renato Carvalho; Ricardo Silva; Ana C. R. Paiva; Miguel Sozinho Ramalho; Daniel Castro Silva (Sci. Comput. Program., 2021)

Schema-guided Testing of Message-oriented Systems. - André Santos 001; Alcino Cunha; Nuno Macedo 001 (ENASE, 2022)

Variability Analysis for Robot Operating System Applications. - André Santos 001; Alcino Cunha; Nuno Macedo 001; Sara Melo; Ricardo Pereira (IRC, 2022)

Verification of railway network models with EVEREST. - João Martins; José M. Fonseca 002; Rafael Costa; José Creissac Campos; Alcino Cunha; Nuno Macedo 001; José N. Oliveira (MoDELS, 2022)

Timely Specification Repair for Alloy 6. - Jorge Cerqueira; Alcino Cunha; Nuno Macedo 001 (SEFM, 2022)

Quantitative relational modelling with QAlloy. - Pedro Silva; José N. Oliveira; Nuno Macedo 001; Alcino Cunha (ESEC/SIGSOFT FSE, 2022)

Pardinus: A Temporal Relational Model Finder. - Nuno Macedo 001; Julien Brunel; David Chemouil; Alcino Cunha (J. Autom. Reason., 2022)

Merging cloned Alloy models with colorful refactorings. - Chong Liu; Nuno Macedo 001; Alcino Cunha (Sci. Comput. Program., 2022)

Exploring Automatic Specification Repair in Dafny Programs. - Alexandre Abreu; Nuno Macedo 001; Alexandra Mendes (ASEW, 2023)

Adding Records to Alloy. - Julien Brunel; David Chemouil; Alcino Cunha; Nuno Macedo 001 (ABZ, 2023)

Task Model Design and Analysis with Alloy. - Alcino Cunha; Nuno Macedo 001; Eunsuk Kang (ABZ, 2023)

Verifying Temporal Relational Models with Pardinus. - Nuno Macedo 001; Julien Brunel; David Chemouil; Alcino Cunha (ABZ, 2023)

Alloy Repair Hint Generation Based on Historical Data. - Ana Barros; Henrique Neto; Alcino Cunha; Nuno Macedo 001; Ana C. R. Paiva (FM (2), 2024)

Assessing the impact of hints in learning formal specification. - Alcino Cunha; Nuno Macedo 001; José Creissac Campos; Iara Margolis; Emanuel Sousa (SEET@ICSE, 2024)

Alloy Goes Fuzzy. - Pedro Silva; Alcino Cunha; Nuno Macedo 001; José N. Oliveira (ABZ, 2024)

Validating multiple variants of an automotive light system with Alloy 6. - Alcino Cunha; Nuno Macedo 001; Chong Liu (Int. J. Softw. Tools Technol. Transf., 2024)

On Quantitative Solution Iteration in QAlloy. - Pedro Silva; Nuno Macedo 001; José N. Oliveira (ABZ, 2025)