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.
Full Professor at INESC TEC, Univ. Minho.
Full Professor at INESC TEC, Univ. Minho, and INL.
Associate professor at INESC TEC, Univ. Minho.
Associate professor at INESC TEC, Univ. Minho.
Associate professor at INESC TEC, Univ. Minho
Auxiliar professor at INESC TEC, Univ. Minho.
Auxiliar professor at INESC TEC, Univ. Minho
PhD student at INESC TEC and Univ. Minho.
PhD student at University of Aveiro.
PhD student at INESC TEC and Univ. Minho.
PhD researcher at INESC TEC, Univ. Minho.
Post-Doc at CISTER
Assistant professor at CIDMA.
Associate professor at Univ. Aveiro.
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.
M.D. Harrison, P. Masci, and J.C. Campos. Balancing the formal and the informal in user centred design. Interacting with Computers, 33(1):55--72, January 2021. [ bib | DOI ]
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 ]
Dirk Hofmann, Renato Neves, and Pedro Nora. Limits in categories of vietoris coalgebras. Math. Struct. Comput. Sci., 29(4):552--587, 2019. [ bib | DOI | http ]
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 ]
Renato Neves and Luís Soares Barbosa. Languages and models for hybrid automata: A coalgebraic perspective. Theor. Comput. Sci., 744:113--142, 2018. [ 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.
(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.