Write a Blog >>
ICSE 2020
Wed 24 June - Thu 16 July 2020
Tue 7 Jul 2020 15:46 - 15:58 at Goguryeo - A2-Testing and Debugging 1 Chair(s): Na Meng

This experience report describes a style of applying symbolic model checking developed over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous C-based systems, e.g., custom hypervisors, encryption code, boot loaders, and the FreeRTOS operating system. Using our methodology, we find that we can prove the correctness of industrial low-level C-based systems with reasonable effort and predictability. Furthermore, AWS developers are increasingly writing their own formal specifications. All proofs discussed in this paper are publicly available on GitHub.

Tue 7 Jul
Times are displayed in time zone: (UTC) Coordinated Universal Time change

15:00 - 15:12
Talk
Technical Papers
Boyuan ChenYork University, Zhen Ming (Jack) JiangYork University
Authorizer link Pre-print
15:12 - 15:24
Talk
Technical Papers
Brittany JohnsonUniversity of Massachusetts Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Alexandra MeliouUniversity of Massachusetts Amherst
Link to publication DOI Pre-print Media Attached
15:24 - 15:32
Talk
Journal First
Yi ZengConcordia University, Jinfu ChenConcordia University, Canada, Weiyi ShangConcordia University, Tse-Hsun (Peter) ChenConcordia University
Authorizer link Pre-print
15:32 - 15:38
Talk
New Ideas and Emerging Results
Jude ArokiamOntario Tech University, Jeremy BradburyOntario Tech University
15:38 - 15:46
Talk
Journal First
Rubing HuangJiangsu University, Weifeng SunJiangsu University, Yinyin XuJiangsu University, Haibo ChenJiangsu University, Dave ToweyUniversity of Nottingham Ningbo China, Xin XiaMonash University
15:46 - 15:58
Talk
Software Engineering in Practice
Nathan ChongAmazon, Byron CookAmazon, Konstantinos KallasUniversity of Pennsylvania, Kareem KhazemAmazon, Felipe R. MonteiroAmazon, Daniel Schwartz-NarbonneAmazon, n.n., Serdar TasiranAmazon, n.n., Michael TautschnigAmazon Web Services, Mark R. TuttleAmazon
Pre-print Media Attached