Proving copyless message passing J Villard, É Lozes, C Calcagno Programming Languages and Systems, 194-209, 2009 | 82 | 2009 |

The ramifications of sharing in data structures A Hobor, J Villard Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2013 | 71 | 2013 |

Parametric completeness for separation theories J Brotherston, J Villard ACM SIGPLAN Notices 49 (1), 453-464, 2014 | 55 | 2014 |

Tracking Heaps that Hop with Heap-Hop J Villard, É Lozes, C Calcagno Tools and Algorithms for the Construction and Analysis of Systems, 275-279, 2010 | 41 | 2010 |

Heaps and Hops J Villard PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, 2011 | 37 | 2011 |

Colosl: Concurrent local subjective logic A Raad, J Villard, P Gardner European Symposium on Programming Languages and Systems, 710-735, 2015 | 34 | 2015 |

Developments in Concurrent Kleene Algebra T Hoare, S van Staden, B Möller, G Struth, J Villard, H Zhu, P O'Hearn Relational and Algebraic Methods in Computer Science 8428, 1-18, 2014 | 21 | 2014 |

Sub-classical Boolean bunched logics and the meaning of par J Brotherston, J Villard 24th EACSL Annual Conference on Computer Science Logic (CSL 2015), 2015 | 15 | 2015 |

A spatial equational logic for the applied pi-calculus É Lozes, J Villard Distributed Computing 23 (1), 61-83, 2010 | 15* | 2010 |

On the relation between concurrent separation logic and concurrent Kleene algebra PW O'Hearn, RL Petersen, J Villard, A Hussain Journal of Logical and Algebraic Methods in Programming 84 (3), 285-302, 2015 | 14 | 2015 |

Reliable Contracts for Unreliable Half-Duplex Communications⋆ É Lozes, J Villard Web Services and Formal Methods 7176, 2-16, 2011 | 13 | 2011 |

Verifying concurrent graph algorithms A Raad, A Hobor, J Villard, P Gardner Asian Symposium on Programming Languages and Systems, 314-334, 2016 | 11 | 2016 |

Local reasoning about the presence of bugs: Incorrectness separation logic A Raad, J Berdine, HH Dang, D Dreyer, P O’Hearn, J Villard International Conference on Computer Aided Verification, 225-252, 2020 | 6 | 2020 |

Multiple congruence relations, first-order theories on terms, and the frames of the applied pi-calculus F Jacquemard, E Lozes, R Treinen, J Villard Joint Workshop on Theory of Security and Applications, 166-185, 2011 | 4* | 2011 |

Shared contract-obedient channels É Lozes, J Villard Science of Computer Programming 100, 28-60, 2015 | 3 | 2015 |

Sharing contract-obedient endpoints É Lozes, J Villard Proceedings of Interaction and Concurrency Experience (ICE'12) 104, 17-31, 2012 | 3 | 2012 |

Bi-intuitionistic boolean bunched logic J Brotherston, J Villard RN 14, 06, 2014 | 2 | 2014 |

Here be wyverns! Verifying LLVM bitcode with llStar J Villard | 2* | |

The Ramifications of Sharing in Data Structures J Villard | | |

CoLoSL: Concurrent Local Subjective Logic PA Gardner, A Raad, J Villard Springer, 0 | | |