Gillian, part i: a multi-language platform for symbolic execution. - José Fragoso Santos; Petar Maksimovic 001; Sacha-Élie Ayoun; Philippa Gardner (PLDI, 2020)

Gillian: Compositional Symbolic Execution for All. - José Fragoso Santos; Petar Maksimovic 001; Sacha-Élie Ayoun; Philippa Gardner (CoRR, 2020)

Gillian, Part II: Real-World Verification for JavaScript and C. - Petar Maksimovic 001; Sacha-Élie Ayoun; José Fragoso Santos; Philippa Gardner (CAV (2), 2021)

Gillian: A Multi-Language Platform for Unified Symbolic Analysis. - Petar Maksimovic 001; José Fragoso Santos; Sacha-Élie Ayoun; Philippa Gardner (CoRR, 2021)

Exact Separation Logic. - Petar Maksimovic 001; Caroline Cronjäger; Julian Sutherland; Andreas Lööw; Sacha-Élie Ayoun; Philippa Gardner (CoRR, 2022)

Symbolic Debugging with Gillian. - Nat Karmios; Sacha-Élie Ayoun; Philippa Gardner (DEBT@ISSTA, 2023)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Matching Plans for Frame Inference in Compositional Reasoning. - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Petar Maksimovic 001; Philippa Gardner (ECOOP, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Petar Maksimovic 001; Philippa Gardner (CoRR, 2024)

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). - Andreas Lööw; Daniele Nantes-Sobrinho; Sacha-Élie Ayoun; Caroline Cronjäger; Nat Karmios; Petar Maksimovic 001; Philippa Gardner (Dagstuhl Artifacts Ser., 2024)

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness. - Pedro Carrott; Sacha-Élie Ayoun; Azalea Raad (ECOOP, 2025)

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact). - Pedro Carrott; Sacha-Élie Ayoun; Azalea Raad (Dagstuhl Artifacts Ser., 2025)

A Hybrid Approach to Semi-automated Rust Verification. - Sacha-Élie Ayoun; Xavier Denis; Petar Maksimovic 001; Philippa Gardner (Proc. ACM Program. Lang., 2025)