10 citations · 28 across the 17 of their papers we have counts for
4 papers · 1 filter
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…
Executable Operational Semantics of Solidity
Jiao Jiao, Shuanglong Kan, Shang-Wei Lin +3
Bitcoin has attracted everyone's attention and interest recently. Ethereum (ETH), a second generation cryptocurrency, extends Bitcoin's design by offering a Turing-complete program…
An Executable Operational Semantics for Rust with the Formalization of Ownership and Borrowing
Shuanglong Kan, Zhe Chen, David Sanan +2
Rust is an emergent systems programming language highlighting memory safety by its Ownership and Borrowing System (OBS). The existing formal semantics for Rust only covers limited…