2 papers
cs.LO2025
Compositional Verification in Concurrent Separation Logic with Permissions Regions
Quang Loc Le
Concurrent separation logic with fractional permissions (CSLPerm) provides a promising reasoning system to verify most complex sequential and concurrent fine-grained programs. The…
cs.LO2025
Cyclic Proofs in Hoare Logic and its Reverse
James Brotherston, Quang Loc Le, Gauri Desai +1
We examine the relationships between axiomatic and cyclic proof systems for the partial and total versions of Hoare logic and those of its dual, known as reverse Hoare logic (or so…