Data races indicate serious concurrency bugs such as order, atomicity, and sequential consistency violations. Races are difficult to find and fix, often manifesting only in deploy...
Michael D. Bond, Katherine E. Coons, Kathryn S. Mc...
A number of programming languages use rich type systems to verify security properties of code. Some of these languages are meant for source programming, but programs written in th...
An ad hoc data format is any non-standard, semi-structured data format for which robust data processing tools are not available. In this paper, we present ANNE, a new kind of mark...
Synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, synthesis algor...
Viktor Kuncak, Mika l Mayer, Ruzica Piskac, Philip...
We define the reachability-bound problem to be the problem of finding a symbolic worst-case bound on the number of times a given control location inside a procedure is visited in ...
Dependent types provide a strong foundation for specifying and verifying rich properties of programs through type-checking. The earliest implementations combined dependency, which...