The following pages link to Andrew W. Appel (Q1663237):
Displaying 18 items.
- VST-Floyd: a separation logic tool to verify correctness of C programs (Q1663238) (← links)
- A trustworthy proof checker (Q1826468) (← links)
- A list-machine benchmark for mechanized metatheory (Q1945921) (← links)
- Abstraction and subsumption in modular verification of C programs (Q2147702) (← links)
- (Q2723406) (← links)
- Compositional CompCert (Q2819813) (← links)
- (Q2871863) (← links)
- A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow (Q2894335) (← links)
- Mostly Sound Type System Improves a Foundational Program Verifier (Q2938037) (← links)
- Verified Software Toolchain (Q3000569) (← links)
- (Q3026313) (← links)
- A very modal model of a modern, major, general type system (Q3189790) (← links)
- Generalizations of the sethi‐ullman algorithm for register allocation (Q4727417) (← links)
- C-language floating-point proofs layered with VST and Flocq (Q5014364) (← links)
- Corrigendum: C floating-point proofs layered with VST and Flocq (Q5014365) (← links)
- Multimodal Separation Logic for Reasoning About Operational Semantics (Q5415628) (← links)
- A solver for arrays with concatenation (Q6156632) (← links)
- Efficient extensional binary tries (Q6156636) (← links)
