Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich
We present a new static analysis to infer necessary field conditions for object-oriented programs. A necessary field condition is a property that should hold on the fields of a given object, for otherwise there exists a calling context leading to a failure due to bad object state. Our analysis also infers the provenance of the necessary condition, so that if a necessary field condition is violated then an explanation containing the sequence of method calls leading to a failing assertion can be produced. When the analysis is restricted to readonly fields, i.e., fields that can only be set in the initialization phase of an object, it infers object invariants. We provide empirical evidence on the usefulness of necessary field conditions by integrating the analysis into cccheck, our static analyzer for .NET. Robust inference of readonly object field invariants was the #1 request from cccheck users.
|Published in||10th Asian Symposium on Programming Languages and Systems (APLAS 2012)|
Francesco Logozzo, Shuvendu Lahiri, Manuel Fahndrich, and Sam Blackshear. Verification Modulo Versions: Towards Usable Verification, ACM SIGPLAN, June 2014.
Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo. Automatic Inference of Necessary Preconditions, Springer Verlag, January 2013.
Francesco Logozzo. Practical Specification and Verification with CodeContracts, ACM, November 2013.
Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett. A Semantic Integrated Development Environment, ACM SIGPLAN, October 2012.
Manuel Fahndrich and Francesco Logozzo. Static contract checking with Abstract Interpretation, Springer Verlag, October 2010.
Mike Barnett, Manuel Fahndrich, and Francesco Logozzo. Embedded Contract Languages, Association for Computing Machinery, Inc., March 2010.
Francesco Logozzo and Tom Ball. Modular and Verified Automatic Program Repair, ACM SIGPLAN, 23 October 2012.