I am an engineering at Arm, focusing on formal verification and security. My work involves in examining specifications, protocol designs and software implementations and prototyping verification strategies for increasing their quality and security. Most common techniques we are using includes model checking, fuzzing, and even theorem prover. 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.
I have contributed to Veracruz project, a software stack mainly written in Rust that provides a uniform interfact and infrastructure to untilise 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.
shale.xiong [AT] arm.com
110 Fulbourn Rd,
Cambridge CB1 9NJ, UK
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 mordern 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 performancers.
- The Phantom Of The Opera
- Jean Paul Gaultier Fashion Freak Show
- Les Misérables
- Best of Enemies
- Cirque du Soleil Kurios
- Brokeback Mountain
- Matthew Bourne’s Romeo and Juliet
- Don Quixote
- Jersey Boys
- Lion King
- A Mirror
- Cirque du Soleil Alegria
- New Works
Gaming, on PC
I like RPG, simulation and strategy games. Some games I like:
- World of Warcraft
- Civilization V and VI
- Tropico 4, 5 and 6
- Two Point Hospital
- Total War: Warhammer II
- The Elder Scrolls V
- Mess Effect 3
- Divinity: Original Sin 1 and 2
- The Witcher 3: Wild Hunt
- Pillars of Eternity 1 and 2
- Age of Wonders 4
- Baldur’s Gate 3
There are few games I am no long play but I still watch matches:
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 dicards any tile; or it can be tiles other players discards in his/her turn.