SRC04: Automatic Generation and Inference of Interface Properties from Program Source Code

Robustness and security of software are governed by various temporal properties related to interfaces. We present an approach to effectively generate a large number of formal interface properties for verification. We propose a framework to automatically infer system specific interface specifications and properties from static push-down model-checking traces.