Formal certification of a compiler back-end or
From MaRDI portal
Publication:5348912
DOI10.1145/1111037.1111042zbMath1369.68124OpenAlexW2129695855MaRDI QIDQ5348912
Publication date: 21 August 2017
Published in: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1111037.1111042
compiler optimizationprogram proofCoq theorem proversemantic preservationcompiler transformationcertified compilation
Related Items
A FORMAL PROOF OF THE KEPLER CONJECTURE, versat: A Verified Modern SAT Solver, Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms, TWAM: a certifying abstract machine for logic programs, Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs, Directly reflective meta-programming, Formal Certification of a Resource-Aware Language Implementation, A Certified Data Race Analysis for a Java-like Language, Practical Tactics for Separation Logic, A Hoare Logic for the State Monad, An Introduction to Certificate Translation, Certified Static Analysis by Abstract Interpretation, Code-carrying theories, Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems, Computational logic: its origins and applications, Proof-carrying code from certified abstract interpretation and fixpoint compression, Mechanized semantics for the clight subset of the C language, A formally verified compiler back-end, Mechanising a type-safe model of multithreaded Java with a verified compiler, Calculating Certified Compilers for Non-deterministic Languages, A formal treatment of the role of verified compilers in secure computation, Mechanized Verification of CPS Transformations, System-level non-interference of constant-time cryptography. I: Model, Formal verification of synchronous data-flow program transformations toward certified compilers, CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types, Extracting functional programs from Coq, in Coq, Extraction in Coq: An Overview, A formal C memory model for separation logic, Theoretical and practical approaches to the denotational semantics for MDESL based on UTP, Certifying compilers using higher-order theorem provers as certificate checkers, Function extraction, The area method. A recapitulation, A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation, SMT proof checking using a logical framework, Unnamed Item, Grammar semantics, analysis and parsing by abstract interpretation, Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves, Preservation of Proof Obligations from Java to the Java Virtual Machine, A Short Presentation of Coq, Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL, Runtime verification of embedded real-time systems, System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory, Verified Software Toolchain, A self-certifying compilation framework for WebAssembly, Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC, Formal verification of a C-like memory model and its uses for verifying program transformations, Flag-based big-step semantics, Building Certified Static Analysers by Modular Construction of Well-founded Lattices, Pollack-inconsistency, Verified Compilation and the B Method: A Proposal and a First Appraisal, Relational bytecode correlations, Structural Abstract Interpretation: A Formal Study Using Coq, An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model, Inferring functional properties of matrix manipulating programs by abstract interpretation, Extensible and Efficient Automation Through Reflective Tactics, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Beyond Provable Security Verifiable IND-CCA Security of OAEP, Certifying Findel derivatives for blockchain, Coinductive big-step operational semantics, A formalization of multi-tape Turing machines, A Verified Runtime for a Verified Theorem Prover, Automatic Parallelization and Optimization of Programs by Proof Rewriting, Inter-program Properties, Pervasive Theory of Memory, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Formal Verification for High-Assurance Behavioral Synthesis, Operating system verification---an overview, Formalizing Arrow's theorem, Linear capabilities for fully abstract compilation of separation-logic-verified code, A formalization of SQL with nulls, Type-Safe Code Transformations in Haskell
Uses Software
