corpus.blog
41554 blogs · [ { "id": "01a0878e-a06d-70ba-9b50-31a974e470a7", "title": "An Empirical Study of Policy as Code: Adoption, Purpose, and Maintenance", "url": "https://joaoff.com/publication/2026/msr/", "published_at": "2026-04-13T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a975838b4d", "title": "ProfOlaf: Semi-Automated Tool for Systematic Literature Reviews", "url": "https://joaoff.com/publication/2026/fse/", "published_at": "2026-03-17T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9759d9ecd", "title": "The Ultimate Configuration Management Tool? Lessons from a Mixed Methods Study of Ansible's Challenges", "url": "https://joaoff.com/publication/2026/ease/", "published_at": "2026-03-13T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9766ebc1d", "title": "Vibenix: An AI Assistant for Software Packaging with Nix", "url": "https://joaoff.com/publication/2026/last-x/", "published_at": "2026-02-27T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9772e8b43", "title": "ICSE 2020 paper is the most cited according to 2025 Scholar Metrics", "url": "https://joaoff.com/2025/07/25/icse-2020-paper-is-the-most-cited-according-to-2025-scholar-metrics/", "published_at": "2025-07-25T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a977384ba0", "title": "Awarded an Amazon Research Award on Automated Reasoning!", "url": "https://joaoff.com/2025/06/03/awarded-an-amazon-research-award-on-automated-reasoning/", "published_at": "2025-06-03T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a977dcdf0b", "title": "Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification", "url": "https://joaoff.com/publication/2025/icse/", "published_at": "2025-04-27T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97873b49e", "title": "InfraFix: Technology-Agnostic Repair of Infrastructure as Code", "url": "https://joaoff.com/publication/2025/issta/", "published_at": "2025-04-11T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97958038d", "title": "ACM SIGSOFT Distinguished Paper Award at ICSE 2025", "url": "https://joaoff.com/2025/04/03/acm-sigsoft-distinguished-paper-award-at-icse-2025/", "published_at": "2025-04-03T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a979c95c7e", "title": "Do Experts Agree About Smelly Infrastructure?", "url": "https://joaoff.com/publication/2025/tse/", "published_at": "2025-03-19T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97a7abc21", "title": "InfraGov: New Funded Project on Reliable and Secure IT Infrastructure", "url": "https://joaoff.com/2025/03/01/infragov-new-funded-project-on-reliable-and-secure-it-infrastructure/", "published_at": "2025-03-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97b572a2b", "title": "Contract Usage and Evolution in Android Mobile Applications", "url": "https://joaoff.com/publication/2025/ecoop/", "published_at": "2025-02-28T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97b58ed15", "title": "CoqPyt: Proof Navigation in Python in the Era of LLMs", "url": "https://joaoff.com/publication/2024/fse-coqpyt/", "published_at": "2024-04-16T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97c01795e", "title": "How are Contracts Used in Android Mobile Applications?", "url": "https://joaoff.com/publication/2024/icse-poster-contracts/", "published_at": "2024-04-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97c5d109d", "title": "Evolution of automated weakness detection in Ethereum bytecode: a comprehensive study", "url": "https://joaoff.com/publication/2024/emse/", "published_at": "2024-01-02T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97d1481d4", "title": "AI for Formal Verification", "url": "https://joaoff.com/project/ai-for-formal-verification/", "published_at": "2024-01-02T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97d992556", "title": "Leveraging Large Language Models to Boost Dafny's Developers Productivity", "url": "https://joaoff.com/publication/2024/formalise/", "published_at": "2024-01-02T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97dcaa45a", "title": "DifFuzzAR: automatic repair of timing side-channel vulnerabilities via refactoring", "url": "https://joaoff.com/publication/2024/jase/", "published_at": "2024-01-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97deb6d93", "title": "Polyglot Code Smell Detection for Infrastructure as Code with GLITCH", "url": "https://joaoff.com/publication/2023/ase-glitch/", "published_at": "2023-07-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97dfbab82", "title": "SmartBugs 2.0: An Execution Framework for Weakness Detection in Ethereum Smart Contracts", "url": "https://joaoff.com/publication/2023/ase-smartbugs2/", "published_at": "2023-07-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97dfc463c", "title": "Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution", "url": "https://joaoff.com/publication/2023/ecoop/", "published_at": "2023-05-12T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97e88214e", "title": "MUFIN: Improving Neural Repair Models with Back-Translation", "url": "https://joaoff.com/publication/2023/mufin/", "published_at": "2023-04-05T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97e9090d6", "title": "bGSL: An Imperative Language for Specification and Refinement of Backtracking Programs", "url": "https://joaoff.com/publication/2022/jlamp/", "published_at": "2022-08-01T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a97f8aef17", "title": "GLITCH: Automated Polyglot Security Smell Detection in Infrastructure as Code", "url": "https://joaoff.com/publication/2022/ase/", "published_at": "2022-07-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a980450773", "title": "Extending EcoAndroid with Automated Detection of Resource Leaks", "url": "https://joaoff.com/publication/2022/mobilesoft/", "published_at": "2022-05-14T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a980c3f632", "title": "Verified password generation from password composition policies", "url": "https://joaoff.com/publication/2022/ifm/", "published_at": "2022-05-07T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a980fc4ab5", "title": "A Preliminary Study on Generating Well-Formed Q# Quantum Programs for Fuzz Testing", "url": "https://joaoff.com/publication/2022/aist/", "published_at": "2022-04-04T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a981145340", "title": "Reliable DevOps", "url": "https://joaoff.com/project/reliable-devops/", "published_at": "2022-02-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98153ee8a", "title": "EcoAndroid: An Android Studio Plugin for Developing Energy-efficient Java Mobile Applications", "url": "https://joaoff.com/publication/2021/qrs/", "published_at": "2021-12-07T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9819d0458", "title": "Exploring Usable Security to Improve the Impact of Formal Verification: A Research Agenda", "url": "https://joaoff.com/publication/2021/appfm/", "published_at": "2021-11-23T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9829019b7", "title": "Formal Methods Teaching: 4th International Workshop and Tutorial (FMTea 2021)", "url": "https://joaoff.com/publication/2021/fmtea/", "published_at": "2021-11-23T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98353a161", "title": "Automatic Repair of Java Code with Timing Side-Channel Vulnerabilities", "url": "https://joaoff.com/publication/2021/iwor/", "published_at": "2021-11-10T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98429ecc5", "title": "Towards Improving the Usability of Password Managers", "url": "https://joaoff.com/publication/2021/inforum/", "published_at": "2021-09-10T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a984e59398", "title": "Automated narrative planning model extension", "url": "https://joaoff.com/publication/2021/jaamas/", "published_at": "2021-05-07T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98570aa4c", "title": "SmartBugs: A Framework to Analyze Solidity Smart Contracts", "url": "https://joaoff.com/publication/2020/ase/", "published_at": "2020-08-07T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9866fd571", "title": "Evaluating the Accuracy of Password Strength Meters using Off-The-Shelf Guessing Attacks", "url": "https://joaoff.com/publication/2020/rsda/", "published_at": "2020-08-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a986e27de4", "title": "Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts", "url": "https://joaoff.com/publication/2020/icse/", "published_at": "2020-05-23T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a986f71a02", "title": "Teaching", "url": "https://joaoff.com/teaching/", "published_at": "2020-03-12T00:00:59+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a987f321dc", "title": "SmartBugs: An Execution Framework for Automated Analysis of Smart Contracts", "url": "https://joaoff.com/2020/03/05/smartbugs-an-execution-framework-for-automated-analysis-of-smart-contracts/", "published_at": "2020-03-05T10:17:30+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a988d009d0", "title": "Skeptic: Automatic, Justified and Privacy-Preserving Password Composition Policy Selection", "url": "https://joaoff.com/publication/2020/asiaccs/", "published_at": "2020-02-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a989a16175", "title": "Smartbugs", "url": "https://joaoff.com/project/smartbugs/", "published_at": "2020-02-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a989dd3982", "title": "Extending Narrative Planning Domains with Linguistic Resources", "url": "https://joaoff.com/publication/2020/aamas/", "published_at": "2020-01-15T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98a56967d", "title": "Narrative Planning Model Acquisition from Text Summaries and Descriptions", "url": "https://joaoff.com/publication/2020/aaai/", "published_at": "2020-01-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98b17e8d6", "title": "Research Opportunities", "url": "https://joaoff.com/opportunities/", "published_at": "2019-12-26T13:27:59+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98b999ce1", "title": "Logic, Algebra, and Geometry at the Foundation of Computer Science", "url": "https://joaoff.com/publication/2019/fmtea/", "published_at": "2019-08-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98bf76655", "title": "Lost in Disclosure: On The Inference of Password Composition Policies", "url": "https://joaoff.com/publication/2019/rsda/", "published_at": "2019-08-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98c023b98", "title": "Open and Interactive Learning Resources for Algorithmic Problem Solving", "url": "https://joaoff.com/publication/2019/opencert/", "published_at": "2019-08-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98ce574d4", "title": "GPS+: Reasoning About Fences and Relaxed Atomics", "url": "https://joaoff.com/publication/2018/ijpp/", "published_at": "2018-12-01T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98d69d263", "title": "Towards a Program Logic for C11 Release-Sequences", "url": "https://joaoff.com/publication/2018/tase/", "published_at": "2018-07-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98dead74d", "title": "Towards Verified Handwritten Calculational Proofs", "url": "https://joaoff.com/publication/2018/itp/", "published_at": "2018-07-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98ea85ac1", "title": "Certified Password Quality: A Case Study Using Coq and Linux Pluggable Authentication Modules", "url": "https://joaoff.com/publication/2017/ifm/", "published_at": "2017-09-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98ef7ed2f", "title": "Framer: Planning Models from Natural Language Action Descriptions", "url": "https://joaoff.com/publication/2017/icaps/", "published_at": "2017-09-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a98fdcebcc", "title": "ReqCap: Hierarchical Requirements Modeling and Test Generation for Industrial Control Systems", "url": "https://joaoff.com/publication/2017/ret/", "published_at": "2017-09-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9908364ab", "title": "StoryFramer: From Input Stories to Output Planning Models", "url": "https://joaoff.com/publication/2017/keps/", "published_at": "2017-09-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a990e5a7b3", "title": "Towards a Constraints Approach to Generating Personalised Horror Film Variants", "url": "https://joaoff.com/publication/2017/coplas/", "published_at": "2017-09-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99108bac2", "title": "Visualization of Patient Behavior from Natural Language Recommendations", "url": "https://joaoff.com/publication/2017/kcap/", "published_at": "2017-09-11T11:32:32+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a991eb40b5", "title": "Password Security", "url": "https://joaoff.com/project/password-security/", "published_at": "2017-09-01T21:20:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a992ab8178", "title": "A calculational approach to path-based properties of the Eisenstein-Stern and Stern-Brocot trees via matrix algebra", "url": "https://joaoff.com/publication/2016/jlamp/", "published_at": "2016-08-01T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9935531db", "title": "Reasoning about Fences and Relaxed Atomics", "url": "https://joaoff.com/publication/2016/pdp/", "published_at": "2016-07-01T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9938ffa8e", "title": "Supporting Social Skills Rehabilitation with Virtual Storytelling", "url": "https://joaoff.com/publication/2016/flairs/", "published_at": "2016-07-01T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a993ffdb87", "title": "Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK", "url": "https://joaoff.com/publication/2014/sttt/", "published_at": "2014-11-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9941ec4e9", "title": "Structure Editing of Handwritten Mathematics: Improving the Computer Support for the Calculational Method", "url": "https://joaoff.com/publication/2014/its/", "published_at": "2014-11-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9945c41be", "title": "The Magic of Algorithm Design and Analysis: Teaching Algorithmic Skills using Magic Card Tricks", "url": "https://joaoff.com/publication/2014/iticse/", "published_at": "2014-06-23T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a994cb7669", "title": "Generative Story Worlds as Linear Logic Programs", "url": "https://joaoff.com/publication/2014/int7/", "published_at": "2014-06-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a994df42ca", "title": "Interactive Narratives", "url": "https://joaoff.com/project/computational-narratives/", "published_at": "2013-03-01T21:20:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a995cb11b3", "title": "The Algorithmics of Solitaire-Like Games (Extended Version)", "url": "https://joaoff.com/publication/2013/scp/", "published_at": "2013-02-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9965d7c7f", "title": "Linear logic programming for narrative generation", "url": "https://joaoff.com/publication/2013/lpnmr/", "published_at": "2013-01-06T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9970df09b", "title": "Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts", "url": "https://joaoff.com/publication/2013/icfem/", "published_at": "2013-01-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a997f91c37", "title": "Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK", "url": "https://joaoff.com/publication/2012/tase/", "published_at": "2012-11-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a998a92635", "title": "An Improved Proof of the Handshaking Lemma", "url": "https://joaoff.com/2011/09/20/an-improved-proof-of-the-handshaking-lemma/", "published_at": "2011-09-20T10:54:42+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9998b20f6", "title": "Principles and Applications of APS", "url": "https://joaoff.com/2011/06/02/principles-and-applications-of-aps/", "published_at": "2011-06-02T10:38:33+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99996d132", "title": "On Euclid's Algorithm and Elementary Number Theory", "url": "https://joaoff.com/publication/2011/scp/", "published_at": "2011-02-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99a3d44b0", "title": "Logic Training through Algorithmic Problem Solving", "url": "https://joaoff.com/publication/2011/ticttl/", "published_at": "2011-01-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99b1b75c2", "title": "Principles and Applications of Algorithmic Problem Solving", "url": "https://joaoff.com/publication/2010/thesis/", "published_at": "2010-12-06T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99c0fc1ab", "title": "Designing an Algorithmic Proof of the Two-Squares Theorem", "url": "https://joaoff.com/publication/2010/mpc/", "published_at": "2010-02-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99cabbaca", "title": "The Algorithmics of Solitaire-Like Games", "url": "https://joaoff.com/publication/2010/mpc-invited/", "published_at": "2010-02-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99d89d644", "title": "Probabilities in Proofreading", "url": "https://joaoff.com/2009/09/14/probabilities-in-proofreading/", "published_at": "2009-09-14T10:11:17+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99dda6ea7", "title": "Students' Feedback on Teaching Mathematics Through The Calculational Method", "url": "https://joaoff.com/publication/2009/fie/", "published_at": "2009-01-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99e793544", "title": "Which Mathematics for the Information Society?", "url": "https://joaoff.com/publication/2009/tfm/", "published_at": "2009-01-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a99f727bb9", "title": "Multiples in the Fibonacci Series", "url": "https://joaoff.com/2008/05/09/multiples-in-the-fibonacci-series/", "published_at": "2008-05-09T01:30:33+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a062e0d8", "title": "JFF7: An exercise from \"The Art of Computer Programming\"", "url": "https://joaoff.com/publication/jffs/jff7/", "published_at": "2008-02-28T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a085ad20", "title": "A Reward Check From Donald Knuth", "url": "https://joaoff.com/2008/02/25/a-reward-check-from-donald-knuth/", "published_at": "2008-02-25T16:31:01+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a09a2d79", "title": "A Square Grid Path Problem", "url": "https://joaoff.com/2008/01/20/a-square-grid-path-problem/", "published_at": "2008-01-20T15:59:49+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a100efbd", "title": "Recounting the Rationals: Twice!", "url": "https://joaoff.com/publication/2008/mpc/", "published_at": "2008-01-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a11bc5f3", "title": "JFF6: Resolução eficaz de problemas, quatro exemplos", "url": "https://joaoff.com/publication/jffs/jff6/", "published_at": "2008-01-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a1c5188f", "title": "JFF1: Exchanging the values of two variables", "url": "https://joaoff.com/publication/jffs/jff1/", "published_at": "2007-05-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a2249800", "title": "JFF0: Distributivity and the greatest common divisor", "url": "https://joaoff.com/publication/jffs/jff0/", "published_at": "2006-11-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a2e20202", "title": "JaSkel: A Java Skeleton-Based Framework for Structured Cluster and Grid Computing", "url": "https://joaoff.com/publication/2006/ccgrid/", "published_at": "2006-01-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a324462b", "title": "FM Education", "url": "https://joaoff.com/project/fm-education/", "published_at": "2006-01-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a3ea8372", "title": "A contribution towards a Distributed Java Virtual Machine", "url": "https://joaoff.com/publication/2005/contributiondistjvm/", "published_at": "2005-11-01T00:00:00+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a4defdec", "title": "ParC#: Parallel Computing with C# in .NET", "url": "https://joaoff.com/publication/2005/pact/", "published_at": "2005-09-05T09:35:12+00:00" }, { "id": "01a0878e-a06d-70ba-9b50-31a9a54b60d2", "title": "Camila Revival: VDM meets Haskell", "url": "https://joaoff.com/publication/2005/overture/", "published_at": "2005-07-05T09:35:12+00:00" } ] posts Claim your blog
Back to joaoff.com
Blog · corpus.blog/blogs/joaoff.com/posts

