Person: Rubio Cuéllar, Rubén Rafael
Loading...
First Name
Rubén Rafael
Last Name
Rubio Cuéllar
Affiliation
Universidad Complutense de Madrid
Faculty / Institute
Informática
Department
Sistemas Informáticos y Computación
Area
Lenguajes y Sistemas Informáticos
Identifiers
7 results
Search Results
Now showing 1 - 7 of 7
- Project number: 18
Item Juez automático para el aprendizaje de bases de datos(2021) Martín Martín, Enrique; Burgoa Muñoz, Iker; Rubio Cuéllar, Rubén Rafael; Cerro Cañizares, Pablo; Correas Fernández, Jesús; Montenegro Montes, Manuel; Riesco Rodríguez, AdriánProponemos desarrollar un juez automático para el aprendizaje de bases de datos. Este sistema web permitirá a los estudiantes practicar con diferentes ejercicios de bases de datos desde casa y recibir retroalimentación inmediata sobre los fallos. Item Improving database learning with an automatic judge(2022) Martín Martín, Enrique; Montenegro Montes, Manuel; Riesco Rodríguez, Adrián; Rubio Cuéllar, Rubén RafaelDatabases are a key subject in several technical degrees. Because they have a strong practical nature, students require a large number of problems to master them. However, these problems are useful only if accurate and timely feedback is provided. In this paper, we present the learning improvements obtained by using LearnSQL, an automatic judge that has been designed to complement face-to-face lectures. We have measured the impact of this judge during the 2021/22 academic year and report promising results both in student engagement and final grades.Item Theorem Proving for Maude Specifications Using Lean(2022) Rubio Cuéllar, Rubén Rafael; Riesco Rodríguez, Adrián; Riesco Rodríguez, Adrián; Zhang, MinMaude is a specification language based on rewriting logic whose programs can be executed, model checked, and analyzed with other techniques, but not easily theorem proved. On the other hand, Lean is a modern proof assistant based on the calculus of inductive constructions with a wide library of reusable proofs and definitions. This paper presents a translation from the first formalism to the second, and a tool that derives a Lean program from a Maude module in a predictable way. Hence, theorems can be proved in Lean about Maude specifications.Item Maude2Lean: Theorem proving for Maude specifications using Lean(Journal of Logical and Algebraic Methods in Programming, 2025) Rubio Cuéllar, Rubén Rafael; Riesco Rodríguez, AdriánMaude is a specification language based on rewriting logic whose programs can be executed, model checked, and analyzed with other automated techniques, but not easily theorem proved. On the other hand, Lean is a modern proof assistant based on the calculus of inductive constructions with a wide library of reusable proofs and definitions. This paper presents a translation from the first formalism to the second, and the maude2lean tool that predictably derives a Lean program from a Maude module. Hence, theorems can be proved in Lean about Maude specifications.- Project number: 387
Item Evaluación del impacto sobre el aprendizaje de bases de datos del juez automático LearnSQL(2022) Martín Martín, Enrique; Correas Fernández, Jesús; Garmendia Salvador, Luis; Montenegro Montes, Manuel; Riesco Rodríguez, Adrián; Rubio Cuéllar, Rubén Rafael; Sáenz Pérez, FernandoUtilizamos el juez automático "LearnSQL" en la docencia de varios grupos de la asignatura "Bases de Datos" y medimos de manera rigurosa y extensiva el impacto que este tiene sobre el aprendizaje de los estudiantes. - Project number: 84
Item Aplicación web progresiva para la realización de cuestionarios offline: difusión e integración con Moodle(2023) Montenegro Montes, Manuel; Martín Martín, Enrique; Riesco Rodríguez, Adrián; Rubio Cuéllar, Rubén Rafael; Verdejo López, José Alberto; El Fakhri Ouajih, Zakaria; Martínez Gamero, Pedro Item Verification of the ROS NavFn planner using executable specification languages(Journal of Logical and Algebraic Methods in Programming, 2023) Martin-Martin, Enrique; Montenegro Montes, Manuel; Riesco Rodríguez, Adrián; Rodríguez Hortalá, Juan; Rubio Cuéllar, Rubén RafaelThe Robot Operating System (ROS) is a framework for building robust software for complex robot systems in several domains. The Navigation Stack stands out among the different libraries available in ROS, providing a set of components that can be reused to build robots with autonomous navigation capabilities. This library is a critical component, as navigation failures could have catastrophic consequences for applications like self-driving cars where safety is crucial. Here we devise a general methodology for verifying this kind of complex systems by specifying them in different executable specification languages with verification support and validating the equivalence between the specifications and the original system using differential testing techniques. The complex system can then be indirectly analyzed using the verification tools of the specification languages like model checking, semi-automated functional verification based on Hoare logic, and other formal techniques. In this paper we apply this verification methodology to the NavFn planner, which is the main planner component of the Navigation Stack of ROS, using Maude and Dafny as specification languages. We have formally proved several desirable properties of this planner algorithm like the absence of obstacles in the planned path. Moreover, we have found counterexamples for other concerns like the optimality of the path cost.