me

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. I did my undergrad at École Normale Supérieure de Lyon,

news

publications

Conferences and Workshops with Proceedings

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]