Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett
We present SIDE, a Semantic Integrated Development Environment. SIDE uses static analysis to enrich existing IDE features and also adds new features. It augments the way existing compilers find syntactic errors - in real time, as the programmer is writing code without execution - by also finding semantic errors, e.g., arithmetic expressions that may overflow. If it finds an error, it suggests a repair in the form of code - e.g., providing an equivalent yet non-overflowing expression. Repairs are correct by construction. SIDE also enhances code refactoring (by suggesting precise yet general contracts), code review (by answering what-if questions), and code searching (by answering questions like “find all the callers where x < y”).
SIDE is built on the top of CodeContracts and the Roslyn CTP. CodeContracts provide a lightweight and programmer-friendly specification language. SIDE uses the CodeContracts static checker (based on Abstract Interpretation) to obtain a deep semantic understanding of what the program does.
|Published in||Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012)|
Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett. An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, ACM SIGPLAN, 23 October 2012.
Francesco Logozzo and Tom Ball. Modular and Verified Automatic Program Repair, ACM SIGPLAN, 23 October 2012.
Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich. Inference of Necessary Field Conditions with Abstract Interpretation , Springer, December 2012.
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.
Manuel Fahndrich and Francesco Logozzo. Static contract checking with Abstract Interpretation, Springer Verlag, October 2010.