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.




  • "Model Checker Execution Reports" (New Ideas paper), R. Castaño, Victor A. Braberman, Diego Garbervetsky, Sebastian Uchitel, International Conference on Automated Software Engineering (ASE) 2017. In print. Conference program
  • "On verifying resource contracts using Code Contracts", R. Casta\~no, J. P. Galeotti, D. Garbervetsky, J. Tapicer, E. Zoppi, Latin American Workshop on Formal Methods (LAFM) 2013. pdf
  • "A finite state intersection approach to propositional satisfiability", J.M. Castaño, R. Castaño, Theoretical Computer Science (2012). pdf
  • "Variable and Clause Ordering in an FSA Approach to Propositional Satisfiability”, J. M. Castaño, R. Castaño, 16th International Conference on Implementation and Application of Automata (CIAA­2011). pdf
  • “Propositional satisfiability (SAT) as a language problem“, J. M. Castaño, R. Castaño, Workshop Aspectos Teóricos de Ciencias de la Computación, XVII Congreso Argentino de Ciencias de la Computación, 2011. pdf


  • "Understanding partial verification attempts", R. Castaño, 3rd International Conference on Software Engineering (ICSE 2017) PhD and Young Researchers Warm Up Symposium, September 9, 2016
  • “Backbones Generator (Bbgen2)” H. Arregui, R. Castaño, L. Lauría, R. Garabato, E. Fernández, M. Villarreal, D. Gutson. 2do Congreso Argentino de Bioinformática, May 11­-13, 2011
  • “Generation of a complete repository of protein backbones”, R. Castaño, L. Lauría, G. Biset, R. Garabato, D. Gutson, M. Villarreal. 1er Congreso Argentino de Bioinformática, May 12­-14, 2010