Jules Villard

about me

I am a Software Engineer in the Static Analysis Tools team at Meta in London. I am interested in finding bugs in programs, large and small, and sometimes proving them correct. I like formal verification techniques and semantics of programming languages, especially if they are compositional.

I am currently working on the Infer static analysis platform and its Pulse memory and value analysis.

I did my PhD at ENS Cachan under the supervision of Étienne Lozes. After that I held post-doc positions at, successively, Queen Mary University London, University College London, and Imperial College London.

news

Speaker Invité at JFLA 2024
PC Member of Incorrectness 2024
PC Member of POPL 2024
Sept 2023
Invited speaker at the Summer School on Security Testing and Verification
Aug 2023
Invited speaker at the VeTSS Summer School
Dec 2021
Co-organising this year's Facebook Testing and Verification Symposium
Jun 2021
Second edition of the Infer Practitioners Workshop, co-located with PLDI 2021
Jan 2021
PC Member of CAV 2021
Jun 2020
First-ever Infer Practitioners Workshop, co-located with PLDI 2020
Jan 2019
Tutorial about writing new analyses in Infer at POPL 2019's TutorialFest

publications

Conferences and Workshops with Proceedings

LRVBDO22: Finding Real Bugs in Big Programs with Incorrectness Logic. L. Le, A. Raad, J. Villard, J. Berdine, D. Dreyer, and P. O'Hearn. OOPSLA'22, ACM, 2022. SIGPLAN Distinguished Paper Award [pdf | bib | abstract]
RBDDOV20: Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. A. Raad, J. Berdine, H.-H. Dang, D. Dreyer, P. O'Hearn, and J. Villard. CAV'20, LNCS, Springer, 2020. [pdf | bib | abstract]
RHVG16: Verifying Concurrent Graph Algorithms. A. Raad, A. Hobor, J. Villard, and P. Gardner. APLAS'16, LNCS, Springer, 2016. [pdf | bib | abstract]
RVG15: CoLoSL: Concurrent Local Subjective Logic. A. Raad, J. Villard, and P. Gardner. ESOP'15, LNCS, Springer, 2015. [pdf | bib | abstract]
HvS+14: Developments in Concurrent Kleene Algebra. T. Hoare, S. van Staden, B. Möller, G. Struth, J. Villard, H. Zhu, and P. O'Hearn. RAMiCS'14, LNCS 8428, Springer, 2014 (invited talk). [pdf | bib | abstract]
BV14: Parametric completeness for separation theories. J. Brotherston and J. Villard. In POPL'14, ACM, 2014. [pdf | bib | abstract | slides]
Also available as a UCL Research Note (RN/13/11).
HV13: The ramifications of sharing in data structures. A. Hobor and J. Villard. In POPL'13, ACM, 2013. [pdf | slides | more…]
LV12: Sharing contract-obedient endpoints. É. Lozes, J. Villard . In ICE'12, EPTCS 104, Open Publishing Association, 2012. [pdf | bib | abstract]
LV11: Reliable contracts for unreliable half-duplex communications. É. Lozes, J. Villard. In WS-FM'11, LNCS 7176, Springer, 2011. [pdf | bib | abstract]
JLTV11: Multiple congruence relations, first-order theories on terms, and the frames of the applied π-calculus. F. Jacquemard, É. Lozes, R. Treinen, and J. Villard . In TOSCA'11, LNCS 6993, Springer, 2011. [pdf | bib | abstract]
VLC10: Tracking heaps that hop with Heap-Hop. J. Villard, É. Lozes, and C. Calcagno. In TACAS'10, LNCS 6015, Springer, 2010. [pdf | bib | abstract]
VLC09: Proving copyless message passing. J. Villard, É. Lozes and C. Calcagno. In APLAS'09 , LNCS 5904, Springer, 2009. [pdf | bib | abstract]
LV08: A spatial equational logic for the applied π-calculus. É. Lozes and J. Villard. In CONCUR'08, LNCS 5201, Springer, 2008. [pdf | bib | abstract]

Journals

LV14: Shared contract-obedient channels. É. Lozes, J. Villard. Science of Computer Programming, 2014. [ pdf | bib | abstract]
OPVH14: On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra. P. O'Hearn, R. L. Petersen, J. Villard, and A. Hussain. Journal of Logical and Algebraic Methods in Programming, 2014. [pdf |bib |abstract]
LV10: A spatial equational logic for the applied π-calculus. É. Lozes and J. Villard. Distributed Computing 23(1), 2010. [pdf | bib | abstract]

Conferences and Workshops without Proceedings

Vil12: The ramification rule of separation logic. J. Villard. High Confidence Software and Systems Conference, 2012. [abstract | slides]
Vil09: Proving copyless message passing. J. Villard. Young Researchers Workshop on Concurrency Theory, 2009. [pdf | slides]

PhD Dissertation

Vil11: Heaps and hops. J. Villard. LSV, ENS Cachan, France, 2011. [pdf | bib | abstract | slides]

Unpublished

BV14: Bi-Intuitionistic Boolean Bunched Logic. J. Brotherston and J. Villard. UCL Research Note RN/14/06, 2014. [pdf | bib | abstract]

Here be wyverns! Verifying LLVM IR with llStar. J. Villard. [Draft | slides]