Jules Villard

I'm a Research Assistant in the Programming Principles, Logic and Verification group of UCL in London, working on program verification and concurrency.

I did my PhD at LSV in Cachan (near Paris) under the supervision of Étienne Lozes, during which I created the Heap-Hop tool for the verification of heap-manipulating message-passing programs.

Software

I am actively developing Heap-Hop. It verifies message-passing programs against their Hoare-style separation logic specifications on the one hand, and the communication protocols they implement, expressed using communicating finite state machines, on the other hand.

While Heap-Hop has been great for verifying toy programs written in an idealised language, being able to verify real programs is a different kind of fun! My new tool, LStar, is about verifying LLVM "bitcode" programs using separation logic.

Publications

In progress

BV13: Parametric Completeness for Separation Theories
J. Brotherston and J. Villard. UCL Research Note RN/13/11, 2013. [PDF | BibTeX | abstract]
OPVH: On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra
P. O'Hearn, R. L. Petersen, J. Villard and A. Hussain.
LV: Sharing Contract-Obedient Endpoints (extended version)
É. Lozes, J. Villard . /dd>

Recent and Upcoming talks

13/06/13: I talked about Heap-Hop at the Verified Concurrent Programmes workshop at Microsoft Research Cambridge.
10/04/13: I went to Microsoft Research Cambridge to talk about ramification.
01/04/13: I was at a Dagstuhl seminar about accelerator programming.
15/03/13: I am giving a talk at the theory seminar in Birmingham.
25/01/13: I presented our paper at POPL in Rome.
20/09/12: I was invited to the Wessex Theory Seminar and presented our work on ramification.
16/06/12: In Stockholm to talk about sharing endpoints at the ICE workshop.
31/05/12: Seminar at MSR Cambridge on reasoning about programs with sharing.
15/05/12: Seminar at Princeton University on reasoning about programs with sharing.
14/05/12: Seminar at Yale University on reasoning about programs with sharing.
10/05/12: Talk at the HCSS conference about “The Ramification Rule of Separation Logic”, in Annapolis, Maryland.
25/02/12: I gave a talk about Heap-Hop at the CS seminar of the School of Computing at NUS, in Singapore. I was visiting there for 2 weeks. [slides]
30/06/11: Heap-Hop presentation at the VERIDYC Verification and Synthesis workshop in Grenoble. [slides]
12/05/11: Lab seminar about message-passing program verification at the MoVe team, in Marseille. [slides]
19/04/11: Heap-Hop is at the Behavioural Types workshop, in Lisbon. [slides]
15/04/11: Heap-Hop is at the Dublin Concurrency Workshop. [slides]
31/03/11: I presented our work on “Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus” at the TOSCA conference of ETAPS 2011, in Saarbrücken. [slides | paper]
18/02/11: PhD: defended! [slides | thesis]

Program Committee

PC member of the FTfJP 2012 workshop of ECOOP 2012 in Beijing.

Jules Villard

Contact

Software

Publications

In progress

Journals

Conferences

Workshops with Proceedings

Conferences and Workshops without Proceedings

Thesis

Recent and Upcoming talks

Program Committee