Formal Verification of Out-of-Order Execution Using Incremental Flushing
No abstract available.
Related papers
- Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86 OOPSLA 2020
- Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving CAV 2002
- Verification of an Advanced mips-Type Out-of-Order Execution Algorithm CAV 2004
- ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction - (Competition Contribution) TACAS 2025
- Putting Weak Memory in Order via a Promising Intermediate Representation PLDI 2023
- Sound Gradual Verification with Symbolic Execution POPL 2024
- Promising-ARM/RISC-V: a simpler and faster operational concurrency model PLDI 2019
- Interfaces for stack inspection JFP 2005