The following pages link to Andrew W. Appel (Q1663237):
Displaying 39 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)
- Separation Logic for Small-Step cminor (Q3523161) (← links)
- Formal Verification of Coalescing Graph-Coloring Register Allocation (Q3558221) (← links)
- (Q4343027) (← links)
- (Q4343028) (← links)
- Shrinking lambda expressions in linear time (Q4376489) (← links)
- (Q4379577) (← links)
- Modern Compiler Implementation in Java (Q4406527) (← links)
- Generalizations of the sethi‐ullman algorithm for register allocation (Q4727417) (← links)
- Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf (Q4819003) (← links)
- Dependent types ensure partial correctness of theorem provers (Q4819651) (← links)
- Efficient Substitution in Hoare Logic Expressions (Q4921508) (← 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)
- Connecting Higher-Order Separation Logic to a First-Order Outside World (Q5041105) (← links)
- Bringing Order to the Separation Logic Jungle (Q5055998) (← links)
- Verified heap theorem prover by paramodulation (Q5168877) (← links)
- A semantic model of types and machine instructions for proof-carrying code (Q5178856) (← links)
- A theory of indirection via approximation (Q5255071) (← links)
- Lambda-splitting (Q5348869) (← links)
- Verified Compilation for Shared-Memory C (Q5410696) (← links)
- Multimodal Separation Logic for Reasoning About Operational Semantics (Q5415628) (← links)
- Oracle Semantics for Concurrent Separation Logic (Q5458409) (← links)
- Program Logics for Certified Compilers (Q5494381) (← links)
- Verification, Model Checking, and Abstract Interpretation (Q5898611) (← links)
- Verification, Model Checking, and Abstract Interpretation (Q5901901) (← links)
- A solver for arrays with concatenation (Q6156632) (← links)
- Efficient extensional binary tries (Q6156636) (← links)
