Pages that link to "Item:Q2655325"
From MaRDI portal
The following pages link to Mechanized semantics for the clight subset of the C language (Q2655325):
Displayed 20 items.
- Verified abstract interpretation techniques for disassembling low-level self-modifying code (Q287369) (← links)
- The rewriting logic semantics project: a progress report (Q393080) (← links)
- Toward compositional verification of interruptible OS kernels and device drivers (Q1663225) (← links)
- A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data (Q1739908) (← links)
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle (Q2119971) (← links)
- Reasoning about iteration and recursion uniformly based on big-step semantics (Q2154025) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM (Q2233462) (← links)
- Translating Xd-C programs to MSVL programs (Q2290648) (← links)
- A formally verified compiler back-end (Q2655327) (← links)
- Concrete Memory Models for Shape Analysis (Q2814114) (← links)
- A Concrete Memory Model for CompCert (Q2945624) (← links)
- The Rewriting Logic Semantics Project: A Progress Report (Q3088267) (← links)
- (Q5020649) (← links)
- Ott: Effective tool support for the working semanticist (Q5189646) (← links)
- A Formalization of the C99 Standard in HOL, Isabelle and Coq (Q5200133) (← links)
- (Q5866349) (← links)
- (Q5875431) (← links)
- A Verified LL(1) Parser Generator (Q5875434) (← links)
- Analysis and Transformation of Constrained Horn Clauses for Program Verification (Q6063893) (← links)