Testing Dafny (experience paper)
Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamarić, Neha Rungta, Emina Torlak
Abstract
Verification toolchains 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 these toolchains. 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.
Topics & Concepts
Fuzz testingComputer scienceProgramming languageCorrectnessCompilerJavaScriptJavaHoare logicSoftware testingSoftware engineeringSoftwareSoftware Testing and Debugging TechniquesSoftware Reliability and Analysis ResearchAdvanced Malware Detection Techniques