Professor Rueda’s research interests are mainly in the area of the use of formalisms and tools for modeling and verifying interactive systems. There are two main formalisms he privileges in his research, one derived from the “correct by construction” software development paradigm (essentially based on predicate calculus specification of system properties), and the other coming from concurrency theory, namely the formal calculi of concurrent processes.
In the first, he is interested in finding ways to make the paradigm accessible to the mainstream software development practitioners by offering provably correct translations between a formal system model in the correct by construction paradigm and a fully specified computer program in some mainstream language.
In the second, the goal is being able to model and verify systems in very complex interaction contexts. Among the variety of calculi proposed for this, he is most interested in those capable of performing computation under partial information and having some formal logic equivalence, such as the so-called concurrent constraints calculi (CCP). The application of this theoretical work I consider mostly is in the field of multimedia interaction, for example, the coordination of human and computers in musical performance, such as in a computers involved in music improvisation scenarios.
His third line of research is the use of languages and techniques derived from constraint programming for solving combinatorial problems. In particular, in approaching the declarative modeling convenience of constraint programming to the solution of real-world engineering problems.