Conference Paper/Proceeding/Abstract 75 views
Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
Harry Bryant,
Andrew Lawrence,
Monika Seisenberger 
,
Anton Setzer
,
Anton Setzer
RocqPL 2026
Swansea University Authors:
Harry Bryant, Monika Seisenberger , Anton Setzer
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 correctnes...
| Published in: | RocqPL 2026 |
|---|---|
| Published: |
Rennes, France
ACM
|
| Online Access: |
https://popl26.sigplan.org/home/rocqpl-2026#event-overview |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa71163 |
| 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. |
|---|---|
| College: |
Faculty of Science and Engineering |