I am an engineering at Arm, focusing on formal verification and security. My work involves in defining and examining specifications, protocol designs and software implementations and prototyping verification strategies for increasing their quality and security. Most common techniques I am using includes model checking, fuzzing, and even theorem-prover. I also investigate in custom tools. Although a full autogenerated verification stack is probably the ultimate goal and dream of many verification specialists, my work put emphasis on scalability and bugs hunting with a minimum interruption to the product development cycle.

Since 2024, I have mainly contributed to the diy7, a part of herdtools7. Although it targets various architectures, the former generates litmus tests for memory model of AArch64. The latter, currently maintained by the entire team, also includes (1) herd7 that simulates the expected behaviours of memory events from litmus tests, (2) cat that is a DSL to specify memory model, and (3) many memory model specifications using cat for different architectures with different architecture features.

From 2020 to 2024, I have contributed to Veracruz project, a software stack mainly written in Rust that provides a uniform interface and infrastructure to utilise trusted execution environment (TEE), which includes Arm CCA being one of the backend. Separately, I have contributed and now driven a CBMC verification stack to verify the functional correctness and some concurrency aspects with the help of tailored ghost state of Realm Management Monitor (RMM), a firmware of Arm CCA.

I received PhD in Computer Science from Verified Trustworthy Software Specification Group, Dept. of Computing, Imperial College, supervised by Prof. Philippa Gardner, working on verification of concurrent programs and consistency models of distributed systems and databases. I received MSc. in Advanced Computing from Imperial College London in 2015, and BEng. in Software Engineering from Southwest Jiaotong University (西南交通大学), China in 2014.

Contact

Email:

shale.xiong [AT] arm.com

Address:

110 Fulbourn Rd,
Cambridge CB1 9NJ, UK

My Hobbies

Cooking and Restaurants

I enjoying cooking for myself of a Chinese style food based on available ingredients. I grew up in Changsha, Hunan and spent another 4 years as undergraduate in Chengdu, Sichuan, so I am familiar to spicy and chilli food.

I spent a portion of my leisure and travelling on trying restaurants, in particular, those often being referred as fine-dining restaurants. I try to write up for fun and post here for all those restaurants I visited in the past. Of course, it is not my main work and I am not a professional.

Stage Show and Theatre

I enjoy going to the theatre, mostly for musical, play and ballet. I also like circus show and modern dance etc. I usually go to London for theatre since I live in Cambridge, only less an hour train from London. In general, I like a good story and admire the skills of the performances.

Gaming, on PC

I like RPG, simulation and strategy games. Some games I like:

There are few games I am no long play but I still watch matches:

Mahjong (麻将)

It is a game played by four people. In China, different areas have slightly different rules but the general rules are similar.

Every player has 13 tiles in their hands and can only be seen by players themselves by default. There are 3 suits, each of which contains four duplicated tiles from number one to nine. Some areas also have extra tiles and each of them also have four duplications (with few exceptions, but they do not really affect the rule but affect how much a player(s) pay when losing).

Initially players get 13 tiles and afterwards the game is organised by rounds until a player(s) win. A round is divided into four turns for the four players. In the counter-clock order players draw a new tile and then discard a tile chosen by themselves . Note that a play always has 13 tiles either hidden or seen by everyone (there is a mechanism to reveal tiles). To win, a player’s 13 tiles plus an extra one need to form certain pattern. The extra one can be the immediate new tile the player draws before s/he discards any tile; or it can be tiles other players discards in his/her turn.