European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

September 17-19, 2025

Program

The event is scheduled as a two and a half-day meeting. Times are CET.

Day 1

  • Opening & Presentation (09:00-09:30): The EuroProofNet COST Action and WG3 “Program Verification”. Adrián Riesco
  • WG3 (9:30-10:30)
    • Deliverables D11 & D12. Adrián Riesco and Alicia Villanueva
    • Discussion
  • Talks (11:00-12:30)
    • :large_blue_circle: Sound and Complete Invariant-Based Heap Encodings. Esen Zafer (Uppsala University, Sweden)
    • :white_circle: TBA. Sibylle Möhle (Max Planck Institute for Informatics, Germany)
  • Talks (14:00-15:30)
    • :large_blue_circle: Formal Analysis of Attested TLS in Industrial Settings. Usama Sardar (TU Dresden, Germany)
    • :white_circle: Separation Logic is incomplete. Hans-Dieter Hiep (NLnet Foundation)
  • Talks and Discussion (16:00-17:30)
    • :white_circle: Formally verified domains in Why3. Catherine Dubois (ENSIIE, France).

Day 2

  • Talks (09:00-10:30)
    • :white_circle: Verification tools. Madalina Erascu (West University of Timisoara, Romania)
    • :large_blue_circle: Prove your Colorings: Formal Verification of Cache Coloring of Bao Hypervisor. Nikolai Kosmatov (Thales Research and Technology,France)
  • WG3 + MCLP Session (11:00-12:30)
    • :clipboard: A Lean-based Language for Teaching Proof in High-school. Frédéric Tran Minh (UGA-Grenoble INP-Esisar), Laure Gonnord (Grenoble-INP / LCIS), and Julien Narboux (RIF - Université Paris Cité)
  • WG3 + MCLP Session (14:00-15:30)
    • :large_blue_circle: Singular and Plural Functions. Adrian Riesco* and Juan Rodriguez-Hortala (Universidad Complutense de Madrid, Spain)
    • TBA. Roussanka Loukanova, (Bulgarian Academy of Sciences)
  • WG3 + MCLP Session (16:00-17:00)
    • :large_blue_circle: Natural Logic: Proof Systems for Reasoning in Natural Language. Lawrence S. Moss* (Indiana University, USA)
  • Closing the day

Day 3

  • Talks (9:00-10:30)
    • :large_blue_circle: A Global Specification Model for Data-Aware Coordination (with an application to smart contracts). António Ravara (New University of Lisbon, Portugal)
    • :white_circle: MongoDB Specification in Maude. Beatriz Alcaide (UCM, Madrid)
  • Talks & Conclusion (11:00-12:30)
    • TBA

List of participants:

  • After the meeting