joaoff.com

joaoff.com

2026

An Empirical Study of Policy as Code: Adoption, Purpose, and Maintenanceoriginal ↗
13 Apr 2026
ProfOlaf: Semi-Automated Tool for Systematic Literature Reviewsoriginal ↗
17 Mar 2026
The Ultimate Configuration Management Tool? Lessons from a Mixed Methods Study of Ansible's Challengesoriginal ↗
13 Mar 2026
Vibenix: An AI Assistant for Software Packaging with Nixoriginal ↗
27 Feb 2026

2025

ICSE 2020 paper is the most cited according to 2025 Scholar Metricsoriginal ↗
25 Jul 2025
Awarded an Amazon Research Award on Automated Reasoning!original ↗
3 Jun 2025
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationoriginal ↗
27 Apr 2025
InfraFix: Technology-Agnostic Repair of Infrastructure as Codeoriginal ↗
11 Apr 2025
ACM SIGSOFT Distinguished Paper Award at ICSE 2025original ↗
3 Apr 2025
Do Experts Agree About Smelly Infrastructure?original ↗
19 Mar 2025
InfraGov: New Funded Project on Reliable and Secure IT Infrastructureoriginal ↗
1 Mar 2025
Contract Usage and Evolution in Android Mobile Applicationsoriginal ↗
28 Feb 2025

