The design and implementation of a certifying compiler

No abstract is available for this paper.

• Publication year

  1998

• Venue

  ACM-SIGPLAN Symposium on Programming Language Design and Implementation

• Publication date

  1998-05-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/277650.277752
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Alias Types

  2000cited by this paper
• Certifying Compilation and Run-Time Code Generation

  1999cited by this paper
• Java Virtual Machine

  1998cited by this paper
• Safe, Untrusted Agents Using Proof-Carrying Code

  1998cited by this paper
• Compiling with proofs

  1998cited by this paper
• Translation Validation

  1998cited by this paper
• Software reliability via run-time result-checking

  1997cited by this paper
• Efficient Representation and Validation of Logical Proofs

  1997cited by this paper
• From system F to typed assembly language

  1997cited by this paper
• 7 Conclusion and Results 5 Functional Speciication of the Logger/checker

  1997cited by this paper
• Safe kernel extensions without run-time checking

  1996influential reference
• The Java Language Specification

  1996influential reference
• The Java Virtual Machine Specification

  1996cited by this paper
• TIL: a type-directed optimizing compiler for ML

  1996cited by this paper
• The VLISP verified PreScheme compiler

  1995cited by this paper
• {28 () Vlisp: a Veriied Implementation of Scheme *

  1995cited by this paper
• VLISP: A verified implementation of Scheme

  1995cited by this paper
• A framework for defining logics

  1993cited by this paper
• PVS: A Prototype Verification System

  1992cited by this paper
• PVS: A Prototype . . .

  1992cited by this paper
• A Framework for De ning LogicsRobert Harper

  1987cited by this paper
• Using Domain Algebras to Prove the Correctness of a Compiler

  1985cited by this paper
• HOL : A machine oriented formulation of higher order logic

  1985cited by this paper
• Deciding Linear Inequalities by Computing Loop Residues

  1981cited by this paper
• Stanford Pascal Verifier user manual

  1979cited by this paper
• Simplification by Cooperating Decision Procedures

  1979cited by this paper
• More on Advice on Structuring Compilers and Proving them Correct

  1979cited by this paper
• Advice on structuring compilers and proving them correct

  1973cited by this paper
• Computational logic

  1949cited by this paper

• Verifiable Provenance of Software Artifacts with Zero-Knowledge Compilation

  2026cites this paper
• A Certifying Proof Assistant for Synthetic Mathematics in Lean

  2026cites this paper
• Firmware Secure Updates meet Formal Verification

  2025cites this paper
• End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation

  2025cites this paper
• Auditable Algorithms for Approximate Model Counting

  2023cites this paper
• FuzzyFlow: Leveraging Dataflow To Find and Squash Program Optimization Bugs

  2023cites this paper
• OBSan: An Out-Of-Bound Sanitizer to Harden DNN Executables

  2023cites this paper
• Qualification of Proof Assistants, Checkers, and Generators: Where Are We and What Next?

  2023cites this paper
• Defect Categorization in Compilers: A Multi-vocal Literature Review

  2023cites this paper
• S×C4IoT: A Security-by-contract Framework for Dynamic Evolving IoT Devices

  2022cites this paper
• This paper is included in the Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation

  2021cites this paper
• Leo: A Programming Language for Formally Verified, Zero-Knowledge Applications

  2021cites this paper
• Certifying the synthesis of heap-manipulating programs

  2021cites this paper
• Typsysteme auf Bit-Ebene für Assembler-Sprachen

  2021cites this paper
• SANRAZOR: Reducing Redundant Sanitizer Checks in C/C++ Programs

  2021cites this paper
• Resource Bound Certi cation �

  2020cites this paper
• Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings

  2020cites this paper
• Verified Rust Monitors for Lola Specifications

  2020cites this paper
• Compiling Dependent Types Without Continuations

  2019cites this paper
• Verified Software. Theories, Tools, and Experiments: 10th International Conference, VSTTE 2018, Oxford, UK, July 18–19, 2018, Revised Selected Papers

  2018influential citation
• On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency

  2018cites this paper
• TWAM: A Certifying Abstract Machine for Logic Programs

  2018influential citation
• A Case for Certifying Compilers in Industrial Automation

  2018cites this paper
• Stopping injection attacks with proof carrying code and structured data

  2018cites this paper
• Stopping Injection Attacks with Code and Structured Data

  2018cites this paper
• Verification by Reduction to Functional Programs

  2017cites this paper
• Verified Translation Validation of Static Analyses

  2017cites this paper
• ASLR: How Robust Is the Randomness?

  2017cites this paper
• Intersert: Assertions on Distributed Process Interaction Sessions

  2017cites this paper
• Full-stack static security analysis for the Java platform

  2016cites this paper
• A Study of Security Isolation Techniques

  2016cites this paper
• Proof-Carrying Apps: Contract-Based Deployment-Time Verification

  2016cites this paper
• Verified Proofs of Higher-Order Masking

  2015cites this paper
• Verification and code generation for invariant diagrams in Isabelle

  2015cites this paper
• Proofs of Higher-Order Masking Overview of an article for the Research Seminar in Cryptography

  2015cites this paper
• Advanced Development of Certified OS Kernels

  2015cites this paper
• Model Checking for Dynamic Datapaths

  2014cites this paper
• A defense framework against malware and vulnerability exploits

  2014cites this paper
• Source-free binary mutation for offense and defense

  2014cites this paper
• Secure virtual architecture: security for commodity software systems

  2014cites this paper
• Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers (dissertation, updated version)

  2014cites this paper
• Compilation certifiée de SCADE/LUSTRE

  2013cites this paper
• The state of the art of application restrictions and sandboxes: A survey of application-oriented access controls and their shortfalls

  2013cites this paper
• Certification of static analysis in many-sorted first-order logic. (Analyse statique certifiée en logique du premier ordre multi-sortée)

  2013cites this paper
• On Verification by Translation to Recursive Functions An Overview of the Leon Verification System

  2013cites this paper
• An Empirical Evaluation of Automated Theorem Provers in Software Certification

  2013cites this paper
• Linear and Affine Typing of Continuation-Passing Style

  2013cites this paper
• Automatic generation of compiler backends

  2013cites this paper
• Defending Against the Buffer Overflows: A Static Approach Using Proof-Carrying Code

  2013cites this paper
• Energy-efficient Designs For Securing Embedded and Mobile Computing Systems

  2013cites this paper
• A language-independent static checking system for coding conventions

  2013cites this paper
• An overview of the Leon verification system: verification by translation to recursive functions

  2013cites this paper
• A Performance-Oriented Monitoring System for Security Properties in Cloud Computing Applications

  2012cites this paper
• Frankenstein: Stitching Malware from Benign Binaries

  2012cites this paper
• Languages and Security

  2012cites this paper
• A Certified Constraint Solver over Finite Domains

  2012cites this paper
• Building safe PaaS clouds: A survey on security in multitenant software platforms

  2012cites this paper
• Inférence de certificats pour la vérification statique des programmes Java

  2012influential citation
• Microkernel Verification Down To Assembly Extending the seL 4 verification

  2012cites this paper
• mTags: augmenting microkernel messages with lightweight metadata

  2012cites this paper
• Security and privacy in automotive on-board networks

  2012cites this paper
• Verification of Imperative Programs in Scala

  2012cites this paper
• Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols

  2012cites this paper
• Towards a Secure Federated Information System

  2012cites this paper
• Scheduling and deployment of large-scale applications on Cloud platforms. (Ordonnancement et déploiement d'applications de gestion de données à grande échelle sur des plates-formes de type Clouds)

  2012cites this paper
• A verifiable low-level concurrent programming model based on colored Petri nets

  2011cites this paper
• Model Checking Approach to Secure Host Access Enforcement of Mobile Tasks in Scientific Workflows

  2011cites this paper
• A Method for Certifying Code in Trust-By-Policy-Adherence

  2011cites this paper
• Towards Formally Verified Optimizing Compilation in Flight Control Software

  2011cites this paper
• Bringing Theory to Practice : Predictability and Performance in Embedded Systems

  2011cites this paper
• An Abstract Model of Certificate Translation

  2011cites this paper
• Safety properties and memory bound analysis in a functional language without a garbage collector

  2011cites this paper
• Efficient Encoding of SystemC/TLM in Promela

  2011cites this paper
• Interpretational overhead in system software

  2011cites this paper
• Generation of Certifiably Correct Programs from Formal Models

  2011cites this paper
• Abstract Certification of Java Programs in Rewriting Logic

  2011cites this paper
• Certifying compilers using higher-order theorem provers as certificate checkers

  2011cites this paper
• Functional pearl: every bit counts

  2010cites this paper
• Compilación de programas seguros

  2010cites this paper
• Static analysis by abstract interpretation of embedded critical software

  2010cites this paper
• Security of Software on Mobile Devices

  2010cites this paper
• A verified compiler for Handel-C

  2010influential citation
• Towards the Future Internet

  2010cites this paper
• Towards Optimizing Certified Compilation in Flight Control Software ∗

  2010cites this paper
• Trust Extension as a Mechanism for Secure Code Execution on Commodity Computers

  2010cites this paper
• A Proof Carrying Code Framework for Inlined Reference Monitors in Java Bytecode

  2010cites this paper
• A Type System for Access Control Views in Object-Oriented Languages

  2010cites this paper
• An Extended Proof-Carrying Code Framework for Security Enforcement

  2010cites this paper
• Explicitly typed static single-assignment form

  2010cites this paper
• Runtime monitoring for next generation Java ME platform

  2010cites this paper
• Completeness of automatically generated instruction selectors

  2010cites this paper
• Detecting bugs in register allocation

  2010cites this paper
• Generating Bijections between HOAS and the Natural Numbers

  2010cites this paper
• A Certifying Compiler for Clike Subset of C Language

  2010cites this paper
• Securing Mobile-Agent Systems through Collaboration

  2010cites this paper
• A Pointer Logic for Verification of Pointer Programs

  2009cites this paper
• GRACE TECHNICAL REPORTS Proceedings of the Sixth Asian Workshop on Foundations of Software

  2009cites this paper
• An Introduction to Certificate Translation

  2009cites this paper
• Retrofitting programs for complete security mediation

  2009cites this paper
• Fabric: a platform for secure distributed computation and storage

  2009cites this paper