Jules Villard

about me

I am a Software Engineer in the Static Analysis Tools team in Facebook London, working on Infer.

Before that I was a post-doc working successively at Queen Mary University London, University College London, and Imperial College London.

I did my PhD at École Normale Supérieure de Cachan under the supervision of Étienne Lozes, and my undergrad at École Normale Supérieure de Lyon.



Conferences and Workshops with Proceedings

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]