Abstract is missing.
- Scalable Formal Machine ModelsGreg Morrisett. 1-3 [doi]
- Mechanized Semantics for Compiler VerificationXavier Leroy. 4-6 [doi]
- Automation in Computer-Aided Cryptography: Proofs, Attacks and DesignsGilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin. 7-8 [doi]
- Program Certification by Higher-Order Model CheckingNaoki Kobayashi 0001. 9-10 [doi]
- A Formally-Verified Alias AnalysisValentin Robert, Xavier Leroy. 11-26 [doi]
- Mechanized Verification of Computing Dominators for Formalizing CompilersJianzhou Zhao, Steve Zdancewic. 27-42 [doi]
- On the Correctness of an Optimising Assembler for the Intel MCS-51 MicroprocessorDominic P. Mulligan, Claudio Sacerdoti Coen. 43-59 [doi]
- An Executable Semantics for CompCert CBrian Campbell. 60-75 [doi]
- Producing Certified Functional Code from Inductive SpecificationsPierre-Nicolas Tollitte, David Delahaye, Catherine Dubois. 76-91 [doi]
- The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One RoofLukas Bulwahn. 92-108 [doi]
- Proving Concurrent NoninterferenceAndrei Popescu 0001, Johannes Hölzl, Tobias Nipkow. 109-125 [doi]
- Noninterference for Operating System KernelsToby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein. 126-142 [doi]
- Compositional Verification of a Baby Virtual Memory ManagerAlexander Vaynberg, Zhong Shao. 143-159 [doi]
- Shall We Juggle, Coinductively?Keisuke Nakano. 160-172 [doi]
- Proof Pearl: Abella Formalization of λ-Calculus Cube PropertyBeniamino Accattoli. 173-187 [doi]
- A String of Pearls: Proofs of Fermat's Little TheoremHing-Lun Chan, Michael Norrish. 188-207 [doi]
- Compact Proof Certificates for Linear LogicKaustuv Chaudhuri. 208-223 [doi]
- Constructive Completeness for Modal Logic with Transitive ClosureChristian Doczkal, Gert Smolka. 224-239 [doi]
- Rating Disambiguation ErrorsAndrea Asperti, Wilmer Ricciotti. 240-255 [doi]
- A Formal Proof of Square Root and Division Elimination in Embedded ProgramsPierre Néron. 256-272 [doi]
- Coherent and Strongly Discrete Rings in Type TheoryThierry Coquand, Anders Mörtberg, Vincent Siles. 273-288 [doi]
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and DerivativesSylvie Boldo, Catherine Lelay, Guillaume Melquiond. 289-304 [doi]