10 citations · 28 across the 17 of their papers we have counts for
Showing 2023Show all
3 papers · 1 filter
cs.SE2023
Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security
Yongwang Zhao, David Sanan
Formal verification of concurrent operating systems (OSs) is challenging, in particular the verification of the dynamic memory management due to its complex data structures and all…
cs.SE2023
Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications
Yongwang Zhao, David Sanan
The rely-guarantee approach is a promising way for compositional verification of concurrent reactive systems (CRSs), e.g. concurrent operating systems, interrupt-driven control sys…
cs.SE2023
Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems
Yongwang Zhao, David Sanan, Fuyuan Zhang +1
High assurance of information-flow security (IFS) for concurrent systems is challenging. A promising way for formal verification of concurrent systems is the rely-guarantee method.…