We are a research group on theoretical computer science and formal methods. Our core topics are:
We have a long scientific tradition, significant links to national industry, and a deep involvement in teaching activities. We also have an extensive track record on attracting competitive funds from different agencies.
If you are interested in working with us do get in touch!! The summing picture of all our research is given by the diagram below - which every computer scientist knows.
We are part of HASLab, a software laboratory at University of Minho associated to INESC TEC. We are also articulated with the research group Quantum and Linear-Optical Computation Group, hosted by INL, the International Iberian Nanotechnology Laboratory.
Fredrik Dahlqvist and Renato Neves. An internal language for categories enriched over generalised metric spaces. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 16:1--16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. [ bib | DOI | http ]
J.C. Campos, C. Fayollas, M.D. Harrison, C. Martinie, P. Masci, and P. Palanque. Supporting the analysis of safety critical user interfaces: an exploration of three formal tools. ACM Transactions on Computer-Human Interaction, 27(5), August 2020. [ bib | DOI | .pdf ]
Sergey Goncharov, Renato Neves, and José Proença. Implementing hybrid semantics: From functional to imperative. In Ka I Pun, Adenilso da Silva Simão, and Volker Stolz, editors, Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau S.A.R., China, October 31 - November 30, 2020, Proceedings, volume 12545 of Lecture Notes in Computer Science. Springer, 2020. [ bib | .pdf ]
M.D. Harrison, P. Masci, and J.C. Campos. Verification templates for the analysis of user interface software design. IEEE Transactions on Software Engineering, 45(8):802--822, August 2019. [ bib | DOI | .pdf ]
Sergey Goncharov, Julian Jakob, and Renato Neves. A semantics for hybrid iteration. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China, volume 118 of LIPIcs, pages 22:1--22:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. [ bib | DOI | http ]
J.C. Campos, M. Sousa, M. Alves, and M.D. Harrison. Formal verification of a space system's user interface with the ivy workbench. IEEE Transactions on Human-Machine Systems, 46(2):303--316, 2016. [ bib | DOI | .pdf ]
This file was generated by bibtex2html 1.99.
C. Silva, J. Vieira, J.C. Campos, R. Couto, and A.N. Ribeiro. Development and validation of a descriptive cognitive model for a low code development platform. Human Factors, 63(6):1012--1032, 2021. [ bib | DOI ]
A. Canny, D. Navarre, J.C. Campos, and P. Palanque. Model-based testing of post-wimp interactions using petri-nets. In E. Sekerinski et al., editor, Formal Methods. FM 2019 International Workshops, volume 12232 of Lecture Notes in Computer Science, pages 486--502. Springer, 2020. [ bib | DOI ]
Sergey Goncharov and Renato Neves. An adequate while-language for hybrid computation. In Ekaterina Komendantskaya, editor, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019, Porto, Portugal, October 7-9, 2019, pages 11:1--11:15. ACM, 2019. [ bib | DOI | http ]
This file was generated by bibtex2html 1.99.
Lince - Modelling and and simulation of hybrid programs.
IFTA: Interface Featured Timed Automata - Implementation of the Interface Featured Timed Automata (IFTA).
QWAK: Quantum Walk Analysis Kit - Python package and GUI for simulating continuous-time quantum walks.
IVY workbench - A model based tool for the analysis of interactive systems designs.
Quantitative methods for cyber-physical programming; Started in 2022.
Distributed Architectures: Variability and Interaction for Cyber-Physical Systems; 2018-2022.
Coalgebraic Modeling and Analysis for Computational Synthetic Biology; 2018-2021
Dynamic logics for cyber-physical systems; 2016–2018.
Trustworthy Software Design with Alloy; 2016–2018.
Lightweight computation for networks at the edge; 2017–2020.
(P2020 NORTE-45-2015-23) Harnessing EGOV for smart governance: Foundations and tools, since May, 2016.
Here is a selection of possible projects for M.Sc. students that would like to work with us. We are also open for discussion about other topics. Note that we have a few grants that can pay for most of the ideas presented in these projects. If you are interested, just come and talk to us.