Skip to main content
SpringerLink
Log in

Certified Programs and Proofs

Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, Proceedings

  • Conference proceedings
  • © 2012

Overview

Editors:
  1. Chris Hawblitzel

    1. Microsoft Research, Redmond, USA

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Dale Miller

    1. INRIA Saclay and LIX, Ecole Polytechnique, Palaiseaux Cedex, France

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  • Up-to-date results
  • Fast-track conference proceedings
  • State-of-the-art research

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 7679)

Part of the book sub series: Theoretical Computer Science and General Issues (LNTCS)

Included in the following conference series:

Conference proceedings info: CPP 2012.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (22 papers)

  1. Front Matter

    Download chapter PDF

  2. Scalable Formal Machine Models

    • Greg Morrisett
    Pages 1-3

  3. Mechanized Semantics for Compiler Verification

    • Xavier Leroy
    Pages 4-6

  4. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs

    • Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin
    Pages 7-8

  5. Program Certification by Higher-Order Model Checking

    • Naoki Kobayashi
    Pages 9-10

  6. A Formally-Verified Alias Analysis

    • Valentin Robert, Xavier Leroy
    Pages 11-26

  7. Mechanized Verification of Computing Dominators for Formalizing Compilers

    • Jianzhou Zhao, Steve Zdancewic
    Pages 27-42

  8. On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor

    • Dominic P. Mulligan, Claudio Sacerdoti Coen
    Pages 43-59

  9. An Executable Semantics for CompCert C

    • Brian Campbell
    Pages 60-75

  10. Producing Certified Functional Code from Inductive Specifications

    • Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois
    Pages 76-91

  11. The New Quickcheck for Isabelle

    • Lukas Bulwahn
    Pages 92-108

  12. Proving Concurrent Noninterference

    • Andrei Popescu, Johannes Hölzl, Tobias Nipkow
    Pages 109-125

  13. Noninterference for Operating System Kernels

    • Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Gerwin Klein
    Pages 126-142

  14. Compositional Verification of a Baby Virtual Memory Manager

    • Alexander Vaynberg, Zhong Shao
    Pages 143-159

  15. Shall We Juggle, Coinductively?

    • Keisuke Nakano
    Pages 160-172

  16. Proof Pearl: Abella Formalization of λ-Calculus Cube Property

    • Beniamino Accattoli
    Pages 173-187

  17. A String of Pearls: Proofs of Fermat’s Little Theorem

    • Hing-Lun Chan, Michael Norrish
    Pages 188-207

  18. Compact Proof Certificates for Linear Logic

    • Kaustuv Chaudhuri
    Pages 208-223

  19. Constructive Completeness for Modal Logic with Transitive Closure

    • Christian Doczkal, Gert Smolka
    Pages 224-239

  20. Rating Disambiguation Errors

    • Andrea Asperti, Wilmer Ricciotti
    Pages 240-255
Back to top

Other volumes

  1. Certified Programs and Proofs

Keywords

About this book

This book constitutes the refereed proceedings of the Second International Conference on Certified Programs and Proofs, CPP 2012, held in Kyoto, Japan, in December 2012. The 18 revised regular papers presented were carefully reviewed and selected from 37 submissions. They deal with those topics in computer science and mathematics in which certification via formal techniques is crucial.

Editors and Affiliations

  • Microsoft Research, Redmond, USA

    Chris Hawblitzel

  • INRIA Saclay and LIX, Ecole Polytechnique, Palaiseaux Cedex, France

    Dale Miller

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation