Pith. sign in

REVIEW 3 major objections 4 minor 55 references

Verifying Device Drivers with Pancake

T0 review · 3 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper claims the first formal verification of a performant, real-world Ethernet NIC driver, using a new language called Pancake with a verified compiler and an automated verification front-end.

desk verdict Real engineering progress on verified drivers, with the end-to-end chain honestly left open at the transpiler; worth refereeing despite the gap. read the letter →

arxiv 2501.08249 v2 pith:PIUUX3WO submitted 2025-01-14 cs.PL cs.CRcs.OS

Junming Zhao , Miki Tanaka , Johannes {AA}man Pohjola , Alessandro Legnani , Tiana Tsang Ung , H. Truong , Tsun Wang Sau , Thomas Sewell
show 5 more authors
Rob Sison Hira Syeda Magnus Myreen Michael Norrish Gernot Heiser
This is my paper · ORCID
classification cs.PLcs.CRcs.OS
keywords devicedriververificationPancakeverifiedcompilerCakeMLViperEthernetNICLionsOSformal
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper aims to show that device driver verification, long considered too costly and too slow to be practical, can be combined with real performance. It introduces Pancake, a minimal imperative systems language with a formal semantics and no undefined behaviour, and builds two tools around it: a verified compiler that reuses the CakeML backend to preserve source semantics down to machine code, and an automated front-end that translates annotated Pancake into the Viper verification language. Using these, the authors verify a driver for the 1 Gb/s Ethernet NIC on NXP i.MX 8M processors, showing that device accesses stay within valid register ranges and values, that the driver follows the OS queue signalling protocol, that packet metadata is preserved across all transfer paths, and that RX and TX memory regions are isolated. Benchmarks on a real board show the verified driver's throughput and latency match the original C driver, with around 10 percent more driver CPU usage under load. The broader claim is that a simple language with a verified compiler plus automated deductive verification makes verified, performant drivers a realistic infrastructure goal rather than a research demonstration.

What carries the argument

The load-bearing machinery is Pancake and its two companion tools. Pancake is a deliberately minimal imperative language: the only data are machine words, code pointers, and structs; all memory is statically allocated; pointers to the stack are not allowed; and the language has no concurrency primitives. Its semantics is a functional big-step trace of observable I/O events, including shared-memory loads and stores that can be parameterised by a model of the environment. The verified compiler flattens structs and loops into intermediate languages and then hands off to the verified CakeML backend, which performs instruction selection, register allocation, stack concretisation, and machine-code encoding; the compiler's correctness theorem says that, given enough stack space, the generated binary produces the same observable I/O events as the source. The automated verification front-end transpiles annotated Pancake into the Viper intermediate language, encoding machine words as integers with overflow checks, ordinary memory as an array of words, and shared or device memory as calls to user-supplied Viper methods that model the hardware and neighbouring OS components.

What would settle it

Construct a Pancake program with a deliberately false annotation whose Viper translation is nevertheless provable, for instance an intended machine-word overflow that the integer-based encoding treats as an unbounded integer, and run the pipeline; a verified result on that counterexample would refute the soundness of the verification front-end.

Watch

Extended reading notes

Core claim

The paper's central claim is that it has carried out the first formal verification of a performant driver for a realistic, non-trivial device, and that the toolchain which made this possible is reusable. The verified artifact is a driver for the MAC-NET 1 Gb/s Ethernet core found in NXP i.MX 8M application processors, written in Pancake and running on the LionsOS microkernel-based system. The verification establishes four classes of guarantees: the driver only accesses valid device-interface addresses and writes only device-permissible values; it honours the single-producer single-consumer queue signalling protocol with the rest of the OS; it preserves packet metadata (addresses and lengths) on every transfer pathway, preventing data loss in the driver; and it restricts access to TX and RX state to the appropriate code paths via permissions. The paper also reports that the verified driver's performance is essentially indistinguishable from the C original in measured throughput, latency, and whole-system CPU utilisation. The reason this case study was tractable, the authors argue, is Pancake itself: a language where everything is a machine word, with a few hundred lines of formal semantics, no pointers into the stack, no concurrency, and no undefined behaviour.

Load-bearing premise

The load-bearing premise is that the automated translation from annotated Pancake to Viper is sound: if the translator has a bug, the verifier can report success for a property that is false of the actual Pancake source, and the compiler's correctness theorem does not yet cover the driver's reentrant exported entry points.

Editorial extensions

If this is right

  • A verified driver can be a production driver: the Pancake Ethernet driver's throughput and latency track the C version, with the extra driver CPU cost landing at about 10 percent under load.
  • Driver verification becomes a developer task rather than a years-long research project: a systems programmer with no prior verification experience completed the port and proof in roughly three person-months.
  • For code reachable through the main entry point, source-level correctness is preserved at the binary level because the compiler itself is verified, not just validated.
  • The driver is intended to become an actual network driver option for LionsOS, so the artifact is not a toy or a one-off benchmark.
  • New drivers for other memory-mapped devices can reuse the pattern of a Viper device model plus top-level annotations, which is how the paper expects the approach to scale to commodity hardware.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the same pipeline should transfer to other NICs and simple peripherals, but the paper's evidence is a single device; re-running the workflow on a second device would show how much of the effort is reusable.
  • Editorial inference: because Pancake forbids concurrency, the verified driver avoids an entire bug class, but the guarantees hold for the driver in isolation and assume neighbouring OS components follow the same queue protocol; composing several verified components would require extending the I/O-trace reasoning the paper sketches as future work.
  • Editorial inference: the device model is deliberately underspecified and documented by hand, so the verification is only as strong as the fidelity of that model to the physical chip; checking the model against real device behaviour would close the largest remaining gap between proof and hardware.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents Pancake, a small imperative systems programming language with a formal HOL4 semantics, a verified compiler that reuses the CakeML backend, and an automated verification front-end that transpiles annotated Pancake programs to the Viper intermediate language. The authors apply this toolchain to a 1 Gb/s Ethernet NIC driver for LionsOS, verifying four classes of guarantees against hand-written Viper models of the device and the OS interfaces: device register/descriptor compliance, OS queue signaling protocols, metadata integrity across descriptor-ring and SPSC-queue transfers, and RX/TX region isolation. They report that the verified Pancake driver's throughput matches the C driver and adds roughly 10% driver CPU overhead. Section 6 explicitly discusses the trusted computing base, including as major gaps the unverified Pancake-to-Viper transpiler and the fact that the compiler correctness theorem currently covers only the main entry point rather than the exported reentrant driver functions.

Significance. The compiler proof, reusing the CakeML backend, is a substantial machine-checked development, and the claimed verification effort (a few person-months by a non-expert) is an important data point for the usability of automated deductive verification for low-level systems code. The performance evaluation with a realistic NIC is also a strength relative to earlier driver-verification projects that did not measure performance. The main deliverable is, however, currently a verification framework plus a case study whose source-level guarantees are conditional on the soundness of an unverified transpiler and whose binary-level guarantees do not yet cover the driver's actual entry points. If the missing links are supplied or the claims are appropriately weakened, the contribution would be significant. The paper is commendably explicit about these limitations.

