Verified Software

Daniele is a tenured assistant professor at the Department of Mathematics, University of Brasília, and collaborated with the group during a long sabbatical leave.

Daniele’s research focuses on equational reasoning and comparative expressiveness of models and languages with concurrency. She was a researcher with the Theoretical Computer Science Group (GTC-UnB), and an external collaborator of the VIDI project Unifying Correctness for Communicating Systems. Her latest publications are Formalising nominal C-unification generalised with protected variables, published in Mathematical Structures for Computer Science, and the conference papers Nominal Equational Problems, published in ETAPS’ Foundations of Software Science and Computation Structures (FOSSACS 2021) series, and Non-deterministic Functions as Non-Deterministic Processes, in Formal Structures for Computation and Deduction (FSCD 2021) series.

Group Publications

1. Compositional Symbolic Execution for the Next 700 Memory Models

   • Andreas Lööw
   • Seung Hoon Park
   • Daniele Nantes-Sobrinho
   • Sacha-Élie Ayoun
   • Opale Sjöstedt
   • Philippa Gardner

   Proc. ACM Program. Lang., vol. 9(OOPSLA2)

2. Matching Plans for Frame Inference in Compositional Reasoning

   • Andreas Lööw
   • Daniele Nantes-Sobrinho
   • Sacha-Élie Ayoun
   • Petar Maksimović
   • Philippa Gardner

   38th European Conference on Object-Oriented Programming (ECOOP 2024), pp. 26:1–26:20

3. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

   • Andreas Lööw
   • Daniele Nantes-Sobrinho
   • Sacha-Élie Ayoun
   • Caroline Cronjäger
   • Petar Maksimović
   • Philippa Gardner

   38th European Conference on Object-Oriented Programming (ECOOP 2024), pp. 25:1–25:28

4. A Certified Algorithm for AC-Unification

   • Mauricio Ayala-Rincón
   • Maribel Fernández
   • Gabriel Ferreira Silva
   • Daniele Nantes

   7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pp. 8:1–8:21

5. Nominal Anti-Unification with Atom-Variables

   • Manfred Schmidt-Schauß
   • Daniele Nantes

   7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), pp. 7:1–7:22

6. Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes

   • Joseph W. N. Paulus
   • Daniele Nantes
   • Jorge A. Pérez

   27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference), pp. 11:1–11:24