Francesco Logozzo
Research Interests
My main research interest is the analysis, the optimization and the verification of object-oriented programs through abstract interpretation
I am working on the design and the development of a language agnostic abstract interpretation-based static contract analyzer and checker for .NET
The static checker (cccheck) can be downloaded as part of the Code Contracts from the Visual Studio Gallery
You can try it online here or just watch a 2 minutes video here
The paper describing the internals of the static checker is this one
Watch the video at Channel9 (Adesso anche in italiano: Parte 1, Parte 2)
I also have fun analyzing dynamic languages, namely Javascript (More info)
Upcoming Community Service
SIGDAda HILT'13, SAS'13 (co-chair), OOPSLA'13 (Student Travel chair and Student Competition judging committee), POPL'13, Bytecode'13, VMCAI'12, Bytecode'12, Tapas'11 (co-chair), Bytecode'11, SAS'10, TAPAS'10, SAC-OOPS'10, Bytecode'10, WING'10, ... Bytecode'08 (chair), VMCAI'08 (co-chair) ...
Recent Publications
2013
- Francesco Logozzo and Matthieu Martel, Automatic Repair of Overflowing Expressions with Abstract Interpretation, in Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Electronic Proceedings in Theoretical Computer Science, September 2013
- Manuel Fahndrich and Francesco Logozzo, Proceedings of the 20th Static Analysis Symposium, Springer Verlag, June 2013
- Michael Barnett, Mehdi Bouaziz, Manuel Fahndrich, and Francesco Logozzo, A case for static analyzers in the cloud, in Bytecode 2013, , March 2013
- Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo, Automatic Inference of Necessary Preconditions, in in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13), Springer Verlag, January 2013
2012
- Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich, Inference of Necessary Field Conditions with Abstract Interpretation , in 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), Springer, December 2012
- Francesco Logozzo and Tom Ball, Modular and Verified Automatic Program Repair, in Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12), ACM SIGPLAN, 23 October 2012
- Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett, An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, in Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12), ACM SIGPLAN, 23 October 2012
- Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett, A Semantic Integrated Development Environment, in Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), ACM SIGPLAN, October 2012
- Manuel Fahndrich, Michael Barnett, Daan Leijen, and Francesco Logozzo, Integrating a Set of Contract Checking Tools into Visual Studio, in Proceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012), IEEE, 3 June 2012
- Francesco Logozzo, Our Experience with the CodeContracts Static Checker, in Proceedings of the Verified Software: Theories, Tools, and Experiments, Springer, January 2012
2011
- Manuel Fahndrich and Francesco Logozzo, Checking Compatibility of Bit Sizes in Floating Point Comparison Operations, in Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains, Electronic Proceedings in Theoretical Computer Science, September 2011
- Vincent Laviron and Francesco Logozzo, SubPolyhedra: a family of numerical abstract domains for the (more) scalable inference of linear inequalities , in International Journal on Software Tools for Technology Transfer (STTT) , Springer Verlag, June 2011
- Francesco Logozzo, Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, in Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Springer Verlag, January 2011
- Agostino Cortesi and Francesco Logozzo, Non-functional Requirements Verification by Abstract Interpretation, in Handbook of Research on Non-Functional Properties for Service-Oriented Systems: Future Directions, IGI Global, 2011
- Patrick Cousot, Radhia Cousot, and Francesco Logozzo, A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis, in Proceedings of the 38th Symposium on Programming Languages (POPL'11), Association for Computing Machinery, Inc., January 2011
- Patrick Cousot, Radhia Cousot, and Francesco Logozzo, Contract Precondition Inference from Intermittent Assertions on Collections, in Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Springer Verlag, January 2011
2010
- Manuel Fahndrich and Francesco Logozzo, Static contract checking with Abstract Interpretation, in Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010) , Springer Verlag, October 2010
- Patrick Cousot, Radhia Cousot, and Francesco Logozzo, Contract Precondition Inference from Intermittent Assertions on Collections, no. MSR-TR-2010-117, September 2010
- Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter, SPUR: A Trace-Based JIT Compiler for CIL, no. MSR-TR-2010-27, 25 March 2010
- Mike Barnett, Manuel Fahndrich, and Francesco Logozzo, Embedded Contract Languages, in ACM SAC - OOPS, Association for Computing Machinery, Inc., March 2010
- Francesco Logozzo and Herman Venter, Rapid Atomic Type Analysis by Abstract Interpretation. Application to JavaScript optimization, in Proceedings of the International Conference on Compiler Construction, Springer Verlag, March 2010
- Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter, SPUR: a trace-based JIT compiler for CIL, in Proceedings of the ACM international conference on Object oriented programming systems languages and applications, ACM, New York, NY, USA, 2010
2009
- Vincent Laviron and Francesco Logozzo, Refining Abstract Interpretation-based Static Analyses with Hints, in Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009), Springer Verlag, December 2009
- Songtao Xia, Manuel Fahndrich, and Francesco Logozzo, Inferring Dataflow Properties of User Defined Table Processors, in Proceeding of the 16th International Static Analysis Symposium (SAS'09), Springer Verlag, August 2009
- Francesco Logozzo, Class invariants as abstract interpretation of trace semantics, in Computer Languages, Systems & Structures, Elsevier , July 2009
- Francesco Logozzo, Corneliu Popeea, and Vincent Laviron, Towards a Quantitative Estimation of Abstract Interpretations, in Workshop on Quantitative Analysis of Software, Microsoft, 28 June 2009
- Michael Barnett, Manuel Fahndrich, Francesco Logozzo, Peli de Halleux, and Nikolai Tillmann, Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract, in Proc. 31st International Conference on Software Engineering (ICSE'2009) , IEEE, May 2009
- Francesco Logozzo and Vincent Laviron, SubPolyhedra: A (more) scalable approach to infer linear inequalities, in Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'09), Springer Verlag, January 2009
- Francesco Logozzo and Manuel Fahndrich, Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses, in Science of Computer Programming, Springer Verlag, 2009
2008
- Pietro Ferrara, Francesco Logozzo, and Manuel Fähndrich, Safer unsafe code for .NET, in Proceedings of the 23rd ACM Conference on Object-Oriented Programming (OOPSLA'08), Association for Computing Machinery, Inc., October 2008
- Francesco Logozzo and Manuel Fähndrich, Pentagons: A weakly relational domain for the efficient validation of array accesses, in Proceedings of the 23th ACM Symposium on Applied Computing , Association for Computing Machinery, Inc., March 2008
- Francesco Logozzo and Manuel Fähndrich, On the Relative Completeness of Bytecode Analysis versus Source Code Analysis, in Proceedings of the International Conference on Compiler Construction, Springer Verlag, 2008
- Francesco Logozzo, Doron Peled, and Lenore Zuck, Proceedings of the 9th International conference on Verification, Model checking and Abstract interpretation, Springer Verlag, 2008
- John Boyland, Dave Clarke, Gary T. Leavens, Francesco Logozzo, and Arnd Poetzsch-Heffter, Formal Techniques for Java-Like Programs: Report on the Workshop at ECOOP 2007., in Object-Oriented Technology, ECOOP 2007 Workshop Reader, Springer Verlag, 2008
Quick Links
Downloads
News
- I will talk at the ECOOP'13 summer school this July
- I will give a talk and demo of SPA at BUILD
- I will give a keynote talk at the formal methods for industry forum in Toulouse
- Read about strongest necessary preconditions here
- I've uploaded a short video demoing the code fixes feature of cccheck.
- How do you infer which conditions should hold on your object fields? Read this APLAS'12 paper...
- Come at the demo session of OOPSLA'12 to see a Semantic IDE in action. I will demo the two OOPSLA'12 papers and more!
- The paper on modular, verified and automatic program repairs has been accepted at OOPSLA'12
- The paper on proof-preserving proofs has been accepted at OOPSLA'12
- Co-chair for the next Static Analysis Symposium (SAS'13)
- Invited speaker at the prestigious ETH Colloquium. Talk was recorded, click here to watch.
- Member of POPL'13 Program Committee
- Giving an invited tutorial at the Verified Software: Theories, Tools and Experiments conference, colocated with POPL'12
- Teaching at the ECI Summer (oops winter) school
- The paper on the static analysis of array contents has been accepted to POPL'11
- The paper on precondition inference has been accepted to VMCAI'11
- I will be giving an invited talk at the Verification, Model Checking and Abstract Interpretation conference in January'11
- I will be giving an invited talk to the International conference on Formal Verification of Object-oriented Software in June
- I will be giving a lecture on CodeContracts at the ECOOP Summer school
- Now the Channel 9 is available also in Italian. Click here for part 1 (Contract specification and runtime checking) and here for part 2 (static checking via abstract interpretation)
- I have done a short Channel 9 video demoing the static checker for CodeContracts and giving some ideas on abstract interpretation
- I gave an invited talk at the ES_PASS workshop in Madrid
Short Bio
- I am a researcher in the RiSE group. I joined Microsoft Research in October 2006.
- I was a postdoctoral researcher in the abstract interpretation team at the Ecole Normale Superieure in Paris.
- I have done my Ph.D. under the supervision of Dr. Radhia Cousot. The title of the thesis is Modular static analysis of object-oriented languages.
- I am a former student of Scuola Normale Superiore of Pisa (Italy).
