ISSTA 2022
Mon 18 - Fri 22 July 2022 Online

Program verifiers are widely used to prove the correctness of critical software systems. To build confidence in their results, it is important to develop testing frameworks that help detect bugs in verifiers. Inspired by the success of fuzzing in finding bugs in compilers and SMT solvers, we have built the first fuzzing and differential testing framework for Dafny, a high-level programming language with a Floyd-Hoare-style program verifier and compilers to C#, Java, Go, and Javascript.

This paper presents our experience building and using XDsmith, a testing framework that targets the entire XDsmith toolchain, from verification to compilation. XDsmith randomly generates Dafny programs that are annotated with preconditions, postconditions, and assertions. These programs are used to test the soundness and precision of the Dafny verifier, and to perform differential testing on the four XDsmith compilers. Using XDsmith, we uncovered 31 bugs across the XDsmith verifier and compilers, each of which has been confirmed by the XDsmith developers. Moreover, 8 of these bugs have been fixed in the mainline release of XDsmith.

Thu 21 Jul

Displayed time zone: Seoul change

01:20 - 02:00
Session 1-5: Static Analysis and Specifications Testing DTechnical Papers at ISSTA 1
01:20
20m
Talk
Testing Dafny (Experience Paper)
Technical Papers
Ahmed Irfan Amazon Web Services, Sorawee Porncharoenwase University of Washington, Zvonimir Rakamaric Amazon Web Services, Neha Rungta Amazon Web Services, Emina Torlak Amazon Web Services
DOI
01:40
20m
Talk
The Raise of Machine Learning Hyperparameter Constraints in Python CodeACM SIGSOFT Distinguished Paper
Technical Papers
Ingkarat Rak-amnouykit Rensselaer Polytechnic Institute, Ana Milanova Rensselaer Polytechnic Institute, Guillaume Baudart Inria; ENS; PSL University, Martin Hirzel IBM Research, Julian Dolby IBM Research, USA
DOI
08:40 - 09:40
Session 2-10: Static Analysis and Specifications Testing BTechnical Papers at ISSTA 2
Chair(s): Behnaz Hassanshahi Oracle Labs, Australia
08:40
20m
Talk
Path-Sensitive Code Embedding via Contrastive Learning for Software Vulnerability Detection
Technical Papers
Xiao Cheng University of Technology Sydney, Guanqin Zhang University of Technology Sydney, Haoyu Wang Huazhong University of Science and Technology, China, Yulei Sui University of Technology Sydney
DOI
09:00
20m
Talk
Testing Dafny (Experience Paper)
Technical Papers
Ahmed Irfan Amazon Web Services, Sorawee Porncharoenwase University of Washington, Zvonimir Rakamaric Amazon Web Services, Neha Rungta Amazon Web Services, Emina Torlak Amazon Web Services
DOI
09:20
20m
Talk
The Raise of Machine Learning Hyperparameter Constraints in Python CodeACM SIGSOFT Distinguished Paper
Technical Papers
Ingkarat Rak-amnouykit Rensselaer Polytechnic Institute, Ana Milanova Rensselaer Polytechnic Institute, Guillaume Baudart Inria; ENS; PSL University, Martin Hirzel IBM Research, Julian Dolby IBM Research, USA
DOI