publicações selecionadas
-
artigo académico
- Tourism-Led Change of the City Centre. Land. 2024
- Urban Rehabilitation and Tourism: Lessons from Porto (2010–2020) 2023
- A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3. Journal of Logical and Algebraic Methods in Programming. 2023
- A tribute to José Manuel Valença. Journal of Logical and Algebraic Methods in Programming. 2022
- Assessment of electromagnetic tracking systems in a surgical environment using ultrasonography and ureteroscopy instruments for percutaneous renal access 2019
- Culture and Tourism in Porto City Centre: Conflicts and (Im)Possible Solutions 2019
- Gentrification in Porto: floating city users and internationally-driven urban change. Urban Geography. 2019
- Gentrification in Porto: problems and opportunities in the past and in the future of an internationally open city. GOT - Geography and Spatial Planning Journal. 2018
- Formal verification of side-channel countermeasures using self-composition. International Journal on Software Tools for Technology Transfer. 2013
- TV WPN : programa de cálculo automático para análise da vulnerabilidade de redes de abastecimento de água. Águas & Resíduos. 2012
- Assertion-based slicing and slice graphs. Formal Aspects of Computing. 2012
- CAOVerif: An open-source deductive verification platform for cryptographic software implementations. International Journal on Software Tools for Technology Transfer. 2012
- Risco de cenários de dano vulneráveis de redes de abastecimento de água. Territorium. 2012
- Verification conditions for single-assignment programs. Proceedings of the ACM Symposium on Applied Computing. 2012
- GammaPolarSlicer. Computer Science and Information Systems. 2011
- Verification conditions for source-level imperative programs. Computer Science Review. 2011
- Sistemas de abastecimento de água - Avaliação da vulnerabilidade. Recursos Hídricos. 2010
- Deductive verification of cryptographic software. Innovations in Systems and Software Engineering. 2010
- Safe integration of annotated components in open source projects. Electronic Communications of the EASST. 2010
- Verifying cryptographic software correctness with respect to reference implementations. International Journal on Software Tools for Technology Transfer. 2009
- A Tool for Programming with Interaction Nets. Electronic Notes in Theoretical Computer Science. 2008
- Token-passing Nets for Functional Languages. Electronic Notes in Theoretical Computer Science. 2008
- A Local Graph-rewriting System for Deciding Equality in Sum-product Theories. Electronic Notes in Theoretical Computer Science. 2007
- Recursion patterns and time-analysis. ACM SIGPLAN Notices. 2005
-
artigo de conferência
- Pode o turismo matar uma cidade? Um postal de Veneza para o Porto 2019
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. International Journal on Software Tools for Technology Transfer. 2016
- A Bounded Model Checker for SPARK Programs. International Journal on Software Tools for Technology Transfer. 2014
- Interactive verification of safety-critical software. Proceedings International Computer Software and Applications Conference. 2013
- Study of retention-treatment basins in highways: case study of A24 (northern Portugal) 2011
- Avaliação da vulnerabilidade de redes de abastecimento de água 2010
- GamaSlicer: An online laboratory for program verification and analysis 2010
- Teoria da vulnerabilidade de redes hidráulicas de abastecimento de água (TVRHAA) 2009
- A framework for point-free program transformation. International Journal on Software Tools for Technology Transfer. 2006
-
capítulo de livro
-
documento
- Why3-do: The way of harmonious distributed system proofs. International Journal on Software Tools for Technology Transfer. 2022
- A deductive reasoning approach for database applications using verification conditions. Journal of Systems and Software. 2021
- Real-time MTL with durations as SMT with applications to schedulability analysis 2020
- Testing for race conditions in distributed systems via smt solving. International Journal on Software Tools for Technology Transfer. 2020
- A generalized program verification workflow based on loop elimination and SA form. FME Workshop on Formal Methods in Software Engineering. 2019
- A generalized approach to verification condition generation. Proceedings International Computer Software and Applications Conference. 2018
- K-Taint: an executable rewriting logic semantics for taint analysis in the K framework 2018
- Runtime verification of autopilot systems using a fragment of MTL-∫. International Journal on Software Tools for Technology Transfer. 2018
- SMT-based schedulability analysis using RMTL-∫. ACM SIGBED Review. 2017
- Formal verification with Frama-C: a case study in the space software domain. IEEE Transactions on Reliability. 2016
- Monitoring for a decidable fragment of MTL-∫. International Journal on Software Tools for Technology Transfer. 2015
- Logic-based schedulability analysis for compositional hard real-time embedded systems. ACM SIGBED Review. 2015
- Studying verification conditions for imperative programs. Electronic Communications of the EASST. 2015
- A compositional monitoring framework for hard real-time systems. International Journal on Software Tools for Technology Transfer. 2014
- Formal verification of kLIBC with the WP frama-C plug-in. International Journal on Software Tools for Technology Transfer. 2014
- Towards a runtime verification framework for the Ada Programming Language. International Journal on Software Tools for Technology Transfer. 2014
- Experimenting with predicate abstraction 2013
- SPARK-BMC: checking SPARK code for bugs 2013
- Towards a mostly-automated prover for bit-vector arithmetic 2013
- Using abstract interpretation to produce dependable aerospace control software 2013
- A case study on model checking and deductive verification techniques of safety-critical software 2012
- An approach to model checking Ada programs. International Journal on Software Tools for Technology Transfer. 2012
- Towards specification and verification frameworks for concurrent real-time systems 2012
- Using term rewriting to solve bit-vector arithmetic problems (Poster presentation). International Journal on Software Tools for Technology Transfer. 2012
- A visual inspector for Boogie programs 2011
- Formal verification of side channel countermeasures using self-composition. International Journal on Software Tools for Technology Transfer. 2011
- Risco de cenários de dano vulneráveis de redes de abastecimento de água. Territorium. 2011
- A deductive verification platform for cryptographic software. Electronic Communications of the EASST. 2010
- Contract-based slicing helps on safety reuse 2010
- Model-checking temporal properties of real-time HTL programs. International Journal on Software Tools for Technology Transfer. 2010
- Program verification in SPARK and ACSL : a comparative case study. International Journal on Software Tools for Technology Transfer. 2010
- Sistemas de abastecimento de água: avaliação da vulnerabilidade 2010
- Code analysis: past and present 2009
- Iterators and interaction 2009
- A comparative study of verification condition generators 2008
- Deriving Sorting Algorithms 2008
- Properties preservation during transformation 2008
- Visual programming with Interaction Nets. International Journal on Software Tools for Technology Transfer. 2008
- A higher-order calculus for graph transformation. Electronic Notes in Theoretical Computer Science. 2007
- Visual programming with recursion patterns in interaction nets. Electronic Communications of the EASST. 2007
- A local graph-rewriting system for deciding equality in sum-product theories 2006
- Lissom, a source level proof carrying code platform 2006
- Down with variables 2005
- Functional programming and program transformation with interaction nets 2005
- Point-free program transformation. Fundamenta Informaticae. 2005
- Generalizing Hylo-shift 2004
- Making the point-free calculus less pointless 2004
- Point-free program transformation 2004
- Weak reduction and garbage collection in interaction nets. Electronic Notes in Theoretical Computer Science. 2003
- Encoding linear logic with interaction combinators. Information and Computation. 2002
- Combining interaction nets with externally defined programs 2001
- Parallel evaluation of interaction nets with MPINE. International Journal on Software Tools for Technology Transfer. 2001
- Parallel implementation models for the lambda-calculus using the geometry of interaction. International Journal on Software Tools for Technology Transfer. 2001
- Guiões das aulas práticas laboratoriais sobre o sistema COQ 1998
- Introdução ao sistema COQ de assistência à prova 1998
- Using Internet technology for course support. Sigcse Bulletin (association for Computing Machinery, Special Interest Group on Computer Science Education). 1996
-
livro