Research interests
During my PhD I have been working on the problem of leveraging partial model checker explorations. When a model checker runs out of resources or cannot continue due to a limitation of its underlying logic, for example, the result is inconclusive. The property has not been proven but a counterexample has not been produced either. However, could we produce a more useful output about what has, in fact, been explored?
In some settings, it can be useful to produce a coverage metric that can be used as part of a dependability case and directly compared to that of a test suite. In other cases users might want to observe what has been explored, essentially a report of the work performed. Such a report could be used to exclude the already explored state space from subsequent runs. A verification expert might want to be able to better understand whether the tool was making any progress and possibly get some insights from that. These and other use cases require entirely different approaches and we continue to explore these challenges.
As an undergraduate student I worked on different translations of the propositional satisfiability problem (SAT) to equivalent formal languages' problems. We have seen some very interesting results in terms of performance using Finite State Automata and grammar representations of the problem.
I worked as a C++ developer with a research group working on bioinformatics. I would be interested on further working on these topics.