2024

CoqPyt: Proof Navigation in Python in the Era of LLMsoriginal ↗
16 Apr 2024
How are Contracts Used in Android Mobile Applications?original ↗
1 Apr 2024
Evolution of automated weakness detection in Ethereum bytecode: a comprehensive studyoriginal ↗
2 Jan 2024
AI for Formal Verificationoriginal ↗
2 Jan 2024
Leveraging Large Language Models to Boost Dafny's Developers Productivityoriginal ↗
2 Jan 2024
DifFuzzAR: automatic repair of timing side-channel vulnerabilities via refactoringoriginal ↗
1 Jan 2024

2023

Polyglot Code Smell Detection for Infrastructure as Code with GLITCHoriginal ↗
1 Jul 2023
SmartBugs 2.0: An Execution Framework for Weakness Detection in Ethereum Smart Contractsoriginal ↗
1 Jul 2023
Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Executionoriginal ↗
12 May 2023
MUFIN: Improving Neural Repair Models with Back-Translationoriginal ↗
5 Apr 2023

2022

bGSL: An Imperative Language for Specification and Refinement of Backtracking Programsoriginal ↗
1 Aug 2022
GLITCH: Automated Polyglot Security Smell Detection in Infrastructure as Codeoriginal ↗
1 Jul 2022
Extending EcoAndroid with Automated Detection of Resource Leaksoriginal ↗
14 May 2022
Verified password generation from password composition policiesoriginal ↗
7 May 2022
A Preliminary Study on Generating Well-Formed Q# Quantum Programs for Fuzz Testingoriginal ↗
4 Apr 2022
Reliable DevOpsoriginal ↗
1 Feb 2022

