Rene Just
University of Washington
Computer Science and Engineering
Computer Science Building, Room 151
Faculty Host: Yuriy Brun
Hardly any area exists in our everyday life that is not affected by software, yet software remains buggy. These software bugs not only affect correctness and robustness but also cause severe security vulnerabilities. Software verification can provide strong guarantees about important (security) properties of a program, but full verification of software correctness is prohibitively expensive for most applications. Software testing is the predominant approach for assuring software correctness and robustness, but software testing is not complete and can only increase confidence. It is therefore important to measure the adequacy of testing techniques.
In this talk, I will present some of my work in verification and testing that aims to improve software security and robustness. First, I will present a model and type system to statically verify the absence of information-flow malware in mobile apps. I will also describe techniques I developed to significantly reduce the number of false positives and an evaluation on real-world apps. For 72 apps, totaling 570,000 lines of code, the results show that the model and type system are effective and that the developer burden is low. Second, I will present my work on improving software testing. In particular, I will focus on mutation analysis, which measures the adequacy of testing techniques using artificial faults (mutants). I will present an empirical study that involved more than 350 real faults and 230,000 mutants, in which I have shown that mutants are a valid substitute for real faults, and that mutation analysis is significantly more effective than code coverage.
A reception will be held at 3:40 in the atrium, outside the presentation room.