Equivalences of executions play a central role in testing and verification of concurrent programs. Mazurkiewicz traces have so-far been the favourite equivalence of executions used in a variety of verification and testing techniques, including stateless model checking of concurrent programs and predictive runtime analysis. In model checking, they have helped define infinite-space subclasses for which the reachability problem is decidable. In the generally undecidable software model checking problem, they have been used to search for simpler proofs where the verification conditions fall under decidable theories handled by SMT solvers.
On the other hand, in testing approaches such as runtime verification, the notion of equivalences allows to do more exhaustive testing. Finally, they have been used classically to power a large array of partial order reduction techniques for pruning search in a variety of model checking problems.

A recent trend in stateless model checking techniques for concurrent programs has been to incorporate equivalences classes that are provably coarser than Mazurkiewicz equivalences. In the wider scope of the aforementioned applications, certain properties of Mazurkiewicz traces are essential for the effectiveness of the algorithms behind these techniques. One vital property is that the minimal set of the representatives of the equivalence classes is regular. In this paper, we investigate relaxations of the notion of Mazurkiewicz equivalence classes. Specifically, we consider a semantic notion, generalizing the Sasha-Snir equivalence, that preserves the reads-from mapping of each read event across different members of the equivalences. We show how the regularity of representatives is quickly lost in this case and propose a careful restriction that helps regain regularity. We then show that this restriction can be useful in the context of predictive monitoring, as in data race prediction.

Formal Methods and Logic and their applications to Programming Languages and Software Engineering. I like to explore and re-investigate the foundations of traditional solutions for intractable problems arising in testing, verification and synthesis of software systems. The current focus of my research is on developing techniques for detecting concurrency bugs, and on developing techniques for decidable program verification and synthesis.