Francesco Logozzo

Research Interests

My main research goal is Usable Program Verification. Usable verification consists of effective verification tools and specification languages which help the programmer to produce more reliable code. An usable verification tool provides feedback in the early stages of the program development. It is precise (few false alarms), automatic,  user-oriented, and scalable. It helps the programmer, instead of being helped by her!

I think abstract interpretation is the right approach towards usable verification, and I co-authored several static analysis tools based on abstract interpretation. The latest one is the popular CodeContracts static checker (cccheck) that 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

ECOOP'15, SAS'14, VSTTE'14, HOPA'14SIGDAda HILT'13, SAS'13 (co-chair), OOPSLA'13 (Student Travel chair and Student Competition judging committee), POPL'13, Bytecode'13VMCAI'12, Bytecode'12, Tapas'11 (co-chair), Bytecode'11, SAS'10, TAPAS'10SAC-OOPS'10, Bytecode'10, WING'10, ... Bytecode'08 (chair), VMCAI'08 (co-chair) ...

Recent Publications









    • Verification modulo versions paper accepted at PLDI'14
    • Giving talk at the 1st MSR/IMDEA workshop
    • Tracing compilation is Abstract Interpretation: see the paper accepted at POPL'14
    • I will be at two panels and giving a CodeContracts tutorial at ACM SigAda HILT 2013
    • Watch my BUILD talk! From minute 25
    • I will lecture at the ECOOP'13 summer school this coming 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).