Tomorrow, December 4, Suzette Person, Ph.D., will give a talk at 4:00 p.m. in 115 Avery Hall. A reception will precede it at 3:30 p.m. in 348 Avery Hall. The name of the talk is "Making Programming with Assertions More Practical."
Description:
Annotating functional correctness properties of code, using assertions or other executable contracts, offers a number of benefits in automated conformance checking of program behaviors to expected properties, e.g., to support bug finding. Effectively utilizing program properties in practice, however, is complicated by two basic factors. One, it requires the properties to first be specified and then maintained such that they correctly reflect the expected behaviors of the code, even as it evolves. Two, it requires efficient and cost-effective techniques to check the actual behaviors of the code with respect to the specified properties. In this work, we present two techniques to help software developers specify and check functional properties encoded as assertions.The first technique, iDiscovery, leverages symbolic execution to improve the quality of auto-generated invariants to support the property specification process. The second technique, iProperty, performs incremental checking of functional properties to help reduce the computational cost of property checking during initial development of the properties. We also show how iProperty can be used in synergy with a program behavior differencing technique to analyze properties as the code evolves.
If this sounds interesting to you, attend the colloquium tomorrow afternoon.