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.



Conferences and Workshops with Proceedings

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]
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]
Verifying Concurrent Graph Algorithms. A. Raad, A. Hobor, J. Villard, and P. Gardner. APLAS'16, LNCS, Springer, 2016. [pdf | bib | abstract]
CoLoSL: Concurrent Local Subjective Logic. A. Raad, J. Villard, and P. Gardner. ESOP'15, LNCS, Springer, 2015. [pdf | bib | abstract]
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]
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).
The ramifications of sharing in data structures. A. Hobor and J. Villard. In POPL'13, ACM, 2013. [pdf | slides | more…]
Sharing contract-obedient endpoints. É. Lozes, J. Villard . In ICE'12, EPTCS 104, Open Publishing Association, 2012. [pdf | bib | abstract]
Reliable contracts for unreliable half-duplex communications. É. Lozes, J. Villard. In WS-FM'11, LNCS 7176, Springer, 2011. [pdf | bib | abstract]
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]
Tracking heaps that hop with Heap-Hop. J. Villard, É. Lozes, and C. Calcagno. In TACAS'10, LNCS 6015, Springer, 2010. [pdf | bib | abstract]
Proving copyless message passing. J. Villard, É. Lozes and C. Calcagno. In APLAS'09 , LNCS 5904, Springer, 2009. [pdf | bib | abstract]
A spatial equational logic for the applied π-calculus. É. Lozes and J. Villard. In CONCUR'08, LNCS 5201, Springer, 2008. [pdf | bib | abstract]


Shared contract-obedient channels. É. Lozes, J. Villard. Science of Computer Programming, 2014. [ pdf | bib | abstract]
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]
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

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

PhD Dissertation

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


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]