Automated Verification of Go Programs via Bounded Model Checking
The Go programming language offers a wide range of primitives to coordinate lightweight threads, i.e., channels, waitgroups, and mutexes — all of which may cause concurrency bugs. Static checkers that guarantee the absence of bugs are essential to help programmers avoid these costly errors before their code is executed. However existing tools either miss too many bugs or cannot handle large programs. To address these limitations, we propose a static checker for Go programs which relies on performing bounded model checking of their concurrent behaviours. In contrast to previous works, our approach deals with large code bases, supports programs that have statically unknown parameters, and is extensible to additional concurrency primitives. Our work includes a detailed presentation of the extraction algorithm from Go programs to models, an algorithm to automatically check programs with statically unknown parameters, and a large scale evaluation of our approach. The latter shows that our approach outperforms the state-of-the-art.
Thu 18 NovDisplayed time zone: Hobart change
22:00 - 23:00 | |||
22:00 20mTalk | Modeling Team Dynamics for the Characterization and Prediction of Delays in User Stories Research Papers Elvan Kula Delft University of Technology, Arie van Deursen Delft University of Technology, Netherlands, Georgios Gousios Facebook & Delft University of Technology Pre-print | ||
22:20 20mTalk | DeepMemory: Model-based Memorization Analysis of Deep Neural Language Models Research Papers Derui Zhu Technical University of Munich, Jinfu Chen Centre for Software Excellence, Huawei, Canada, Weiyi Shang Concordia University, Xuebing Zhou Huawei Munich Research Center, Jens Grossklags Technical University of Munich, Ahmed E. Hassan Queen's University | ||
22:40 20mTalk | Automated Verification of Go Programs via Bounded Model Checking Research Papers Pre-print |