major comments (3)
  1. [Section 6.1 / Section 3] The load-bearing gap is the unverified Pancake-to-Viper transpiler. Section 3 states that the encoding is designed to be sound but that proving its soundness is left to future work, and Section 6.1 concedes that a transpiler bug could produce a Viper query provable by the backend even when the corresponding Pancake property is false. Since every guarantee in Section 4 is obtained by verifying the output of this transpiler, the present results do not establish those properties of the Pancake source, nor of the compiled binary. The Section 8 claim of 'the first formal verification of a demonstrably performant driver' is therefore stronger than what the formal artefacts support. The supported statement is conditional on the soundness of the transpiler for this program and on the soundness of Viper and its SMT backends. I ask the authors to either state the main theorems with transpiler soundness as an explicit hypothesis and weaken the abstract and conclusion accordingly, or prove the transpiler correct for the language subset used by the driver.
  2. [Section 2.4 / Section 6.1] The compiler correctness theorem covers only the main entry point, not the exported reentrant entry points that the driver actually exposes. Section 2.4 notes that the top-level proof 'currently accounts only for the main entry point,' and Section 6.1 similarly says the compiler is verified 'to preserve the semantics of the main function of the source program.' Since the driver is invoked through these exported functions, the binary-level guarantee does not yet apply to the driver as a whole. This gap should be stated as a current limitation in the abstract and conclusion rather than as part of the achieved end-to-end claim.
  3. [Section 3.1] The machine-word encoding in Section 3.1 restricts the verifiable fragment of Pancake to programs that avoid intentional overflow, and it relies on unproved rewrites such as x&255 to x%256. The paper notes that the original C driver used overflow and the Pancake version needed a one-line change. This is a concrete instance where the Viper-verified property could diverge from the Pancake word-level semantics if the bounds checks or rewrites are wrong. I request a precise characterization of the fragment of Pancake for which the encoding is intended to be sound, together with either a proof of the rewrites or an explicit conditional in the statement of the Section 4 guarantees.
minor comments (4)
  1. [Abstract] There is a typo in the abstract: 'Usng' should be 'Using'.
  2. [Section 7] The claim that prior work has not verified a realistic, performant driver should directly engage with the Ironclad network driver and the Erbsen et al. system, both of which include Ethernet drivers and performance data; the current surrounding text explains some distinctions but does not crisply state why those efforts are excluded.
  3. [Section 4.4] The 'data integrity' guarantee concerns packet metadata (addresses and lengths), not the packet payload; this should be made explicit in the contribution list, since readers may infer a stronger confidentiality or integrity guarantee over the packet data.
  4. [Figures 4-5] The methods for measuring driver-only CPU utilisation and separating it from total CPU utilisation should be described; the two figures also use different CPU scales, which makes a direct visual comparison harder.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular steps: the Pancake compiler proof and Viper-based driver verification are independent; the unverified transpiler is a TCB gap, not a circular derivation.

full rationale

The derivation chain is not circular. The paper's two main technical components are independent of each other and of the claimed results: (1) the Pancake compiler correctness proof is a machine-checked HOL4 development that reuses the verified CakeML backend, so the statement that the binary preserves Pancake semantics for the main entry point is an independent theorem rather than a restatement of an assumption; and (2) the driver verification is performed by transpiling annotated Pancake to Viper and checking the result with Viper's external Silicon backend, so the four classes of guarantees in Section 4 are checked properties relative to explicitly stated device and OS-interface models, not fitted quantities or renamed inputs. The device and neighbouring-component models are assumptions (Section 3.3), but assumptions are not circular derivations. The paper itself flags the remaining load-bearing gap in Section 6.1: the Pancake-to-Viper transpiler is unverified, so a transpiler bug could make Viper prove a property that is false of the Pancake program, and Section 2.4 notes the compiler-correctness theorem does not yet cover exported re-entry points. These are soundness and TCB limitations, not circularity: the Viper checks are external, and the encoding is not defined in terms of the properties it is used to prove. The self-citations to CakeML, seL4, and LionsOS are either machine-checked developments or contextual performance claims, not load-bearing justifications of the verification result. No step reduces by construction to its own inputs, so the circularity score is 0.

Assumptions & free parameters 0 free parameters · 8 assumptions · 4 invented entities

No numeric parameters are fitted in this paper: there are no empirical constants or learned values. The verification is theorem-proving based. However, the device model and OS component model in Viper contain method specifications (requires/ensures) that are hand-written choices, and the machine-word encoding decision (treating wraps as failures) is a manual modeling choice.

