6 papers
An Executable Formal Model of the VHDL in Isabelle/HOL
Wilayat Khan, Zhe Hou, David Sanan +3
In the hardware design process, hardware components are usually described in a hardware description language. Most of the hardware description languages, such as Verilog and VHDL,…
A formalisation of the SPARC TSO memory model for multi-core machine code
Zhe Hou, David Sanan, Alwen Tiu +2
SPARC processors have many applications in mission-critical industries such as aviation and space engineering. Hence, it is important to provide formal frameworks that facilitate t…
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…