On the 20th of September 2024, I successfully defended my Ph.D. thesis titled "Formal Verification of Heap Space Bounds under Garbage Collection".

The manuscript be found here. The slides are here.

Music

A piece of music accompanies each chapter of the thesis, illustrating the text. Feel free to play the music while reading.

  1. Introduction
    Prokofiev S. Violin Concerto No. 2, Andante Assai. [ youtube (Jansen) | spotify (Jansen) ]
  2. Key Ideas
    The Jamaicans. Ba Ba Boom. [ youtube | spotify ]
  3. Why Treiber’s Stack Needs Protected Sections
    Gottschalk, L. M. Souvenir de Porto-Rico, marche des Gibaros. [ youtube (Lively) | spotify (Martin) ]
  4. Syntax and Semantics of LambdaFit
    Janequin, C. Le chant des oyseaulx. [ youtube (Ensemble Clément Janequin) | spotify (Seyer-Hansen) ]
  5. Program Logic: Assertions
    Pink Floyd. Atom Heart Mother. [ youtube | spotify ]
  6. Program Logic: Reasoning Rules
    Rachmaninoff, S. Rhapsody on a Theme of Paganini. [ youtube (Rubinstein) | spotify (Trifonov) ]
  7. Safety, Liveness and Core Soundness Theorems
    Dave Brubeck Quartet. Take Five. [ youtube | spotify ]
  8. Proof of the Core Soundness Theorem
    Beethoven, L. Rondo a capriccio “Rage Over a Lost Penny”. [ youtube (Scheps) | spotify (Lisitsa) ]
  9. Closures
    Poulenc, F. Clarinet Sonata. [ youtube, live (Baldeyrou/Cournot) | spotify (Wien-Berlin/Levine) ]
  10. Triples with Souvenir
    Yom. The Old Man. [ youtube | spotify ]
  11. Sequential Case Studies
    Vaughan, S. Lullaby of Birdland. [ youtube | spotify ]
  12. Concurrent Case Studies
    Schubert, F. String Quartet No. 14 “Death and the Maiden”. [ youtube (Integra) | spotify (Arod) ]
  13. Related Work
    Queen. Bohemian Rhapsody. [ youtube | spotify ]
  14. Conclusion
    Piazzolla, A. Las Cuatro Estaciones Porteñas, Primavera Porteña. [ youtube | spotify ]
  15. Bibliography
    Mozart, W. A. Don Giovanni, “Madamina, il catalogo è questo”. [ youtube (van Dam) | spotify (van Dam) ]