assumptions (8)
  • domain assumption HOL4 theorem prover is sound.
    Section 6.1 lists it as part of the TCB.
  • domain assumption The official ARM ISA specification is correctly implemented by the CPU.
    Section 6.1: 'the official specification of the Arm ISA is correctly implemented by the CPU.'
  • domain assumption The unverified linker that connects the Pancake binary to external code is correct.
    Section 6.1 lists the linker as TCB.
  • domain assumption The Viper verification infrastructure and SMT solvers are sound.
    Section 6.1: 'we also trust the Viper verification infrastructure and SMT solvers.'
  • ad hoc to paper The Pancake-to-Viper translation is sound.
    Section 6.1 states this is not proved; transpiler is in TCB.
  • ad hoc to paper The device model accurately captures the NIC behavior, including no device interference with descriptor ring indices.
    Section 4.2 and Section 5: device state is modeled in Viper; the paper notes the device is documented not to interfere with ring indices (Section 7).
  • domain assumption Neighboring OS components comply with the SPSC queue protocols and the driver is sole producer/consumer.
    Section 4.3 and Section 6.1.
  • ad hoc to paper Machine-word semantics can be encoded as unbounded integers with overflow treated as failure.
    Section 3.1: overflows are verification failures, changing behavior from C; this is a modeling decision.
invented entities (4)
  • Pancake language
    purpose: New imperative systems programming language with minimal semantics for verification
    Introduced by this paper; only evidence is the implementation and proofs in the CakeML repository, not an independent falsifiable handle.
  • CrepLang and LoopLang intermediate languages
    purpose: Compiler IRs that bridge Pancake syntax to CakeML's WordLang
    Internal compiler artifacts, no external handle.
  • ShMemLoad and ShMemStore shared-memory primitives
    purpose: Native support for device memory and inter-component shared memory in Pancake semantics
    New semantic primitives; their correctness is argued via the compiler proof and Viper encoding, not independent evidence.
  • Viper device model for the i.MX NIC
    purpose: A hand-written specification of the NIC hardware interface used as the basis for driver verification
    The model is an assumption made by the authors; the paper does not validate it against external hardware specifications beyond documentation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verifying Device Drivers with Pancake." pith.science (2026). https://pith.science/paper/PIUUX3WO

@misc{pith2026250108249,
  author       = {Pith},
  title        = {Pith review of: Verifying Device Drivers with Pancake},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PIUUX3WO}},
  note         = {Machine review of arXiv:2501.08249}
}
read the original abstract

Device driver bugs are the leading cause of OS compromises, and their formal verification is therefore highly desirable. To the best of our knowledge, no realistic and performant driver has been verified for a non-trivial device. We propose Pancake, an imperative language for systems programming that features a well-defined and verification-friendly semantics. Leveraging the verified compiler backend of the CakeML functional language, we develop a compiler for Pancake that guarantees that the binary retains the semantics of the source code. Usng automatic translation of Pancake to the Viper SMT front-end, we verify a performant driver for an Ethernet NIC.

Figures

Figures reproduced from arXiv: 2501.08249 by the authors.

