2 papers
cs.LO2026
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…
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…