Skip to main content
  • Expression of Interest

    Reversible debugging and verification of message-passing concurrent and distributed systems

    Germán Vidal (https://gvidal.webs.upv.es/) is currently Professor at the Valencian Research Institute for Artificial Intelligence (vrAIn, https://vrain.upv.es/). He's worked on different topics, ranging from test-case generation to program analysis and verification in the context of functional, logic, and concurrent programs. Recently, he's considered the actor model (and the programming language Erlang in particular) and has introduced a causal-consistent reversible semantics that can be used for replay/reversible debugging of message-passing concurrent processes. While replay debugging is essential for the reproducibility of bugs, reversibility can be very useful not only to locate bugs but also to improve accountability. A debugging tool for Erlang programs following these ideas is publicly available: CauDEr (https://github.com/mistupv/cauder). Moreover, a novel technique for stateless model checking of concurrent processes has been introduced, where dynamic partial order reduction is not needed (check the attached paper). Both replay/reversible debugging and model-checking techniques can be very useful to ensure the safety of message-passing concurrent and distributed systems.

    {Empty}