Rodrigo Castaño

Rodrigo Castaño

rcastano (en) dc . uba . ar




Rodrigo Castaño

I am a Computer Science PhD student at Universidad de Buenos Aires since 2013 with a CONICET scholarship.

My PhD topic is centered around improving software model checkers when they produce inconclusive results, that is, when they cannot find a bug but have not finished exploring the whole state space.

Besides my academic work, I have gained valuable industry experience through several internships, both in leading companies, like Google, Facebook and Microsoft and at outstanding research institutes, like INRIA Nancy.

Aside from that, I enjoy classical music and play the violin on a regular basis. I used to play tennis fairly well and I still play every once in a while. I am also a very impatient, and not quite good, fly fisherman, but the landscapes of Patagonia can soothe the beasts.

My Curriculum Vitae as of September 25, 2017. pdf.

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
  • "A finite state intersection approach to propositional satisfiability", J.M. Castaño, R. Castaño, Theoretical Computer Science (2012), In print. 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


  • "On verifying resource contracts using Code Contracts", Rodrigo Castaño, Juan Pablo Galeotti, Diego Garbervetsky, Jonathan Tapicer, Edgardo Zoppi , "On Verifying Resource Contracts using Code Contracts" , Proceedings First Latin American Workshop on Formal Methods, page 1-15 - 2014 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


Other places where you can find me:


Videos of Buenos Aires Student's Orchestra, featuring me amongst the second violins: