| Event Details |
|---|
|
Thursday, December 4, 2014 Talk:
4:00 p.m., Avery 115
Reception:
3:30 p.m., Avery 348
|
Dr. Suzette Person
Researcher, NASA Langley Research CenterAbstract
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.
Speaker Bio
N/A