Research and Activities

My research focuses on automatic software verification, program analysis, and automatic detection of critical software bugs. I have co-designed and co-developed several code analysis tools both in academia and in industry. In particular, the the co-inventor of Infer an open source static analysis tool used at Meta and by many companies around the world (e.g., Amazon, Microsoft,…)

Currently I leading the WhatsApp Dev Infra Org. My team builds tool and infrastructure to help WhatsApp back-end developers shipping more reliable, secure, and private code at a faster pace to the over 2 billions WhatsApp users.

Awards

• IEEE Computer Society Cybersecurity Award For Practice 2021. The IEEE Computer Society Cybersecurity Award for Practice is intended to recognize individuals and small teams who are generating transformative cybersecurity capabilities that have been realized.
• ACM SIGPLAN POPL 2019 Most Influential Paper Award. Presented annually to the author(s) of a paper presented at the POPL held 10 years prior to the award year. The papers are judged by their influence over the past decade.
• SIGPLAN Most influential OOPSLA paper award 2018. Presented annually to the author(s) of a paper presented at the OOPSLA held 10 years prior to the award year. The papers are judged by their influence over the past decade.
• CAV Award 2016. The CAV award is given annually at the CAV conference for fundamental contributions to the field of Computer-Aided Verification.
• Royal Academy of Engineering Silver Medal 2014. The Royal Academy of Engineering Silver Medal recognises outstanding contribution to UK engineering, that also results in successful market exploitation.
• Roger Needham Award, 2012. The Roger Needham Award is made annually by the British Computer Society for a distinguished research contribution in computer science by a UK based researcher within ten years of their PhD.

Software Tools

• INFER (2009-2013) Initially a commercial verification tool for memory safety of C. Industrial users includes Airbus, ARM, Toyota, Mitsubishi, Lawrence Livermore National Labo- ratory. Currently INFER is open source and it’s being developed mainly inside Meta.
• Abductor (2008-2010). Highly-scalable program analysis tool proving memory safety for program manipulating heaps. The first tool performing deep-heap analysis able to scale to millions of line of code.
• Space Invader (2005-2008). Program analysis tool proving safety properties for pro- grams manipulating heaps. Space Invader was the first automatic tool able to verify the use of pointer structures in entire industrial programs (Microsoft and Linux device drivers up to 10K LOC). Released on BSD license in 2008.
• jStar (2008). Program Verification tool for Java programs. The first automatic verification tool able to verify programs extensively used by developers in real-world Java applications.
• Mutant (2006) Program analysis tool proving termination of program manipulating heaps. In collaboration with Microsoft Research (Cambridge).

Program Committee appointments

• VMCAI 2021
• Infer 2021
• ECOOP 2019
• VSTTE 2018 5
• CAV 2017
• Nasa Formal Methods 2017
• SOAP 2016
• CAV 2015
• RV 2015
• MOVEP 2014
• POPL 2014, San Diego, USA.
• FM 2014 (The 19th International Symposium on Formal Methods), Singapore.
• TAPAS 2013
• NFM 2012 (The 4th NASA Formal Methods Symposium 2012). Norfolk, Virginia, USA.
• FM 2012 (The 18th International Symposium on Formal Methods). Paris, France.
• MOVEP 2012 (The 10th School on MOdelling and VErifying parallel Processes), Marseilles, France.
• BOOGIE 2012 (2nd International Workshop on Intermediate Verification Languages), Berkeley, California.
• CONCUR 2011 (International Conference on Concurrency Theory), Aachen, Germany.
• VMCAI 2011 (International Conference on Verification, Model Checking, and Abstract Interpretation). Autstin, USA.
• ICFEM 2011 (The 13th International Conference on Formal Engineering Methods), Durham, UK.
• FOOL 2011 (International workshop on Foundations of Object-Oriented Languages). Portland, USA.
• NSAD 2011 (International Workshop on Numerical and Symbolic Abstract Domains), Venice, Italy.
• ESOP 2010 (European Symposium on Programming). Paphos, Cyprus.
• APLAS 2010 (Asian Symposium on Programming Languages and Systems). Shanghai, China.
• FMICS 2010 (International Workshop on Formal Methods for Industrial Critical Systems). Antwerp, Belgium.
• FTfJP 2010 (Workshop on Formal Techniques for Java-like Programs). Maribor, Slovenia.
• SAC 2010 (ACM Symposium On Applied Computing)
• SSV 2010 (Systems Software Verification). Vancouver Canada.
• NSAD 2010 (International Workshop on Numerical and Symbolic Abstract Domains). Perpignan, France. Sierre and Lausanne, Switzerland.
• ISMM 2009 (International Symposium on Memory Management). Dublin, Ireland.
• VSTTE 2009 (Workshop on Verified Software: Theory, Tools, and Experiments). Eindhoven, The Netherlands.
• FTfJP 2009 (Workshop on Formal Techniques for Java-like Programs). Genova, Italy.
• APV 2009 (Symposium on Automatic Program Verification). Rio Cuarto, Argentina.
• YR-Concur 2009 (Young Researchers Workshop on Concurrency Theory). Bologna, Italy.
• INFINITY 2008 (International Workshop on Verification of Infinite-State Systems). Toronto, Canada.
• GT-VC 2007 (Graph Transformation for Verification and Concurrency). Lisbon Portugal.
• GT-VC 2006 (Graph Transformation for Verification and Concurrency). Bonn, Germany.
• PhD Student Workshop 2002, at FMOODS 2002. Enschede, The Netherlands.