publicações selecionadas
-
artigo académico
- Formally verifying Kyber Episode IV: Implementation correctness. IACR Transactions on Cryptographic Hardware and Embedded System. 2023
- A formal treatment of the role of verified compilers in secure computation. Journal of Logical and Algebraic Methods in Programming. 2022
- Teaching How to Program using Automated Assessment and Functional Glossy Games (Experience Report). Proceedings of the ACM on Programming Languages. 2018
- Formalization of the Pumping Lemma for Context-Free Languages. Journal of Formalized Reasoning. 2016
- Formal verification of side-channel countermeasures using self-composition. International Journal on Software Tools for Technology Transfer. 2013
- CAOVerif: An open-source deductive verification platform for cryptographic software implementations. International Journal on Software Tools for Technology Transfer. 2012
- Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. IACR Cryptology ePrint Archive. 2012
- Real-time dynamic monochromatic ocular wavefront aberrations during accommodation: Preliminary results. 2012 IEEE 2nd Portuguese Meeting in Bioengineering, ENBENG 2012. 2012
- Partial derivative automata formalized in coq. International Journal on Software Tools for Technology Transfer. 2011
- A certifying compiler for zero-knowledge proofs of knowledge based on ¿-protocols. International Journal on Software Tools for Technology Transfer. 2010
- Deductive verification of cryptographic software. Innovations in Systems and Software Engineering. 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
- Equivalences between refractive index and equilibrium water content of conventional and silicone hydrogel contact lenses from automated and manual refractometry. Journal of Biomedical Materials Research: Part B. 2007
- Technical Note: Accuracy and repeatability of a new portable ultrasound pachymeter. Ophthalmic and Physiological Optics. 2007
- Age differences in central and peripheral intraocular pressure using a rebound tonometer. British Journal of Ophthalmology. 2006
- Refractive index and equilibrium water content of conventional and silicone hydrogel contact lenses. Ophthalmic and Physiological Optics. 2006
- The influence of cycloplegia in objective refraction. Investigative Ophthalmology & Visual Science. 2005
- A comparison of the ARK-700A autokeratometer and Medmont E300 corneal topographer when measuring peripheral corneal curvatura. Ophthalmic and Physiological Optics. 2004
- Bounded version vectors. International Journal on Software Tools for Technology Transfer. 2004
-
artigo de conferência
- Leakage-Free Probabilistic Jasmin Programs 2025
- Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt 2024
- Verified Password Generation from Password Composition Policies. International Journal on Software Tools for Technology Transfer. 2022
- Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. Proceedings of the ACM Conference on Computer and Communications Security. 2021
- Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. International Journal on Software Tools for Technology Transfer. 2020
- A Machine-Checked Proof of Security for AWS Key Management Service 2019
- Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3 2019
- Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages. Electronic Notes in Theoretical Computer Science. 2019
- Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks. Proceedings IEEE Computer Security Foundations Symposium. 2018
- A Fast and Verified Software Stack for Secure Function Evaluation. Proceedings of the ACM Conference on Computer and Communications Security. 2017
- Jasmin: High-Assurance and High-Speed Cryptography. Proceedings of the ACM Conference on Computer and Communications Security. 2017
- On the Formalization of Some Results of Context-Free Language Theory. International Journal on Software Tools for Technology Transfer. 2016
- Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. International Journal on Software Tools for Technology Transfer. 2016
- Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations. Proceedings of the ACM Conference on Computer and Communications Security. 2013
- Imaging of aphakic intraocular lens with a slit-scanning tomography system. Proceedings of SPIE. 2012
- A new optical system for 3-dimensional mapping of the cornea 2007
- Within and between session repeatability of topographic data using medmont E-300 corneal topographer 2005
- Topographical changes in anterior corneal curvature after LASIK 2004
-
documento
- The last mile: High-Assurance and High-Speed cryptographic implementations. IEEE Symposium on Security and Privacy. 2020
- Verifying constant-time implementations 2016
- Do consentimento para a utilização de testemunhos de conexão (cookies) 2016
- Crystalline lens imaging with a slit-scanning system 2011
- Formal verification of side channel countermeasures using self-composition. International Journal on Software Tools for Technology Transfer. 2011
- Analysis of surface mechanical properties of unworn and worn silicone hydrogel contact lenses using nanoindentation with AFM 2010
- Surface AFM microscopy of unworn and worn samples of silicone hydrogel contact lenses. Journal of Biomedical Materials Research: Part B. 2009
- Deriving Sorting Algorithms 2008
- Symptoms in a population of contact lens and noncontact lens wearers under different environmental conditions. Investigative Ophthalmology & Visual Science. 2007
- Accuracy and repeatability of a new portable ultrasound pachymeter. Ophthalmic and Physiological Optics. 2007
- Qualitative and quantitative characterization of the in vitro dehydration process of hydrogel contact lenses. Journal of Biomedical Materials Research: Part B. 2007
- CORRELATIONS BETWEEN CORNEAL BIOMECHANICAL PROPERTIES MEASURED WITH THE OCULAR RESPONSE ANALYZER AND ICARE REBOUND TONOMETRY 2007
- Differences in ametropia prevalence obtained different methods of refraction 2006
- The short-term effects of contact lens corneal refractive therapy on corneal topography 2006
- Correlations between central and peripheral changes in anterior corneal topography after myopic LASIK and their implications in postsurgical contact lens fitting. Eye & Contact Lens: Science and Clinical Practice. 2006
- Soft contact lenses for keratoconus: case report. Eye & Contact Lens: Science and Clinical Practice. 2006
- Accuracy and repeatability of a new portable ultrasound pachymeter 2006
- Relationship between central and peripheral iop as measured with icare rebound tonometer : clinical implications 2006
- Microscopic observation of unworn siloxane-hydrogel soft contact lenses by atomic force microscopy. Journal of Biomedical Materials Research: Part B. 2006
- Microscopic observations of superficial ultrastructure of unworn siloxane-hydrogel contact lenses by cryo-scanning electron microscopy. Journal of Biomedical Materials Research: Part B. 2006
- Oxygen transmissibility of piggyback systems with conventional soft and silicone hydrogel contact lenses. Cornea. 2006
- A local graph-rewriting system for deciding equality in sum-product theories 2006
- DIFFERENCES IN CENTRAL AND PERIPHERAL TONOMETRY WITH ICARE® REBOUND TONOMETRY AS A FUNCTION OF AGE 2006
- Differences in Central and Peripheral Tonometry with ICare Rebound Tonometry as a Function of Age 2006
- NON-CONTACT TONOMETRY SYNCHRONIZED WITH CARDIAC RHYTHM AND ITS RELATIONSHIPS WITH BLOOD PRESSURE 2006
- Programming matrix optics into mathematica. Optik. 2005
- Wavefront and ray-density plots using seventh-order matrices. Optik. 2005
- Prospective Study on the Prevalence of Refractive Conditions in the North of Portugal 2005
- Refractive error changes in young adults during a period of 3 years 2005
- Retinoscopy/autorefraction : which is the best starting point for a noncycloplegic refraction?. Investigative Ophthalmology & Visual Science. 2005
- Within and Between Session Repeatability of Topographic Data Using Medmont E-300 Corneal Topographer 2005
- The AC/A ratio in university students in Portugal 2004
- The influence of the cycloplegic in the objective refraction 2004
- The prevalence of refractive errors in university students in Portugal 2004
- Topographical changes in anterior corneal curvature after LASIK 2004
- Variations in ocular biometry in university students in portugal 2004
- Wigner distribution transformations in high-order systems. Journal of Computational and Applied Mathematics. 2003
- Wide angle near-field diffraction and Wigner distribution. Optik. 2003
- Clinical performance Nidek Ark 700A autofractor 2003
- Where does ARK-700A actually measures peripheral corneal curvature? A comparison with medmont videokeratoscope 2003
- Measuring corneal pachymetry with a rotary scanning system. Journal of Refractive Surgery. 2000
-
livro