Contact

me
email
address
Department of Computing
180 Queen's Gate
Imperial College London
London SW7 2AZ
find me
Room 433, Huxley Building

I am a Research Assistant working with Philippa Gardner at Imperial College London. I am interested in program verification, concurrency, automatic tools for verification, and compositional analysis.

Before that, I was a Research Assistant in the Programming Principles, Logic and Verification group of UCL in London.

I did my PhD at LSV in Cachan (France) under the supervision of Étienne Lozes.

Software

Heap-Hop 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.

llStar verifies programs written in LLVM's Intermediate Representeation language using separation logic. Its theory is fully customisable, so that it can be used to quickly implement new analyses and test them on real programs.

Try llStar on the Web!

Publications

In progress

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]

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 with Proceedings

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]

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]

Thesis

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

Students

Master student research internships supervised:

Committees