Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq (RocqPL 2026 - Rocq for Programming Languages 2026)

Sun 11 - Sat 17 January 2026 Rennes, France

Who

Harry Bryant, Andrew Lawrence, Monika Seisenberger, Anton Setzer

Track

RocqPL 2026 Rocq for Programming Languages

This program is tentative and subject to change.

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

Save

When

Sat 17 Jan 2026 16:15 - 16:30 at Salle 14 - Certified Programs and Proofs in Rocq

Abstract

We present a method for verifying in the theorem prover Rocq SAT proofs of railway interlockings generated by Z3 using the RUP format and Tseitin Transformations. We outline the checking procedures for RUP and the supporting Tseitin Transformation rules. This includes steps to prove their correctness and the extraction of a fully verified checker. We prove Tseitin steps correct by turning them into tautologies using a novel technique. The verification process is crucial in the context of railway interlockings, where ensuring logical soundness and a high level of safety are essential.

File attachments

Extended Abstract (rocqpl26-final8.pdf)	603KiB

Harry Bryant

Swansea University

Andrew Lawrence

Siemens Mobility

Monika Seisenberger

Swansea University

Anton Setzer

Swansea University

This program is tentative and subject to change.

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

Display full programSpecify a time band

Save

Session Program

Sat 17 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 18:00	Certified Programs and Proofs in RocqRocqPL at Salle 14

16:00 15m Talk		Abstract VCG: Tie-breaking rules in VCG mechanism design RocqPL Zhan JING Shanghai Jiao Tong University, Pierre Jouvelot
16:15 15m Talk		Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq RocqPL Harry Bryant Swansea University, Andrew Lawrence Siemens Mobility, Monika Seisenberger Swansea University, Anton Setzer Swansea University File Attached
16:30 15m Talk		Formalizing a First-order Differentiable Logic with MathComp RocqPL Jairo Miguel Marulanda-Giraldo University of Southampton
16:45 15m Talk		Recursive Mutexes in Separation Logic RocqPL Ke Du , William Mansky University of Illinois Chicago, Paolo G. Giarrusso Delft University of Technology, Gregory Malecha Skylabs AI
17:00 15m Talk		Towards a Mechanization of the ECMAScript (JavaScript) Proposal "Temporal" RocqPL Aria B. Eide University of Bergen, Vebjørn S. Øiestad University of Bergen, Mikhail Barash University of Bergen File Attached
17:15 15m Talk		Verification of Templated Code in C++ RocqPL Gregory Malecha Skylabs AI, David Swasey Riverside Research, Simon Hudon SkyLabs AI
17:30 15m Talk		Lambda JS à la Carte RocqPL Kirill Golubev University of Turku, Mikhail Barash University of Bergen, Jaakko Järvi University of Turku File Attached

Hide past events