Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- research-articleJanuary 2016
A program logic for concurrent objects under fair scheduling
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesPages 385–399https://doi.org/10.1145/2837614.2837635Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying lock-freedom of non-blocking objects, much less efforts are focused on ...
Also Published in:
ACM SIGPLAN Notices: Volume 51 Issue 1 - ArticleSeptember 2011
Extending ITL with Interleaved Programs for Interactive Verification
TIME '11: Proceedings of the 2011 Eighteenth International Symposium on Temporal Representation and ReasoningPage 7https://doi.org/10.1109/TIME.2011.31The talk presents extensions of ITL that make it a powerful logic to reason about interleaved programs with recursive procedures. The extensions have been implemented in the interactive theorem prover KIV.
- ArticleSeptember 2011
Interleaved Programs and Rely-Guarantee Reasoning with ITL
TIME '11: Proceedings of the 2011 Eighteenth International Symposium on Temporal Representation and ReasoningPages 99–106https://doi.org/10.1109/TIME.2011.12This paper presents a logic that extends basicITL with explicit, interleaved programs. The calculus is based on symbolic execution, as previously described. We extend this former work here, by integrating the logic with higher-order logic, adding ...