2021

EcoAndroid: An Android Studio Plugin for Developing Energy-efficient Java Mobile Applicationsoriginal ↗
7 Dec 2021
Exploring Usable Security to Improve the Impact of Formal Verification: A Research Agendaoriginal ↗
23 Nov 2021
Formal Methods Teaching: 4th International Workshop and Tutorial (FMTea 2021)original ↗
23 Nov 2021
Automatic Repair of Java Code with Timing Side-Channel Vulnerabilitiesoriginal ↗
10 Nov 2021
Towards Improving the Usability of Password Managersoriginal ↗
10 Sept 2021
Automated narrative planning model extensionoriginal ↗
7 May 2021

2020

SmartBugs: A Framework to Analyze Solidity Smart Contractsoriginal ↗
7 Aug 2020
Evaluating the Accuracy of Password Strength Meters using Off-The-Shelf Guessing Attacksoriginal ↗
1 Aug 2020
Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contractsoriginal ↗
23 May 2020
Teachingoriginal ↗
12 Mar 2020
SmartBugs: An Execution Framework for Automated Analysis of Smart Contractsoriginal ↗
5 Mar 2020
Skeptic: Automatic, Justified and Privacy-Preserving Password Composition Policy Selectionoriginal ↗
1 Feb 2020
Smartbugsoriginal ↗
1 Feb 2020
Extending Narrative Planning Domains with Linguistic Resourcesoriginal ↗
15 Jan 2020
Narrative Planning Model Acquisition from Text Summaries and Descriptionsoriginal ↗
1 Jan 2020

