Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP

DOI10.1007/978-3-030-91265-9_5zbMath1498.68018OpenAlexW3212264767MaRDI QIDQ2154026

Huibiao Zhu, Lili Xiao

Publication date: 13 July 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-91265-9_5

zbMATH Keywords

trace semanticsalgebraic lawsrelaxed memory modelMCA ARMv8 architectureunifying theories of programming (UTP)

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical problems of computer architecture (68M07) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Linearizability on hardware weak memory models
• From algebra to operational semantics
• Full abstraction for a shared-variable parallel language
• A wide-spectrum language for verification of programs on weak memory models
• A denotational semantics for SPARC TSO
• Laws of programming

This page was built for publication: Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP