publicações selecionadas
-
artigo académico
- Tourism-Led Change of the City Centre. Land. 2024
- Gentrification in Porto: floating city users and internationally-driven urban change. Urban Geography. 2019
- Assessment of electromagnetic tracking systems in a surgical environment using ultrasonography and ureteroscopy instruments for percutaneous renal access 2019
- TV WPN : programa de cálculo automático para análise da vulnerabilidade de redes de abastecimento de água. Águas & Resíduos. 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
- Sistemas de abastecimento de água - Avaliação da vulnerabilidade. Recursos Hídricos. 2010
- Verifying cryptographic software correctness with respect to reference implementations. Computational Methods in Applied Sciences. 2009
-
artigo de conferência
- Why3-do: The way of harmonious distributed system proofs. Computational Methods in Applied Sciences. 2022
- Real-time MTL with durations as SMT with applications to schedulability analysis 2020
- Testing for race conditions in distributed systems via smt solving. Computational Methods in Applied Sciences. 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
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. Computational Methods in Applied Sciences. 2016
- Monitoring for a decidable fragment of MTL-∫. Computational Methods in Applied Sciences. 2015
- A Bounded Model Checker for SPARK Programs. Computational Methods in Applied Sciences. 2014
- A compositional monitoring framework for hard real-time systems. Computational Methods in Applied Sciences. 2014
- Formal verification of kLIBC with the WP frama-C plug-in. Computational Methods in Applied Sciences. 2014
- Towards a runtime verification framework for the Ada Programming Language. Computational Methods in Applied Sciences. 2014
- Interactive verification of safety-critical software. Proceedings International Computer Software and Applications Conference. 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. Computational Methods in Applied Sciences. 2012
- Using term rewriting to solve bit-vector arithmetic problems (Poster presentation). Computational Methods in Applied Sciences. 2012
- Study of retention-treatment basins in highways: case study of A24 (northern Portugal) 2011
- A visual inspector for Boogie programs 2011
- Avaliação da vulnerabilidade de redes de abastecimento de água 2010
- Contract-based slicing helps on safety reuse 2010
- GamaSlicer: An online laboratory for program verification and analysis 2010
- Model-checking temporal properties of real-time HTL programs. Computational Methods in Applied Sciences. 2010
- Program verification in SPARK and ACSL : a comparative case study. Computational Methods in Applied Sciences. 2010
- Teoria da vulnerabilidade de redes hidráulicas de abastecimento de água (TVRHAA) 2009
- Code analysis: past and present 2009
- Iterators and interaction 2009
- Properties preservation during transformation 2008
- Visual programming with Interaction Nets. Computational Methods in Applied Sciences. 2008
- Visual programming with recursion patterns in interaction nets. Electronic Communications of the EASST. 2007
- A framework for point-free program transformation. Computational Methods in Applied Sciences. 2006
- A local graph-rewriting system for deciding equality in sum-product theories 2006
- Making the point-free calculus less pointless 2004
- Combining interaction nets with externally defined programs 2001
- Parallel evaluation of interaction nets with MPINE. Computational Methods in Applied Sciences. 2001
- Parallel implementation models for the lambda-calculus using the geometry of interaction. Computational Methods in Applied Sciences. 2001
- Using Internet technology for course support. Sigcse Bulletin (association for Computing Machinery, Special Interest Group on Computer Science Education). 1996
-
artigo de revista
- Urban Rehabilitation and Tourism: Lessons from Porto (2010–2020). Sustainability (MDPI). 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 deductive reasoning approach for database applications using verification conditions. Journal of Systems and Software. 2021
- Runtime verification of autopilot systems using a fragment of MTL-∫. Computational Methods in Applied Sciences. 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
- 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
- Formal verification of side-channel countermeasures using self-composition. Computational Methods in Applied Sciences. 2013
- Assertion-based slicing and slice graphs. Formal Aspects of Computing. 2012
- CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Computational Methods in Applied Sciences. 2012
- Formal verification of side channel countermeasures using self-composition. Computational Methods in Applied Sciences. 2011
- GammaPolarSlicer. Computer Science and Information Systems. 2011
- Verification conditions for source-level imperative programs. Computer Science Review. 2011
- A deductive verification platform for cryptographic software. Electronic Communications of the EASST. 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
- 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
- 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
- Point-free program transformation. Fundamenta Informaticae. 2005
- Recursion patterns and time-analysis. ACM SIGPLAN Notices. 2005
- 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
-
capítulo de livro
-
documento
- Experimenting with predicate abstraction 2013
- SPARK-BMC: checking SPARK code for bugs 2013
- Towards specification and verification frameworks for concurrent real-time systems 2012
- Risco de cenários de dano vulneráveis de redes de abastecimento de água 2011
- Sistemas de abastecimento de água: avaliação da vulnerabilidade 2010
- A comparative study of verification condition generators 2008
- Deriving Sorting Algorithms 2008
- Guiões das aulas práticas laboratoriais sobre o sistema COQ 1998
- Introdução ao sistema COQ de assistência à prova 1998
-
livro
-
poster de conferência
-
relatório