Write a Blog >>
ICSE 2020
Mon 5 - Sun 11 October 2020 Yongsan-gu, Seoul, South Korea
Wed 7 Oct 2020 15:00 - 15:20 at TBD6 - Software Verification

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.

Wed 7 Oct

14:00 - 15:40: Paper Presentations - Software Verification at TBD6
icse-2020-papers14:00 - 14:20
Martin KelloggUniversity of Washington, Seattle, Manli RanUniversity of California, Riverside, Manu SridharanUniversity of California Riverside, Martin SchäfAmazon Web Services, USA, Michael D. ErnstUniversity of Washington, USA
Demonstrations14:20 - 14:30
Kush JainThe University of Texas at Austin, Karl PalmskogUniversity of Texas at Austin, Ahmet CelikFacebook, Inc., Emilio Jesús Gallego AriasINRIA, Milos GligoricThe University of Texas at Austin
icse-2020-New-Ideas-and-Emerging-Results14:30 - 14:40
Jude AnilTCS Research, Sumanth PrabhuTCS Research, Kumar MadhukarTCS Innovation Labs (TRDDC), R Venkatesh
icse-2020-papers14:40 - 15:00
Alexandra BugariuETH Zurich, Peter MüllerETH Zurich
icse-2020-Software-Engineering-in-Practice15:00 - 15:20
Nathan ChongAmazon, Byron CookAmazon, Konstantinos KallasUniversity of Pennsylvania, Kareem KhazemAmazon, Felipe R. MonteiroAmazon Web Services, Daniel Schwartz-NarbonneAmazon, n.n., Serdar TasiranAmazon, n.n., Michael TautschnigAmazon Web Services, Mark R. TuttleAmazon
Demonstrations15:20 - 15:30
Zhenbang ChenCollege of Computer, National University of Defense Technology, Changsha, PR China, Hengbiao YuNational University of Defense Technology, Xianjin FuNational University of Defense Technology, Ji WangSchool of Computer, National University of Defense Technology, China
icse-2020-New-Ideas-and-Emerging-Results15:30 - 15:40
Alyas AlmaawiThe University of Texas at Austin, Nima DiniUniversity of Texas at Austin, Cagdas YelenThe University of Texas at Austin, Milos GligoricThe University of Texas at Austin, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Sarfraz KhurshidUniversity of Texas at Austin