2019

Research Opportunitiesoriginal ↗
26 Dec 2019
Logic, Algebra, and Geometry at the Foundation of Computer Scienceoriginal ↗
11 Aug 2019
Lost in Disclosure: On The Inference of Password Composition Policiesoriginal ↗
11 Aug 2019
Open and Interactive Learning Resources for Algorithmic Problem Solvingoriginal ↗
11 Aug 2019

2018

GPS+: Reasoning About Fences and Relaxed Atomicsoriginal ↗
1 Dec 2018
Towards a Program Logic for C11 Release-Sequencesoriginal ↗
5 Jul 2018
Towards Verified Handwritten Calculational Proofsoriginal ↗
5 Jul 2018

2017

Certified Password Quality: A Case Study Using Coq and Linux Pluggable Authentication Modulesoriginal ↗
11 Sept 2017
Framer: Planning Models from Natural Language Action Descriptionsoriginal ↗
11 Sept 2017
ReqCap: Hierarchical Requirements Modeling and Test Generation for Industrial Control Systemsoriginal ↗
11 Sept 2017
StoryFramer: From Input Stories to Output Planning Modelsoriginal ↗
11 Sept 2017
Towards a Constraints Approach to Generating Personalised Horror Film Variantsoriginal ↗
11 Sept 2017
Visualization of Patient Behavior from Natural Language Recommendationsoriginal ↗
11 Sept 2017
Password Securityoriginal ↗
1 Sept 2017

