2024
A. Barros, H. Neto, A. Cunha, N. Macedo and A. C. R. Paiva. Alloy repair hint generation based on historical data . In the proceedings of the 26th International Symposium on Formal Methods (FM'24). Springer, to appear. P. Silva, A. Cunha, N. Macedo and J. N. Oliveira. Alloy goes fuzzy. In the proceedings of the 10th International Conference on Rigorous State Based Methods (ABZ'24). LNCS 14759. Springer, 2024. A. Cunha, N. Macedo, J. C. Campos, I. Margolis and E. Sousa. Assessing the impact of hints in learning formal specification. In the proceedings of the 46th International Conference on Software Engineering: Software Engineering Education and Training (SEET@ICSE'24). IEEE, 2024. A. Cunha, N. Macedo and C. Liu. Validating multiple variants of an automotive light system with Alloy 6. International Journal on Software Tools for Technology Transfer 26(3). Springer, 2024. (extended version of this conference paper)
2023
A. Abreu, N. Macedo and A. Mendes. Exploring automatic specification repair in Dafny programs. In the proceedings of the 5th International Workshop on Automated and Verifiable Software System Development (ASYDE@ASE'23). IEEE, 2023. J. Brunel, D. Chemouil, A. Cunha and N Macedo. Adding records to Alloy. In the proceedings of the 9th International Conference on Rigorous State Based Methods (ABZ'23). LNCS 14010. Springer, 2023. A. Cunha, N. Macedo and E. Kang. Task model design and analysis with Alloy. In the proceedings of the 9th International Conference on Rigorous State Based Methods (ABZ'23). LNCS 14010. Springer, 2023. N. Macedo, J. Brunel, D. Chemouil and A. Cunha. Verifying temporal relational models with Pardinus. In the proceedings of the 9th International Conference on Rigorous State Based Methods (ABZ'23). LNCS 14010. Springer, 2023. (journal-first version of this journal paper) N. Macedo and A. Cunha. Teaching Alloy with Alloy4Fun. Tutorial at the 9th International Conference on Rigorous State Based Methods (ABZ'23). Nancy, France, 2023.
2022
A. Santos, A. Cunha, N. Macedo, S. Melo and R. Pereira. Variability analysis for Robot Operating System applications. In the proceedings of the 4th IEEE International Conference on Robotic Computing (IRC'22). IEEE, 2022. P. Silva, J. N. Oliveira, N. Macedo and A. Cunha. Quantitative relational modelling with QAlloy. 21st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). ACM, 2022. J. Martins, J. M. Fonseca, R. Costa, J. C. Campos, A. Cunha, N. Macedo and J. N. Oliveira. Verification of railway network models with EVEREST. ACM/IEEE 25th International Conference on Model Driven Engineering Languages and Systems (MODELS). ACM, 2022. N. Macedo, J. Brunel, D. Chemouil and A. Cunha. Pardinus: A temporal relational model finder. Journal of Automated Reasoning, 66(4). Springer, 2022. J. Cerqueira, A. Cunha and N. Macedo. Timely specification repair for Alloy 6. 20th International Conference on Software Engineering and Formal Methods (SEFM). LNCS 13550. Springer, 2022. C. Liu, N. Macedo and A. Cunha. Merging cloned Alloy models with colorful refactorings. Science of Computer Programming, 220. Elsevier, 2022. (extended version of this conference paper) A. Santos, A. Cunha and N. Macedo. Schema-guided testing of message-oriented systems. In the proceedings of the 17th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE). SCITEPRESS, 2022.
2021
N. Macedo, A. Cunha, J. Pereira, R. Carvalho, R. Silva, A. C. R. Paiva, M. S. Ramalho and D. Silva. Experiences on teaching Alloy with an automated assessment platform. Science of Computer Programming, 211. Elsevier, 2021. (extended version of this conference paper) A. Santos and N. Macedo. Improving the quality of ROS applications with HAROS. Tutorial at the 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'21). Prague, Czech Republic, 2021. H. Pacheco and N. Macedo. ROSY: An elegant language to teach the pure reactive nature of robot programming. International Journal of Robotic Computing 3(1). KS Press, 2021. (extended version of this conference paper) A. Santos, A. Cunha and N. Macedo. The High-Assurance ROS framework. In the proceedings of the 3rd International Workshop on Robotics Software Engineering (RoSE@ICSE'21). IEEE, 2021. (tool demo)
2020
R. Carvalho, A. Cunha, N. Macedo and A. Santos. Verification of system-wide safety properties of ROS applications. In the proceedings of the 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'20). IEEE, 2020. C. Liu, N. Macedo and A. Cunha. Merging cloned Alloy models with colorful refactorings. In the proceedings of the 23rd Brazilian Symposium on Formal Methods (SBMF'20). LNCS 12475. Springer, 2020. A. Cunha, N. Macedo and C. Liu. Validating multiple variants of an automotive light system with Electrum. In the proceedings of the 7th International Conference on Rigorous State Based Methods (ABZ'20). LNCS 12071. Springer, 2020. N. Macedo, A. Cunha, J. Pereira, R. Carvalho, R. Silva, A. C. R. Paiva, M. S. Ramalho and D. Silva. Experiences on teaching Alloy with an automated assessment platform. In the proceedings of the 7th International Conference on Rigorous State Based Methods (ABZ'20). LNCS 12071. Springer, 2020. H. Pacheco and N. Macedo. ROSY: An elegant language to teach the pure reactive nature of robot programming. In the proceedings of the 4th IEEE International Conference on Robotic Computing (IRC'20). IEEE, 2020. A. Cunha and N. Macedo. Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. International Journal on Software Tools for Technology Transfer 22(3). Springer, 2020. (extended version of this conference paper)
2019
H. Pacheco and N. Macedo. ROSY: An elegant language to teach the pure reactive nature of robot programming. CoRR abs/1911.03262. arXiv, 2019. (draft version of this conference paper) J. Brunel, D. Chemouil, A. Cunha and N. Macedo. Simulation under arbitrary temporal logic constraints. Electronic Proceedings in Theoretical Computer Science 310. Open Publishing Association, 2019. (revised version of this pre-proceedings paper) C. Liu, N. Macedo and A. Cunha. Simplifying the analysis of software design variants with a colorful Alloy. In the proceedings of the 5th International Symposium on Dependable Software Engineering. Theories, Tools, and Applications (SETTA'19). LNCS 11951. Springer, 2019. J. Brunel, D. Chemouil, A. Cunha, E. Kang and N. Macedo. Formal software design with Alloy and Electrum. Tutorial at the 3rd World Congress on Formal Methods (FM'19). Porto, Portugal, 2019. J. Brunel, D. Chemouil, A. Cunha and N. Macedo. Simulation under arbitrary temporal logic constraints. Presented at the 5th Workshop on Formal Integrated Development Environment (F-IDE@FM'19). 2019. N. Macedo, A. Cunha, J. Pereira, R. Carvalho, R. Silva, A. C. R. Paiva, M. S. Ramalho and D. Silva. Sharing and learning Alloy on the web. CoRR abs/1907.02275. arXiv, 2019. (draft version of this journal paper) A. Santos, A. Cunha and N. Macedo. Static-time extraction and analysis of the ROS Computation Graph. In the proceedings of the 3rd IEEE International Conference on Robotic Computing (IRC'19). IEEE, 2019. A. Anjorin, A. Cleve, S. Copei, Z. Diskin, J. Gibbons, H. Ko, N. Macedo, J. McKinna, A. Schürr, B. V. Selic, P. Stevens, J. H. Weber and N. Weidmann. WG2: Partial consistency notions. In the report from the Dagstuhl Seminar on Multidirectional Transformations and Synchronisations (Seminar 18491). Schloss Dagstuhl, 2019.
2018
A. Santos, A. Cunha and N. Macedo. Property-based testing for the Robot Operating System. In the proceedings of the 9th International Workshop on Automated Software Testing (A-TEST@ESEC/FSE'18). ACM, 2018. J. Brunel, D. Chemouil, A. Cunha and N. Macedo. The Electrum Analyzer: Model checking relational first-order temporal specifications. In the proceedings of the 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE'18). ACM, 2018. (tool demo) R. Couto, J. C. Campos, N. Macedo and A. Cunha. Improving the visualization of Alloy instances. Electronic Proceedings in Theoretical Computer Science 284. Open Publishing Association, 2018. (revised version of this pre-proceedings paper) A. Cunha and N. Macedo. Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. In the proceedings of the 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ'18). LNCS 10817. Springer, 2018. J. Brunel, D. Chemouil, A. Cunha, T. Hujsa, N. Macedo and J. Tawa. Proposition of an action layer for Electrum. In the proceedings of the 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ'18). LNCS 10817. Springer, 2018. N. Macedo. On extending Kodkod to support temporal features and scenario exploration. Presented at the Workshop on the Future of Alloy. Cambridge, MA, 2018. J. B. Almeida, A. Cunha, N. Macedo, H. Pacheco and J. Proença. Teaching how to program using automated assessment and functional Glossy games (experience report). In the proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP'18). PACMPL 2(ICFP). ACM, 2018. R. Couto, J. C. Campos, N. Macedo and A. Cunha. Improving the visualization of Alloy instances. Presented at the 4th Workshop on Formal Integrated Development Environment (F-IDE@FLoC'18). Oxford, UK, 2018.
2017
N. Macedo, A. Cunha and E. Pessoa. Exploiting partial knowledge for efficient model analysis. In the proceedings of the 15th International Symposium Automated Technology for Verification and Analysis (ATVA'17). LNCS 10482. Springer, 2017. N. Macedo, T. Jorge and A. Cunha. A feature-based classification of model repair approaches. IEEE Transactions on Software Engineering 43(7). IEEE, 2017. A. Santos, A. Cunha, N. Macedo, R. Arrais and F. N. Santos. Mining the usage patterns of ROS primitives. In the proceedings of the 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'17). IEEE, 2017. R. Halder, J. Proença, N. Macedo and A. Santos. Formal verification of ROS-based robotic applications using timed-automata. In the proceedings of the 5th IEEE/ACM International FME Workshop on Formal Methods in Software Engineering (FormaliSE@ICSE'17). IEEE, 2017. M. Carvalho, N. Macedo and O. Belo. Checking the correctness of what-if scenarios. Presented at the International Conference on Research and Practical Issues of Enterprise Information Systems - 11th IFIP-WG 8.9 Working Conference (CONFENIS'17). Shanghai, China, 2017.
2016
N. Macedo, J. Brunel, D. Chemouil, A. Cunha and D. Kuperberg. Lightweight specification and analysis of dynamic systems with rich configurations. In the proceedings of the 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE'16). ACM, 2016. N. Macedo and A. Cunha. Least-change bidirectional model transformation with QVT-R and ATL. Software and Systems Modeling 15(3). Springer, 2016. (extended version of this conference paper) A. Santos, A. Cunha, N. Macedo and C. Lourenço. A framework for quality assessment of ROS repositories. In the proceedings of the 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS'16). IEEE/RSJ, 2016. B. Oliveira, O. Belo and N. Macedo. Towards a formal validation of ETL patterns behavior. In the proceedings of the 6th International Conference on Model and Data Engineering (MEDI'16). LNCS 9893. Springer, 2016. N. Macedo, A. Cunha. Alloy meets TLA+: An exploratory study. CoRR abs/1603.03599. arXiv, 2016.
2015
N. Macedo, A. Cunha and T. Guimarães. Exploring scenario exploration. In the proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering (FASE@ETAPS'15). LNCS 9033. Springer, 2015. J. M. Moreira, A. Cunha and N. Macedo. An ORCID-based synchronization framework for a national CRIS ecosystem. F1000Research 4:181. F1000Research, 2015. (revised version of this pre-proceedings paper) A. Cunha and N. Macedo. PTCRISync specification: An ORCID-based synchronization framework for PTCRIS. Consultancy report prepared for the FCCN|FCT. INESC TEC, 2015. (superseded by the online documentation) J. M. Moreira, A. Cunha and N. Macedo. An ORCID-based synchronization framework for a national CRIS ecosystem. Presented at the 2015 ORCID-CASRAI Joint Conference (ORCID-CASRAI'15). Barcelona, Spain, 2015. N. Macedo, T. Jorge and A. Cunha. A feature-based classification of model repair approaches. CoRR abs/1504.03947. arXiv, 2017. (draft version of this journal paper)
2014
N. Macedo. A relational approach to bidirectional transformation. PhD Thesis, Universidades do Minho, Aveiro e Porto, Portugal, 2014. A. Cunha, N. Macedo and T. Guimarães. Target oriented relational model finding. In the proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE@ETAPS'14). LNCS 8411. Springer, 2014. N. Macedo, H. Pacheco, N. Sousa and A. Cunha. Bidirectional spreadsheet formulas. In the proceedings of the IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC'14). IEEE, 2014. N. Macedo, A. Cunha and H. Pacheco. Towards a framework for multi-directional model transformations. In the proceedings of the 3rd International Workshop on Bidirectional Transformations (BX@EDBT/ICDT'14). CEUR Workshop Proceedings 1133. CEUR-WS, 2014.
2013
N. Macedo, T. Guimarães and A. Cunha. Model repair and transformation with Echo. In the proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE'13). IEEE, 2013. (tool demo) N. Macedo and A. Cunha. Implementing QVT-R bidirectional model transformations using Alloy. In the proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE@ETAPS'13). LNCS 7793. Springer, 2013. N. Macedo, H. Pacheco, A. Cunha and J. N. Oliveira. Composing least-change lenses. Electronic Communications of the EASST 57. EASST, 2013. (revised version of this pre-proceedings paper) N. Macedo, H. Pacheco, A. Cunha and J. N. Oliveira. Composing least-change lenses. Presented at the 2nd International Workshop on Bidirectional Transformations (BX@ETAPS'13). Rome, Italy, 2013. N. Macedo, H. Pacheco, A. Cunha and J. Voigtländer. A generic scheme and properties of bidirectional transformations. CoRR abs/1306.4473. arXiv, 2013.
< 2012
N. Macedo, H. Pacheco and A. Cunha. Relations as executable specifications: Taming partiality and non-determinism using invariants. In the proceedings of the 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS'12). LNCS 7650. Springer, 2012. (see this tech report for the appendices) N. Macedo, H. Pacheco and A. Cunha. Relations as executable specifications: Taming partiality and non-determinism using invariants. Technical Report TR-HASLab:03:2012. HASLab, 2012. (full version of this conference paper) N. Macedo and A. Cunha. Automatic unbounded verification of Alloy specifications with Prover9. CoRR abs/1209.5773. arXiv, 2011. N. Macedo. Translating Alloy specifications to the point-free style. MSc Thesis, Universidade do Minho, Portugal, 2010.