No Cover Image

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 Orcid Logo, Anton Setzer Orcid Logo

RocqPL 2026

Swansea University Authors: Harry Bryant, Monika Seisenberger Orcid Logo, Anton Setzer Orcid Logo

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...

Full description

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
first_indexed 2025-12-19T17:52:13Z
last_indexed 2026-01-23T06:52:02Z
id cronfa71163
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2026-01-22T12:05:13.7536824</datestamp><bib-version>v2</bib-version><id>71163</id><entry>2025-12-19</entry><title>Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq</title><swanseaauthors><author><sid>2efb4f6a3eec27ae4337ecd971aaeca4</sid><firstname>Harry</firstname><surname>Bryant</surname><name>Harry Bryant</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>d035399b2b324a63fe472ce0344653e0</sid><ORCID>0000-0002-2226-386X</ORCID><firstname>Monika</firstname><surname>Seisenberger</surname><name>Monika Seisenberger</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-12-19</date><deptcode>MACS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>RocqPL 2026</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>ACM</publisher><placeOfPublication>Rennes, France</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>0</publishedDay><publishedMonth>0</publishedMonth><publishedYear>0</publishedYear><publishedDate>0001-01-01</publishedDate><doi/><url>https://popl26.sigplan.org/home/rocqpl-2026#event-overview</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders/><projectreference/><lastEdited>2026-01-22T12:05:13.7536824</lastEdited><Created>2025-12-19T17:38:34.0721325</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Harry</firstname><surname>Bryant</surname><order>1</order></author><author><firstname>Andrew</firstname><surname>Lawrence</surname><order>2</order></author><author><firstname>Monika</firstname><surname>Seisenberger</surname><orcid>0000-0002-2226-386X</orcid><order>3</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</orcid><order>4</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2026-01-22T12:05:13.7536824 v2 71163 2025-12-19 Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq 2efb4f6a3eec27ae4337ecd971aaeca4 Harry Bryant Harry Bryant true false d035399b2b324a63fe472ce0344653e0 0000-0002-2226-386X Monika Seisenberger Monika Seisenberger true false 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 2025-12-19 MACS 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. Conference Paper/Proceeding/Abstract RocqPL 2026 ACM Rennes, France 0 0 0 0001-01-01 https://popl26.sigplan.org/home/rocqpl-2026#event-overview COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University 2026-01-22T12:05:13.7536824 2025-12-19T17:38:34.0721325 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Harry Bryant 1 Andrew Lawrence 2 Monika Seisenberger 0000-0002-2226-386X 3 Anton Setzer 0000-0001-5322-6060 4
title Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
spellingShingle Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
Harry Bryant
Monika Seisenberger
Anton Setzer
title_short Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
title_full Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
title_fullStr Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
title_full_unstemmed Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
title_sort Formal assurance for railway interlockings: Verifying Z3 SAT proofs with Tseitin in Rocq
author_id_str_mv 2efb4f6a3eec27ae4337ecd971aaeca4
d035399b2b324a63fe472ce0344653e0
5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 2efb4f6a3eec27ae4337ecd971aaeca4_***_Harry Bryant
d035399b2b324a63fe472ce0344653e0_***_Monika Seisenberger
5f7695285397f46d121207120247c2ae_***_Anton Setzer
author Harry Bryant
Monika Seisenberger
Anton Setzer
author2 Harry Bryant
Andrew Lawrence
Monika Seisenberger
Anton Setzer
format Conference Paper/Proceeding/Abstract
container_title RocqPL 2026
institution Swansea University
publisher ACM
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url https://popl26.sigplan.org/home/rocqpl-2026#event-overview
document_store_str 0
active_str 0
description 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.
published_date 0001-01-01T05:34:36Z
_version_ 1856987072161644544
score 11.096212

Similar Items