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.

February 8-9, 2023

Program

The event is scheduled as a two-day meeting. Times are EET.

Day 0. February 7th, 2023

  • 19:00 Dinner at The Scotland Yard, Eugeniu de Savoya 9 Street, https://www.facebook.com/scotlandyard.timisoara (Optional, self-pay). Meet in the Perla Hotel lobby or directly at the location.

Day 1. February 8th, 2023

  • 9:00 - 9:30 Registration, Opening & Presentation
    • The EuroProofNet COST Action. WG3 “Program Verification”. Goals of the meeting. Mădălina Erașcu, Alicia Villanueva (slides)
  • 9:30-11:00 Talks
    • 9:30-10:00: Verification Tools, Exchange Formats, and Combination Approaches. Dirk Beyer. LMU Munich (slides)
    • 10:00-10:15: RAPID software verification framework. Pamina Georgiou. TU Wien (slides)
    • 10:15-10:30: Verification with Superposition Provers and Induction. Ahmed Bhayat. University of Manchester (slides)
    • 10:30-10:45: Annotation synthesis for C programs using TriCera. Zafer Esen. Uppsala University (slides)
    • 10:45-11:00: Program analysis and verification. Lilia Georgieva. Heriot Watt University (slides)
  • 11:00-11:30 Coffee Break
  • 11:30-12:30 Talks
    • 11:30-12:00: Techniques and Tools for Automated Termination Analysis. Carsten Fuhs.Birkbeck University of London (slides)
    • 12:00-12:30: Implementing Program Verification in the K Framework. Traian Șerbănuță. University of Bucharest and Runtime Verification Inc. (slides)
  • 12:30-14:00 Lunch break
  • 14:00-15:30 Interaction: Working in groups for deliverables of WP3 or research related to WP3
  • 15:30-16:00 Coffee Break
  • 16:00-17:00 Talks & Conclusions of the day
    • 16:00-16:15: Formal verification of Isawa-Morii authentication protocol. Mehmet Tahir Sandikkaya. Istanbul Technical University (slides)
    • 16:15-16:30: Tools and Techniques for Symbolic Protocol Verification. Muhammad Usama Sardar. TU Dresden (slides)
    • 16:30-17:00: Wrapping-up: Conclusions of the day & plan
  • 18:00 Dinner at Curtea Berarilor Timișoreana, Strada Proclamația de la Timișoara, Nr.7, https://www.facebook.com/curteaberii.timisoara/ (Optional, self-pay). Meet in front of the university building or directly at the location.

Day 2

  • 9:00-11:00 Talks
    • 9:00 - 9:30: Deriving Matching Logic Specifications from Program Annotations. Dorel Lucanu.Alexandru Ioan Cuza University of Iași (slides) (video)
    • 9:30 - 9:45: A language-independent ecosystem for program verification. Amélie Ledein. ENS Paris-Saclay (slides) (video)
    • 9:45 - 10:00: Matching Logic and Lean. Horațiu Cheval. University of Bucharest and Institute for Logic and Data Science (slides) (video)
    • 10:00-10:15: Interactive Verification of Java Programs with KeY. Wolfram Pfeifer. Karlsruhe Institute of Technology (slides) (video)
    • 10:15 - 10:30: Interactive proofs for matching logic, using Coq. Jan Tušil. Masaryk University, Brno (slides) (video)
    • 10:30 - 10:45: Quantitative intersection types for computational core meet dependency. Riccardo Treglia. Università di Bologna
  • 10:45 - 11:00: Discussions
  • 11:00-11:30 Coffee Break
  • 11:30-12:30 Interaction: Working in groups for deliverables of WP3 or research related to WP3
  • 12:30-14:00 Lunch Break
  • 14:00-15:30 Interaction: Working in groups for deliverables of WP3 or research related to WP3
  • 15:30-16:00 Coffee Break
  • 16:00-17:00 Wrapping-up: Setting the agenda for the year

Participants:

List of participants

Photos