Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title: Program Inconsistency Detection using Weakest Preconditions
presenter: Aaron Tomb
time: Tuesday, 25 January 2011, 10:30am
location:Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract: Many tools exist to automate the search for defects in software source code. However, many of these tools have not been widely applied, partly because they tend to work least well in the most common case: on large software systems that have only partial specifications describing correct behavior — often a collection of independent assertions sprinkled throughout the program.
Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumptions. Existing approaches to inconsistency detection have used intentionally unsound techniques aimed at bug-finding rather than verification. In this dissertation, we describe an inconsistency detection analysis that subsumes previous work and is instead based on the foundation of the weakest precondition calculus.
We have applied our analysis to a large body of widely-used open-source software, and found a number of bugs.
bio: Aaron Tomb has worked in Research and Development at Galois since 2007. His research interests include type systems, programming language semantics, automated program analysis and defect detection. At Galois, he has conducted research into tools to help understand the structure of programs and systems for secure web collaboration. Aaron leads the Program Analysis research program at Galois.
Aaron has a B.S. and M.S. in computer science from the University of California, Santa Cruz. This talk is based on his nearly-completed Ph.D. research. His academic work has focused on programming language theory, and particularly on the use of advanced programming language technology to improve software reliability. This has involved type theory, formal methods, program analysis, and a bit of subjective exploration into what makes languages pleasant to use.