A Correct-by-Construction Checker for Validation of Railway Data (Dafny 2026) - POPL 2026

Sun 11 - Sat 17 January 2026 Rennes, France

Who

Benoît Boyer, Noé Canva, Matteo Manighetti, Claude Marché

Track

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

When

Sun 11 Jan 2026 15:12 - 15:30 at Horizons - Applications and Lessons Learned

Abstract

The objective of our work is the checking of requirements on data describing railway networks. We expose the design, the formal specification and an implementation of a program that checks such constraints, with a formal proof of correctness. That program is compiled into an executable code, linked together with some additional, non-verified code for input/output. It is experimented on significantly complex examples, showing that the efficiency of the checker is competitive with non-formally verified related tools.

Link to Publication

https://inria.hal.science/hal-05442460

Benoît Boyer

Mitsubishi Electric R&D Centre Europe, Rennes, France

France

Noé Canva

Inria Saclay & Université Paris-Saclay

Matteo Manighetti

IRIF, Université Paris Cité

France

Claude Marché

Inria Saclay & Université Paris-Saclay

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Session Program

Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

	14:00 - 15:30	Applications and Lessons LearnedDafny at Horizons

	14:00 18m Talk		Lessons from Building an Auto-Active Verifier in Lean Dafny George Pîrlea National University of Singapore, Vladimir Gladshtein , Qiyuan Zhao National University of Singapore, Ilya Sergey National University of Singapore Pre-print
	14:18 18m Talk		Formal Verification of Minimax Algorithms Dafny Wieger Wesselink Eindhoven University of Technology, Kees Huizing Eindhoven University of Technology, Huub van de Wetering Eindhoven University of Technology File Attached
	14:36 18m Talk		Teaching Automata Theory and Formal Languages with Dafny Dafny Ran Ettinger NVIDIA Pre-print
	14:54 18m Talk		Verification of E-Voting Algorithms in Dafny Dafny Robert Büttner University of Regensburg, Fabian Franz Dießl University of Regensburg, Patrick Janoschek University of Regensburg, Ivana Kostadinovic University of Regensburg, Henrik Oback University of Regensburg, Kilian Voß University of Regensburg, Franziska Alber University of Regensburg, Roland Herrmann University of Regensburg, Sibylle Möhle University of Regensburg, Philipp Rümmer University of Regensburg and Uppsala University Pre-print
	15:12 18m Talk		A Correct-by-Construction Checker for Validation of Railway Data Dafny Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Noé Canva Inria Saclay & Université Paris-Saclay, Matteo Manighetti IRIF, Université Paris Cité, Claude Marché Inria Saclay & Université Paris-Saclay Link to publication