He earned a B.Sc. and a M.Sc. degree in Informatics from the Universidad de los Andes (Bogotá, Colombia), and a M.Sc. degree in Mathematics and a Ph.D. degree in Computer Science from the University of Illinois (Urbana, USA). He is currently working on developing symbolic techniques and tools for reachability analysis in rewriting logic. Prof. Rocha has been a regular visitor at NIA where he has been involved, mainly, in efforts towards the formal semantics and verification of NASA’s PLEXIL language. Details and more information about his research can be found at his personal webpage: http://camilorocha.info.