Contact

me
email
address
University College London
Dept. of Computer Science
66-72 Gower Street
London WC1E 6BT

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.

Publications

Journals

LV10

A Spatial Equational Logic for the Applied π-Calculus

É. Lozes and J. Villard. Distributed Computing 23(1), pages 61-83, 2010. [PDF | BibTeX | abstract]

Conferences

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, pages 166-185. Springer, 2011. [PDF | BibTeX | abstract]
VLC10

Tracking Heaps that Hop with Heap-Hop

J. Villard, É. Lozes and C. Calcagno. In TACAS'10, LNCS 6015, pages 275-279. Springer, 2010. [PDF | BibTeX | abstract]
VLC09

Proving Copyless Message Passing

J. Villard, É. Lozes and C. Calcagno. In APLAS'09 , LNCS 5904, pages 194-209. Springer, 2009. [PDF | BibTeX | abstract]
LV08

A Spatial Equational Logic for the Applied π-Calculus

É. Lozes and J. Villard. In CONCUR'08, LNCS 5201, pages 387-401. Springer, 2008. [PDF | BibTeX | abstract]

Workshops

LV11

Reliable Contracts for Unreliable Half-Duplex Communications

É. Lozes, J. Villard . To appear in WS-FM'11, LNCS. Springer, 2011. [PDF | BibTeX | abstract]

Thesis

Vil11

Heaps and Hops

J. Villard. LSV, ENS Cachan, France, 2011. [PDF | BibTeX | abstract | slides]

Recent and Upcoming talks

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, MD.
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