Abstract is missing.
- The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk)June Andronick. 1 [doi]
- Coq's vibrant ecosystem for verification engineering (invited talk)Andrew W. Appel. 2-11 [doi]
- Structural embeddings revisited (invited talk)César Muñoz. 12 [doi]
- Overcoming restraint: composing verification of foreign functions with cogentLouis Cheung, Liam O'Connor, Christine Rizkallah. 13-26 [doi]
- Verbatim++: verified, optimized, and semantically rich lexing with derivativesDerek Egolf, Sam Lasser, Kathleen Fisher. 27-39 [doi]
- Formally verified superblock schedulingCyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino. 40-54 [doi]
- Certified abstract machines for skeletal semanticsGuillaume Ambal, Sergueï Lenglet, Alan Schmitt. 55-67 [doi]
- A compositional proof framework for FRETish requirementsEsther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle. 68-81 [doi]
- Specification and verification of a transient stackAlexandre Moine, Arthur Charguéraud, François Pottier. 82-99 [doi]
- Mechanized verification of a fine-grained concurrent queue from meta's folly librarySimon Friis Vindum, Dan Frumin, Lars Birkedal. 100-115 [doi]
- Applying formal verification to microkernel IPC at metaQuentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli. 116-129 [doi]
- Forward build systems, formallySarah Spall, Neil Mitchell, Sam Tobin-Hochstadt. 130-142 [doi]
- Formal verification of a distributed dynamic reconfiguration protocolWilliam Schultz, Ian Dardik, Stavros Tripakis. 143-152 [doi]
- A verified algebraic representation of cairo program executionJeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman. 153-165 [doi]
- Reflection, rewinding, and coin-toss in EasyCryptDenis Firsov, Dominique Unruh. 166-179 [doi]
- An extension of the framework types-to-sets for Isabelle/HOLMihails Milehins. 180-196 [doi]
- A drag-and-drop proof tacticPablo Donato, Pierre-Yves Strub, Benjamin Werner. 197-209 [doi]
- CertiStr: a certified string solverShuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader. 210-224 [doi]
- Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewritingMichael Färber. 225-238 [doi]
- Formalising lie algebrasOliver Nash. 239-250 [doi]
- Windmills of the minds: an algorithm for fermat's two squares theoremHing-Lun Chan. 251-264 [doi]
- A machine-checked direct proof of the Steiner-lehmus theoremAriel Kellison. 265-273 [doi]
- Undecidability, incompleteness, and completeness of second-order logic in CoqMark Koch, Dominik Kirst. 274-290 [doi]
- Semantic cut elimination for the logic of bunched implications, formalized in CoqDan Frumin. 291-306 [doi]
- Implementing a category-theoretic framework for typed abstract syntaxBenedikt Ahrens, Ralph Matthes, Anders Mörtberg. 307-323 [doi]
- (Deep) induction rules for GADTsPatricia Johann, Enrico Ghiorzi. 324-337 [doi]
- On homotopy of walks and spherical maps in homotopy type theoryJonathan Prieto-Cubides. 338-351 [doi]