Figure 1
Figure 1. Abstract syntax of Pancake. 2.2 The Language and its Semantics Pancake looks and feels like a traditional imperative lan￾guage (see Listing 1, ignore the /@...@/ annotations for now) [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. CakeML and Pancake compiler stack. time. By contrast, Pancake is explicitly designed to be un￾managed and close to hardware, and to have no run￾time. Yet by integration into the CakeML ecosystem, it can reuse many of the existing correctness proofs for the CakeML compiler. The CakeML compiler pro￾vides backends for various target architectures [Tan et al., 2019] verified against detailed models of the target ISA sem… view at source ↗
Figure 3
Figure 3. Driver verification workflow. interface employs lock-free, bounded, single-producer, single-consumer (SPSC) queues that contain meta data buffers for data addresses and lengths, as well as con￾trol information for signaling requests. The driver syn￾chronises with the rest of the OS via semaphores (imple￾mented as seL4 Notifications). The target driver, implemented in Pancake, controls the MAC-NET 1 Gb/s Ethernet cor… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Performance of Ethernet Driver written in [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 5
Figure 5. Figure 5: Performance of Ethernet Driver written in [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

55 extracted references · 51 canonical work pages

  1. [1]

    Alkassar, M

    E. Alkassar, M. Hillebrand, S. Knapp, R. Rusev, and S. Tverdyshev. Formal device and programming model for a serial interface. In International Verification Workshop, pages 4--20, Bremen, DE, July 2007

    work page 2007

  2. [2]

    OS Verification Extended -- On the Formal Verification of Device Drivers and the Correctness of Client/Server Software

    Eyad Alkassar. OS Verification Extended -- On the Formal Verification of Device Drivers and the Correctness of Client/Server Software. PhD thesis, Saarland University, Computer Science Department, 2009

    work page 2009

  3. [3]

    Hillebrand

    Eyad Alkassar and Mark A. Hillebrand. Formal functional verification of device drivers. In Verified Software: Theories, Tools and Experiments, volume 5295 of Lecture Notes in Computer Science, pages 225--239, Toronto, Canada, October 2008. Springer

    work page 2008

  4. [4]

    Cogent : Verifying high-assurance file system implementations

    Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein, and Gernot Heiser. Cogent : Verifying high-assurance file system implementations. In International Conference on Architectural Support for Programming La...

    work page 2016

  5. [5]

    Andrew W. Appel. Verified software toolchain. In European Symposium on Programming, volume 6602 of Lecture Notes in Computer Science, pages 1--17. Springer, 2011

    work page 2011

  6. [6]

    Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter M \" u ller, and Alexander J. Summers. How do programmers use unsafe Rust ? Proceedings of the ACM on Programming Languages, 4 0 ( OOPSLA ): 0 136:1--136:27, 2020

    work page 2020

  7. [7]

    The Prusti project: Formal verification for Rust

    Vytautas Astrauskas, Aurel B \' l \`y , Jon \'a s Fiala, Zachary Grannan, Christoph Matheja, Peter M \"u ller, Federico Poli, and Alexander J Summers. The Prusti project: Formal verification for Rust . In NASA Formal Methods Symposium, pages 88--108. Springer, 2022

    work page 2022

  8. [8]

    Toward compositional verification of interruptible OS kernels and device drivers

    Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, and Ronghui Gu. Toward compositional verification of interruptible OS kernels and device drivers. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 431--447, 2016

    work page 2016

Show all 55 references
  1. [9]

    Veld: Verified Linux drivers

    Xiangdong Chen, Zhaofeng Li, Jerry Zhang, and Anton Burtsev. Veld: Verified Linux drivers. In Workshop on Kernel Isolation, Safety and Verification, page 23–30, New York, NY, USA, 2024. ACM

    2024

  2. [10]

    Formal Verification of Device Drivers in Embedded Systems

    Jianjun Duan. Formal Verification of Device Drivers in Embedded Systems. PhD thesis, University of Utah, USA , 2013

    2013

  3. [11]

    Correctness proofs for device drivers in embedded systems

    Jianjun Duan and John Regehr. Correctness proofs for device drivers in embedded systems. In Systems Software Verification, Vancouver, BC, CA, October 2010. USENIX Association

    2010

  4. [12]

    Is Rust used safely by software developers? In International Conference on Software Engineering, pages 246--257, 2020

    Ana Nora Evans, Bradford Campbell, and Mary Lou Soffa. Is Rust used safely by software developers? In International Conference on Software Engineering, pages 246--257, 2020

    2020

  5. [13]

    Formal specification and verification of ARM6

    Anthony Fox. Formal specification and verification of ARM6 . In International Conference on Theorem Proving in Higher Order Logics, volume 2758 of Lecture Notes in Computer Science, pages 25--40, Rome, Italy, September 2003. Springer

    2003

  6. [14]

    A trustworthy monadic formalization of the ARMv7 instruction set architecture

    Anthony Fox and Magnus Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In International Conference on Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 243--258, Edinburgh, UK, July 2010. Springer

    2010

  7. [15]

    o ssi. A formal semantics for Viper . Master's thesis, Master thesis, ETH Z \

    Cyrill Martin G \"o ssi. A formal semantics for Viper . Master's thesis, Master thesis, ETH Z \"u rich, 2016

    2016

  8. [16]

    Deep specifications and certified abstraction layers

    Ronghui Gu, J \'e r \'e mie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu - Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 595--608....

    2015

  9. [17]

    CertiKOS : An extensible architecture for building certified concurrent OS kernels

    Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\" o berg, and David Costanzo. CertiKOS : An extensible architecture for building certified concurrent OS kernels. In USENIX Symposium on Operating Systems Design and Implementation, pages 653--669, ...

    2016

  10. [18]

    Can we put the "S" into IoT ? In IEEE World Forum on Internet of Things, Yokohama, JP, November 2022

    Gernot Heiser, Lucy Parker, Peter Chubb, Ivan Velickovic, and Ben Leslie. Can we put the "S" into IoT ? In IEEE World Forum on Internet of Things, Yokohama, JP, November 2022

    2022

  11. [19]

    Fast, secure, adaptable: LionsOS design, implementation and performance, January 2025

    Gernot Heiser, Ivan Velickovic, Peter Chubb, Alwin Joshy, Anuraag Ganesh, Bill Nguyen, Cheng Li, Courtney Darville, Guangtao Zhu, James Archer, Jingyao Zhou, Krishnan Winter, Lucy Parker, Szymon Duchniewicz, and Tianyi Bai. Fast, secure, adaptable: LionsOS design, implementati...

    2025 arXiv

  12. [20]

    A quick tour of the VeriFast program verifier

    Bart Jacobs, Jan Smans, and Frank Piessens. A quick tour of the VeriFast program verifier. In Asian Symposium on Programming Languages and Systems (APLAS), volume 6461 of Lecture Notes in Computer Science, pages 304--311. Springer, 2010

    2010

  13. [21]

    Gregory Morrisett, Dan Grossman, Michael W

    Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. Cyclone: A safe dialect of C . In USENIX, pages 275--288, Monterey, CA, USA, June 2002. USENIX

    2002

  14. [22]

    Dejan Jovanovic and Clark W. Barrett. Being careful about theory combination. 42 0 (1): 0 67--90, 2013

    2013

  15. [23]

    RustBelt : Securing the foundations of the Rust programming language

    Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt : Securing the foundations of the Rust programming language. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 66:1--66:34, December 2018

    2018

  16. [24]

    K-Rust : An executable formal semantics for Rust

    Shuanglong Kan, David San \' a n, Shang - Wei Lin, and Yang Liu. K-Rust : An executable formal semantics for Rust . CoRR, abs/1804.07608, 2018. URL http://arxiv.org/abs/1804.07608. Preprint

    2018 arXiv

  17. [25]

    Hrutvik Kanabar, Anthony C. J. Fox, and Magnus O. Myreen. Taming an authoritative Armv8 ISA specification: L3 validation and CakeML compiler verification. In International Conference on Interactive Theorem Proving, page 20:1–20:22, August 2022

    2022

  18. [26]

    Formal verification of a flash memory device driver -- an experience report

    Moonzoo Kim, Yunja Choi, Yunho Kim, and Hotae Kim. Formal verification of a flash memory device driver -- an experience report. In SPIN Workshop on Model Checking Software, volume 5156 of Lecture Notes in Computer Science, pages 144--159, Los Angeles, CA, US, 2008

    2008

  19. [27]

    The Rust Programming Language

    Steve Klabnik and Carol Nichols. The Rust Programming Language . No Starch Press, 2017

    2017

  20. [28]

    seL4 : Formal verification of an OS kernel

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4 : Formal verification of an OS kernel. In ACM Symposium on Operati...

    2009

  21. [29]

    Comprehensive formal verification of an OS microkernel

    Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32 0 (1): 0 2:1--2:70, February 2014

    2014

  22. [30]

    CakeML : A verified implementation of ML

    Ramana Kumar, Magnus Myreen, Michael Norrish, and Scott Owens. CakeML : A verified implementation of ML . In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179--191, San Diego, January 2014. ACM

    2014

  23. [31]

    Verus: Verifying Rust programs using linear ghost types

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. Proceedings of the ACM on Programming Languages, 7 0 (OOPSLA1), April 2023. URL https:...

    2023 doi

  24. [32]

    Formal verification of a realistic compiler

    Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52 0 (7): 0 107--115, 2009

    2009

  25. [33]

    Linux linux kernel: Security vulnerabilities ( CVSS score 9), 2023

    MITRE Corporation . Linux linux kernel: Security vulnerabilities ( CVSS score 9), 2023. URL https://www.cvedetails.com/vulnerability-list.php?vendor_id=33&product_id=47&version_id=&page=1&hasexp=0&opdos=0&opec=0&opov=0&opcsrf=0\ &opgpriv=0&opsqli=0&opxss=0&opdirt=0&opmemc=0&op...

    2023

  26. [34]

    Formal verification of device driver monitors in HOL 4

    Tomas M\" o re. Formal verification of device driver monitors in HOL 4 . Masters thesis, School of EECS, KTH, SE, 2021

    2021

  27. [35]

    Viper: A verification infrastructure for permission-based reasoning

    Peter M \"u ller, Malte Schwerhoff, and Alexander J Summers. Viper: A verification infrastructure for permission-based reasoning. In International Conference on Verification, Model Checking and Abstract Interpretation, pages 41--62, St. Petersburg, FL, US, January 2016 a . Springer

    2016

  28. [36]

    Automatic verification of iterated separating conjunctions using symbolic execution

    Peter M \"u ller, Malte Schwerhoff, and Alexander J Summers. Automatic verification of iterated separating conjunctions using symbolic execution. In International Conference on Computer Aided Verification, pages 405--425. Springer, 2016 b

    2016

  29. [37]

    Type inference verified: Algorithm W in Isabelle/HOL

    Wolfgang Naraschewski and Tobias Nipkow. Type inference verified: Algorithm W in Isabelle/HOL . Journal of Automated Reasoning, 23 0 (3-4): 0 299--318, 1999. URL https://doi.org/10.1023/A:1006277616879

    1999 doi

  30. [38]

    Isabelle/HOL --- A Proof Assistant for Higher-Order Logic , volume 2283 of Lecture Notes in Computer Science

    Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL --- A Proof Assistant for Higher-Order Logic , volume 2283 of Lecture Notes in Computer Science. Springer, 2002

    2002

  31. [39]

    Functional big-step semantics

    Scott Owens, Magnus Myreen, Ramana Kumar, and Yong Kiam Tan. Functional big-step semantics. In European Symposium on Programming, page 27, Eindhoven, The Netherlands, April 2016

    2016

  32. [40]

    Towards trustworthy automated program verifiers: Formally validating translations into an intermediate verification language

    Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter M \"u ller, and Alexander J Summers. Towards trustworthy automated program verifiers: Formally validating translations into an intermediate verification language. Proceedings of the ACM on Programming Languages,...

    2024

  33. [41]

    First steps in verifying the seL4 Core Platform

    Mathieu Paturel, Isitha Subasinghe, and Gernot Heiser. First steps in verifying the seL4 Core Platform . In Asia-Pacific Workshop on Systems (APSys), Seoul, KR, August 2023. ACM

    2023

  34. [42]

    Sound formal verification of Linux's USB BP keyboard driver

    Willem Penninckx, Jan Tobias M \" u hlberg, Jan Smans, Bart Jacobs, and Frank Piessens. Sound formal verification of Linux's USB BP keyboard driver. In NASA Formal Methods Symposium, volume 7226 of Lecture Notes in Computer Science, 2012

    2012

  35. [43]

    Dingo: Taming device drivers

    Leonid Ryzhyk, Peter Chubb, Ihor Kuz, and Gernot Heiser. Dingo: Taming device drivers. In EuroSys Conference, pages 275--288, Nuremberg, DE, April 2009 a

    2009

  36. [44]

    Automatic device driver synthesis with Termite

    Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur, and Gernot Heiser. Automatic device driver synthesis with Termite . In ACM Symposium on Operating Systems Principles, pages 73--86, Big Sky, MT, US, October 2009 b

    2009

  37. [45]

    The case for active device drivers

    Leonid Ryzhyk, Yanjin Zhu, and Gernot Heiser. The case for active device drivers. In Asia-Pacific Workshop on Systems (APSys), pages 25--30, New Delhi, India, August 2010

    2010

  38. [46]

    User-guided device driver synthesis

    Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm, and Mona Vij. User-guided device driver synthesis. In USENIX Symposium on Operating Systems Design and Implementation, pages 661--676, Broomfield, CO, USA, October 2014

    2014

  39. [47]

    Formal verification of secure user mode device execution with DMA

    Oliver Schwarz and Mads Dam. Formal verification of secure user mode device execution with DMA . In Hardware and Software: Verification and Testing, pages 236--251, Cham, 2014. Springer International Publishing

    2014

  40. [48]

    Advancing automated, permission-based program verification using symbolic execution

    Malte H Schwerhoff. Advancing automated, permission-based program verification using symbolic execution. PhD thesis, ETH Zurich, 2016

    2016

  41. [49]

    Translation validation for a verified OS kernel

    Thomas Sewell, Magnus Myreen, and Gerwin Klein. Translation validation for a verified OS kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 471--481, Seattle, Washington, USA, June 2013. ACM

    2013

  42. [50]

    A brief overview of HOL4

    Konrad Slind and Michael Norrish. A brief overview of HOL4 . In International Conference on Theorem Proving in Higher Order Logics, pages 28--32, Montr\'eal, Canada, August 2008. Springer

    2008

  43. [51]

    The verified CakeML compiler backend

    Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. Journal of Functional Programming, 29, February 2019

    2019

  44. [52]

    Krust: A formal executable semantics of rust

    Feng Wang, Fu Song, Min Zhang, Xiaoran Zhu, and Jun Zhang. Krust: A formal executable semantics of rust. In 2018 International Symposium on Theoretical Aspects of Software Engineering ( TASE ) , pages 44--51. IEEE Computer Society, 2018. URL https://doi.org/10.1109/TASE.2018.00014

    2018

  45. [53]

    Matsakis, and Amal Ahmed

    Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. Oxide : The essence of Rust . CoRR, abs/1903.00982, 2019. URL http://arxiv.org/abs/1903.00982. Preprint

    1903 arXiv

  46. [54]

    Gobra: Modular specification and verification of Go programs

    Felix A Wolf, Linard Arquint, Martin Clochard, Wytse Oortwijn, Jo \ a o C Pereira, and Peter M \"u ller. Gobra: Modular specification and verification of Go programs. In International Conference on Computer Aided Verification, pages 367--379. Springer, 2021

    2021

  47. [55]

    Pierce, and Steve Zdancewic

    Li - yao Xia, Yannick Zakowski, Paul He, Chung - Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq . Proceedings of the ACM on Programming Languages, 4: 0 51:1--51:32, January 2020

    2020

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.