Certified programs and proofs : second international conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, proceedings, Chris Hawblitzel, Dale Miller (eds.)

Resource Information

The instance Certified programs and proofs : second international conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, proceedings, Chris Hawblitzel, Dale Miller (eds.) represents a material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries. This resource is a combination of several types including: Instance, Electronic.

Image

http://images.btol.com/ContentCafe/Jacket.aspx?UserID=ebsco-test&Password=ebsco-test&Return=T&Value=9783642353079&Type=L

Label

Certified programs and proofs : second international conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, proceedings, Chris Hawblitzel, Dale Miller (eds.)

Title remainder

second international conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, proceedings

Statement of responsibility

Chris Hawblitzel, Dale Miller (eds.)

Instantiates

• Certified programs and proofs : second international conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, proceedings

Publication

• Berlin | New York, Springer, ©2012

Antecedent source

unknown

Bibliography note

Includes bibliographical references and author index

Carrier category

online resource

Carrier category code

• cr

Carrier MARC source

rdacarrier

Color

multicolored

Content category

text

Content type code

• txt

Content type MARC source

rdacontent

Contents

• A Formally-Verified Alias Analysis
• Valentin Robert and Xavier Leroy
• Mechanized Verification of Computing Dominators for Formalizing Compilers
• Jianzhou Zhao and Steve Zdancewic
• On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor
• Dominic P. Mulligan and Claudio Sacerdoti Coen
• An Executable Semantics for CompCert C
• Brian Campbell
• Producing Certified Functional Code from Inductive Specifications
• Pierre-Nicolas Tollitte, David Delahaye and Catherine Dubois
• Scalable Formal Machine Models
• The New Quickcheck for Isabelle: Random, Exhaustive and Symbolic Testing under One Roof
• Lukas Bulwahn
• Greg Morrisett
• Mechanized Semantics for Compiler Verification
• Xavier Leroy
• Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs
• Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech and Santiago Zanella Béguelin
• Program Certification by Higher-Order Model Checking
• Naoki Kobayashi
• Proof Pearl: Abella Formalization of [lambda]-Calculus Cube Property
• Beniamino Accattoli
• A String of Pearls: Proofs of Fermat's Little Theorem
• Hing-Lun Chan and Michael Norrish
• Compact Proof Certificates for Linear Logic
• Kaustuv Chaudhuri
• Constructive Completeness for Modal Logic with Transitive Closure
• Christian Doczkal and Gert Smolka
• Rating Disambiguation Errors
• Andrea Asperti and Wilmer Ricciotti
• Proving Concurrent Noninterference
• A Formal Proof of Square Root and Division Elimination in Embedded Programs
• Pierre Neron
• Coherent and Strongly Discrete Rings in Type Theory
• Thierry Coquand, Anders Mörtberg and Vincent Siles
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• Sylvie Boldo, Catherine Lelay and Guillaume Melquiond
• Andrei Popescu, Johannes Hölzl and Tobias Nipkow
• Noninterference for Operating System Kernels
• Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein
• Compositional Verification of a Baby Virtual Memory Manager
• Alexander Vaynberg and Zhong Shao
• Shall We Juggle, Coinductively?
• Keisuke Nakano

Control code

819661495

Dimensions

unknown

Extent

1 online resource.

File format

unknown

Form of item

online

Isbn

9783642353079

Level of compression

unknown

Media category

computer

Media MARC source

rdamedia

Media type code

• c

Other control number

10.1007/978-3-642-35308-6

Quality assurance targets

not applicable

Record ID

.b130027315

Reformatting quality

unknown

Sound

unknown sound

Specific material designation

remote

System control number

(OCoLC)819661495