Jules Villard

Conferences and Workshops with Proceedings

LRVBDO22

Finding Real Bugs in Big Programs with Incorrectness Logic. L. Le, A. Raad, J. Villard, J. Berdine, D. Dreyer, and P. O'Hearn. OOPSLA'22, ACM, 2022. SIGPLAN Distinguished Paper Award [pdf | bib | abstract]

RBDDOV20

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]

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]