Pages that link to "Item:Q5348912"
From MaRDI portal
The following pages link to Formal certification of a compiler back-end or (Q5348912):
Displaying 50 items.
- Function extraction (Q436372) (← links)
- The area method. A recapitulation (Q437042) (← links)
- Runtime verification of embedded real-time systems (Q479806) (← links)
- Flag-based big-step semantics (Q516041) (← links)
- Certifying compilers using higher-order theorem provers as certificate checkers (Q633302) (← links)
- Grammar semantics, analysis and parsing by abstract interpretation (Q655410) (← links)
- Relational bytecode correlations (Q710672) (← links)
- A formalization of multi-tape Turing machines (Q744986) (← links)
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) (Q832157) (← links)
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms (Q832310) (← links)
- Directly reflective meta-programming (Q848742) (← links)
- Proof-carrying code from certified abstract interpretation and fixpoint compression (Q860842) (← links)
- Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves (Q928671) (← links)
- Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) (← links)
- Coinductive big-step operational semantics (Q1012129) (← links)
- Operating system verification---an overview (Q1040002) (← links)
- Formalizing Arrow's theorem (Q1040010) (← links)
- TWAM: a certifying abstract machine for logic programs (Q1629962) (← links)
- Mechanising a type-safe model of multithreaded Java with a verified compiler (Q1663233) (← links)
- A formal C memory model for separation logic (Q1694027) (← links)
- Inferring functional properties of matrix manipulating programs by abstract interpretation (Q1791274) (← links)
- An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (Q2031429) (← links)
- Certifying Findel derivatives for blockchain (Q2043802) (← links)
- A formalization of SQL with nulls (Q2102947) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory (Q2228439) (← links)
- A self-certifying compilation framework for WebAssembly (Q2234063) (← links)
- System-level non-interference of constant-time cryptography. I: Model (Q2417947) (← links)
- Formal verification of synchronous data-flow program transformations toward certified compilers (Q2418653) (← links)
- A resource semantics and abstract machine for \textit{Safe}: a functional language with regions and explicit deallocation (Q2437794) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Code-carrying theories (Q2643124) (← links)
- Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems (Q2643128) (← links)
- Mechanized semantics for the clight subset of the C language (Q2655325) (← links)
- A formally verified compiler back-end (Q2655327) (← links)
- A formal treatment of the role of verified compilers in secure computation (Q2669248) (← links)
- Extensible and Efficient Automation Through Reflective Tactics (Q2802496) (← links)
- A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
- Type-Safe Code Transformations in Haskell (Q2866331) (← links)
- versat: A Verified Modern SAT Solver (Q2891429) (← links)
- Calculating Certified Compilers for Non-deterministic Languages (Q2941174) (← links)
- Verified Software Toolchain (Q3000569) (← links)
- Beyond Provable Security Verifiable IND-CCA Security of OAEP (Q3073706) (← links)
- A Verified Runtime for a Verified Theorem Prover (Q3088011) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Formal Certification of a Resource-Aware Language Implementation (Q3183530) (← links)
- A Certified Data Race Analysis for a Java-like Language (Q3183531) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- A Hoare Logic for the State Monad (Q3183544) (← links)
- An Introduction to Certificate Translation (Q3184785) (← links)
