4 citations · 6 across the 6 of their papers we have counts for
6 papers
K-CIRCT: A Layered, Composable, and Executable Formal Semantics for CIRCT Hardware IRs
Jianhong Zhao, Jinhui Kang, Yongwang Zhao
CIRCT, an open-source EDA framework akin to LLVM for software, is a foundation for various hardware description languages. Despite its crucial role, CIRCT's lack of formal semantic…
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…
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…
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.…
Refinement-based Specification and Security Analysis of Separation Kernels
Yongwang Zhao, David Sanan, Fuyuan Zhang +1
Assurance of information-flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for improving safety, ARINC 653 has…
High-Assurance Separation Kernels: A Survey on Formal Methods
Yongwang Zhao, David Sanan, Fuyuan Zhang +1
Separation kernels provide temporal/spatial separation and controlled information flow to their hosted applications. They are introduced to decouple the analysis of applications in…