Skip to main content

End-to-End Verification of Processors with ISA-Formal

Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, Ali Zaidi

DOI 10.1007/978-3-319-41540-6_3 dblp BibTeX

Abstract elided by the publisher.

Related papers

Scaling Instruction-Selection Verification against Authoritative ISA Semantics OOPSLA 2025
Synthesizing Instruction Selection Back-Ends from ISA Specifications Made Practical CGO 2026
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract CAV 2020
Formal Verification of an SSA-Based Middle-End for CompCert TOPLAS 2014
VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems POPL 2025
Verified compilation on a verified processor PLDI 2019
Allocating architected registers through differential encoding TOPLAS 2007
Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting POPL 2025