2 papers
cs.LO2026
Generating Rely-Guarantee Conditions with the Conditional-Writes Domain
James Tobler, Graeme Smith
Abstract interpretation has been shown to be a promising technique for the thread-modular verification of concurrent programs. Central to this is the generation of interferences, i…
cs.LO2025
Detecting speculative data flow vulnerabilities using weakest precondition reasoning
Graeme Smith
Speculative execution is a hardware optimisation technique where a processor, while waiting on the completion of a computation required for an instruction, continues to execute lat…