7 citations · 21 across the 13 of their papers we have counts for
10 papers · 1 filter
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.…
A Verified Timsort C Implementation in Isabelle/HOL
Yu Zhang, Yongwang Zhao, David Sanan
Formal verification of traditional algorithms are of great significance due to their wide application in state-of-the-art software. Timsort is a complicated and hybrid stable sorti…
An Event-based Compositional Reasoning Approach for Concurrent Reactive Systems
Yongwang Zhao, David Sanan, Fuyuan Zhang +1
Reactive systems are composed of a well defined set of input events that the system reacts with by executing an associated handler to each event. In concurrent environments, event…
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…
Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication
Yongwang Zhao, David Sann, Fuyuan Zhang +1
Assurance of information flow security by formal methods is mandated in security certification of separation kernels. As an industrial standard for separation kernels, ARINC 653 ha…
Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B
Yongwang Zhao, Zhibin Yang, David Sanan +1
Standards play the key role in safety-critical systems. Errors in standards could mislead system developer's understanding and introduce bugs into system implementations. In this p…
A survey on formal specification and verification of separation kernels
Yongwang Zhao
Separation kernels are fundamental software of safety and security-critical systems, which provide to their hosted applications spatial and temporal separation as well as controlle…