César Rodríguez
Dr. César Rodríguez

Senior Scientist at Diffblue.
Associate Professor at Université Paris 13, Sorbonne Paris Cité.

Current address:
Diffblue, King Charles House, Park End Street,
Oxford OX11HJ, United Kingdom
Find me on:


NEWS: In May 2017 I have joined Diffblue, a startup focusing on automated analysis of sequential and multithreaded software.

I am also an associate professor (maître de conférences), currently on long-term unpaid leave (détachement) at the University Paris 13, Sorbonne Paris Cité, working in the Specification and Verification team within LIPN.

Prior to my assignment, in September 2014, I was a research assistant at the Compuer Science Department of the University of Oxford, working at Daniel Kroening's team. In December 2013, I received my PhD from the École Normale Supérieure de Cachan (ENS Cachan), where I was a doctoral candidate at the Laboratoire Spécification et Vérification (LSV) under superivision of Stefan Schwoon. See my old webpage.


I am interested in formal methods, i.e., techniques enabling engineers to formally specify and rigorously verify computer systems. In particular, I focus on techniques for automated verification of concurrent software, including:

I have also worked in diagnosis and process discovery. See my publications at my DBLP and Google Scholar profiles for more information.


The central goal of my research is providing tools and techniques for software analysis that have a direct impact on the way people write software and reason about it.

My motivation for, and approach to formal methods stems from my previous life as a embedded developer, mainly within the Nanosat 1B satellite project, during my years with the SRG, University of Alcalá. There, I learnt about the great need for more rigorous and automated approaches to software development and the lack of good tool support for many aspects of the development process. For me, the main value (if not the only) of a technique for formal verification is simplifying the life of an engineer, and that is how I perceive the success of these techniques.


At Diffblue my team and I develop software analysis techniques for multithreaded and distributed programs. Our techniques can be applied to automate a broad range of tasks in software development, such as:

  • Test generation.
  • Bug finding.
  • Data-race and deadlock detection.
  • Concurrency flaw detection.
  • Detection of security vulnerabilities and exploit generation.
  • In general, verification of properties of the program that are related with concurrency.

We are in the process of shaping a new product based on the techniques we develop. We are looking for ways to collaborate with industrial partners to understand their needs in this scope, and how we can help. We are interested in hearing stories about concurrency, difficulties, and needs on testing concurrent code, discovering flaws etc. So feel free to contact me if you think you have something to share in this context!


2016 -- 2017:

2015 -- 2016:

2014 -- 2015: