The following pages link to Verified Software Toolchain (Q3000569):
Displaying 15 items.
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (Q287277) (← 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)
- Safe functional systems through integrity types and verified assembly (Q2220814) (← links)
- From Rewriting Logic, to Programming Language Semantics, to Program Verification (Q2945730) (← links)
- Temporary Read-Only Permissions for Separation Logic (Q2988642) (← links)
- Verified Characteristic Formulae for CakeML (Q2988660) (← links)
- Relational Decomposition (Q3087994) (← links)
- AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code (Q3179279) (← links)
- Concise Read-Only Specifications for Better Synthesis of Programs with Pointers (Q5041091) (← links)
- Local Reasoning for Global Graph Properties (Q5041096) (← links)
- All-Path Reachability Logic (Q5170834) (← links)
- Formally-verified round-off error analysis of Runge-Kutta methods (Q6149594) (← links)
- A solver for arrays with concatenation (Q6156632) (← links)
- Efficient extensional binary tries (Q6156636) (← links)