2016

A calculational approach to path-based properties of the Eisenstein-Stern and Stern-Brocot trees via matrix algebraoriginal ↗
1 Aug 2016
Reasoning about Fences and Relaxed Atomicsoriginal ↗
1 Jul 2016
Supporting Social Skills Rehabilitation with Virtual Storytellingoriginal ↗
1 Jul 2016

2014

Automated Verification of the FreeRTOS Scheduler in HIP/SLEEKoriginal ↗
5 Nov 2014
Structure Editing of Handwritten Mathematics: Improving the Computer Support for the Calculational Methodoriginal ↗
5 Nov 2014
The Magic of Algorithm Design and Analysis: Teaching Algorithmic Skills using Magic Card Tricksoriginal ↗
23 Jun 2014
Generative Story Worlds as Linear Logic Programsoriginal ↗
5 Jun 2014

2013

Interactive Narrativesoriginal ↗
1 Mar 2013
The Algorithmics of Solitaire-Like Games (Extended Version)original ↗
5 Feb 2013
Linear logic programming for narrative generationoriginal ↗
6 Jan 2013
Deadline analysis of AUTOSAR OS periodic tasks in the presence of interruptsoriginal ↗
5 Jan 2013

2012

Automated Verification of the FreeRTOS Scheduler in HIP/SLEEKoriginal ↗
5 Nov 2012

2011

An Improved Proof of the Handshaking Lemmaoriginal ↗
20 Sept 2011
Principles and Applications of APSoriginal ↗
2 Jun 2011
On Euclid's Algorithm and Elementary Number Theoryoriginal ↗
5 Feb 2011
Logic Training through Algorithmic Problem Solvingoriginal ↗
5 Jan 2011

2010

Principles and Applications of Algorithmic Problem Solvingoriginal ↗
6 Dec 2010
Designing an Algorithmic Proof of the Two-Squares Theoremoriginal ↗
5 Feb 2010
The Algorithmics of Solitaire-Like Gamesoriginal ↗
5 Feb 2010

2009

Probabilities in Proofreadingoriginal ↗
14 Sept 2009
Students' Feedback on Teaching Mathematics Through The Calculational Methodoriginal ↗
5 Jan 2009
Which Mathematics for the Information Society?original ↗
5 Jan 2009

2008

Multiples in the Fibonacci Seriesoriginal ↗
9 May 2008
JFF7: An exercise from "The Art of Computer Programming"original ↗
28 Feb 2008
A Reward Check From Donald Knuthoriginal ↗
25 Feb 2008
A Square Grid Path Problemoriginal ↗
20 Jan 2008
Recounting the Rationals: Twice!original ↗
5 Jan 2008
JFF6: Resolução eficaz de problemas, quatro exemplosoriginal ↗
1 Jan 2008

2007

JFF1: Exchanging the values of two variablesoriginal ↗
1 May 2007

2006

JFF0: Distributivity and the greatest common divisororiginal ↗
1 Nov 2006
JaSkel: A Java Skeleton-Based Framework for Structured Cluster and Grid Computingoriginal ↗
5 Jan 2006
FM Educationoriginal ↗
1 Jan 2006

2005

A contribution towards a Distributed Java Virtual Machineoriginal ↗
1 Nov 2005
ParC#: Parallel Computing with C# in .NEToriginal ↗
5 Sept 2005
Camila Revival: VDM meets Haskelloriginal ↗
5 Jul 2005