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 - 16:00: Paper Presentations - A2-Testing and Debugging 1 at Goguryeo
Chair(s): Na MengVirginia Tech
icse-2020-papers15:00 - 15:12
Boyuan ChenYork University, Zhen Ming (Jack) JiangYork University
Authorizer link Pre-print
icse-2020-papers15:12 - 15:24
Brittany JohnsonUniversity of Massachusetts Amherst, Yuriy BrunUniversity of Massachusetts Amherst, Alexandra MeliouUniversity of Massachusetts Amherst
Link to publication DOI Pre-print Media Attached
icse-2020-Journal-First15:24 - 15:32
Yi ZengConcordia University, Jinfu ChenConcordia University, Canada, Weiyi ShangConcordia University, Tse-Hsun (Peter) ChenConcordia University
Authorizer link Pre-print
icse-2020-New-Ideas-and-Emerging-Results15:32 - 15:38
Jude ArokiamOntario Tech University, Jeremy BradburyOntario Tech University
icse-2020-Journal-First15:38 - 15:46
Rubing HuangJiangsu University, Weifeng SunJiangsu University, Yinyin XuJiangsu University, Haibo ChenJiangsu University, Dave ToweyUniversity of Nottingham Ningbo China, Xin XiaMonash University
icse-2020-Software-Engineering-in-Practice15:46 - 15:58
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