Research
Research interests
I carry out research mainly in the field of formal verification of programs. In particular, I study the development of computer-aided verification systems, and their application to complex data structures and algorithms.
More specifically, my current lines of research are the following:
- Formal verification of heap-based mutable data structures
We use the Dafny language to formally verify a number of data structures: linked lists, red-black trees, etc. Although verification of abstract data types have been studied for several decades, we focus on the methological aspects that allow us to carry out this task on mutable data structures while maintaining proper encapsulation. See, for example, JLAMP 2023 paper, and Jorge Blazquez's MSc Thesis.
-
Applications of computer-aided verification
We have successfully applied computer-aided verification systems such as Dafny to verify the NavFn planner of the Navigation Stack of ROS. We have also developed a methodology to verify greedy algorithms and dynamic programming-based algorithms.
-
Verification platforms
I have done research on intermediate representations for program verification, as part of the CAVI-ART project (2014-2021), and also I have devised SMT-based verification condition generators for the Elixir functional language and WebAssembly bytecode.
Past research areas
Before embarking on program verification, my main research area used to be static analysis of programs. In particular:
- Type systems
We have extended Dialyzer's type system (used in Erlang) with polymorphic types (see COLA 2020 paper and Gorka Suarez's PhD Thesis). We have also developed an extension of liquid types in order to allow quantified properties on arrays (see ATVA 17 and TOCL 2020).
- Safe: explicit memory management with pointer safety and resource analysis
Safe was a research platform aimed at investigating the suitability of functional languages for programming devices with strict memory requirements. It consisted in a first-order functional programming language which provided semiexplicit memory management through two mechanisms: region-based memory management (inferred by the compiler) and destructive pattern matching (specified by the programmer). We have developed a type-based analysis guaranteeing the absence of dangling pointers due to the latter, and an abstract-interpretion analysis to infer upper bounds of memory consumption.
Refereed publications
-
Verification of the ROS NavFn planner using executable specification languages
In Journal of Logical and Algebraic Methods in Programming, vol. 132, page 100860 (2023)
-
Verification of mutable linear data structures and iterator-based algorithms in Dafny
In Journal of Logical and Algebraic Methods in Programming, vol. 134, page 100875 (2023)
-
Improving Database Learning with an Automatic Judge
In The 34th International Conference on Software Engineering and Knowledge Engineering, SEKE 2022, KSIR Virtual Conference Center, USA, July 1 - July 10, 2022. KSI Research Inc (2022)
-
Extending Liquid Types to Arrays
In ACM Transactions on Computational Logic (TOCL), vol. 21, pages 13:1-13:41 (2020)
-
Deriving overloaded success type schemes in Erlang
In Journal of Computer Languages, vol. 58, page 100965 (2020)
-
Polymorphic success types for Erlang
In LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018. EPiC Series in Computing, vol. 57. EasyChair (2018)
-
Liquid Types for Array Invariant Synthesis
In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10482. Springer (2017)
-
Polymorphic Types in Erlang Function Specifications
In Functional and Logic Programming - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9613. Springer (2016)
-
Falsification of Java Assertions Using Automatic Test-Case Generators
In International Journal on Advances in Systems and Measurements, vol 9(3-4). Elsevier. ISSN 1942-261x. Pages 177-187 (2016)
-
Shape analysis in a functional language by using regular languages
In Science of Computer Programming, vol. 111, pages 51-78 (2015)
-
Space consumption analysis by abstract interpretation: Inference of recursive functions
In Science of Computer Programming, vol. 111, pages 426-457 (2015)
-
Space consumption analysis by abstract interpretation: Reductivity properties
In Science of Computer Programming, vol. 111, pages 458-482 (2015)
-
Checking Java Assertions Using Automated Test-Case Generation
In Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers. Lecture Notes in Computer Science, vol. 9527. Springer (2015)
-
A Generic Intermediate Representation for Verification Condition Generation
In Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Siena, Italy, July 13-15, 2015. Revised Selected Papers. Lecture Notes in Computer Science, vol. 9527. Springer (2015)
-
Automatic Falsification of Java Assertions
In 7th International Conference on Advances in System Testing and Validation Lifecycle, VALID 2015. ISBN 9781612084411. Pages 36-41. IARIA (2015)
-
ResAna: a resource analysis toolset for (real-time) JAVA
In Concurrency and Computation: Practice and Experience, vol. 26, pages 2432-2455 (2014)
-
A resource semantics and abstract machine for Safe: A functional language with regions and explicit deallocation
In Information and Computation, vol. 235, pages 3-35 (2014)
-
Shape analysis in a functional language by using regular languages
In 15th International Symposium on Principles and Practice of Declarative Programming, PPDP '13, Madrid, Spain, September 16-18, 2013. ACM (2013)
-
Making resource analysis practical for real-time Java
In The 10th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES '12, Copenhagen, Denmark, October 24-26, 2012. ACM (2012)
-
Interpolation-Based Height Analysis for Improving a Recurrence Solver
In Foundational and Practical Aspects of Resource Analysis - Second International Workshop, FOPARA 2011, Madrid, Spain, May 19, 2011, Revised Selected Papers. Lecture Notes in Computer Science, vol. 7177. Springer (2011)
-
Certified Absence of Dangling Pointers in a Language with Explicit Deallocation
In Integrated Formal Methods - 8th International Conference, IFM 2010, Nancy, France, October 11-14, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6396. Springer (2010)
-
A Resource-Aware Semantics and Abstract Machine for a Functional Language with Explicit Deallocation
In Electronic Notes in Theoretical Computer Science (ENTCS), vol. 246, pages 167-182 (2009)
-
A Space Consumption Analysis by Abstract Interpretation
In Foundational and Practical Aspects of Resource Analysis - First International Workshop, FOPARA 2009, Eindhoven, The Netherlands, November 6, 2009, Revised Selected Papers. Lecture Notes in Computer Science, vol. 6324. Springer (2009)
-
A Simple Region Inference Algorithm for a First-Order Functional Language
In Functional and Constraint Logic Programming, 18th International Workshop, WFLP 2009, Brasilia, Brazil, June 28, 2009, Revised Selected Papers. Lecture Notes in Computer Science, vol. 5979. Springer (2009)
-
An Inference Algorithm for Guaranteeing Safe Destruction
In Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, July 17-18, 2008, Revised Selected Papers. Lecture Notes in Computer Science, vol. 5438. Springer (2008)
-
A type system for safe memory management and its proof of correctness
In Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain. ACM (2008)
-
A sharing analysis for SAFE
In Revised Selected Papers from the Seventh Symposium on Trends in Functional Programming, TFP 2006, Nottingham, United Kingdom, 19-21 April 2006. Trends in Functional Programming, vol. 7. Intellect (2006)
PhD Thesis
-
Safety properties and memory bound analysis in a functional language without a garbage collector 🇬🇧
Supervised by Ricardo Peña and Clara Segura
Defended: November 2011