Person:
Segura Díaz, Clara María

First Name

Clara María

Last Name

Segura Díaz

Affiliation

Universidad Complutense de Madrid

Faculty / Institute

Informática

Department

Sistemas Informáticos y Computación

Area

Lenguajes y Sistemas Informáticos

Identifiers

Full item page

Search Results

Now showing 1 - 8 of 8

Extending Liquid Types to Arrays
(ACM, 2020-01-21) Montenegro Montes, Manuel; Nieva Soto, Susana; Peña Marí, Ricardo; Segura Díaz, Clara María
A liquid type is an ordinary Hindley-Milner type annotated with a logical predicate that states the properties satisfied by the elements of that type. Liquid types are a powerful tool for program verification, since programmers can use them to specify pre- and postconditions of their programs, while the predicates of intermediate variables and auxiliary functions are inferred automatically. Type inference is feasible in this context, since the logical predicates within liquid types are constrained to a quantifier-free logic in order to maintain decidability. In this paper we extend liquid types by allowing them to contain quantified properties on arrays, so that they can be used to infer invariants on array-related programs (for example, implementations of sorting algorithms). Although quantified logic is, in general, undecidable, we restrict properties on arrays to a decidable subset introduced by Bradley et al. We describe in detail the extended type system, the verification condition generator, and the iterative weakening algorithm for inferring invariants. After proving the correctness and completeness of these two algorithms, we apply them to find invariants on a set of algorithms involving array manipulations.
Análisis de programas en lenguajes funcionales paralelos
(Universidad Complutense de Madrid, Servicio de Publicaciones, 2004) Segura Díaz, Clara María; Peña Marí, Ricardo
Las tecnicas de análisis de programas se han demostrado útiles en todo tipo de lenguajes de programación para determinar de forma estática aproximaciones a las propiedades dinámicas de los programas. Sus aplicaciones incluyen la optimización y transformación de los programas, así como la demostración o verificación de propiedades de los mismos. El desarrollo y la aplicación de las tecnicas de análisis a los lenguajes funcionales ha sido muy amplio en estas dos ultimas décadas. Esta tesis se enmarca en el área de análisis estáticos de programas aplicados a los lenguajes funcionales paralelos. La programación funcional paralela es un área de investigación intensa en la actualidad que proporciona nuevos problemas en el campo de los análisis de programas, pero es aun un área poco trabajada donde queda mucho por hacer. En esta tesis se definen tres análisis aplicados al lenguaje funcional paralelo Edén: -Análisis de conexión directa: tiene como objetivo optimizar los programas Edén reduciendo sobrecargas debidas a la creación de procesos y a la comunicación entre ellos. -Análisis de no determinismo: pretende delimitar aquellas partes de los programas Edén donde es posible mantener el razonamiento ecuacional característico de los lenguajes funcionales. -Análisis de terminación y productividad: es un sistema de demostración de propiedades de terminación y productividad de los programas Edén que garantiza la ausencia de bloqueos en ellos. Para definir estos análisis se han utilizado algunas de las tecnicas usadas en el análisis de los lenguajes funcionales: la interpretación abstracta y los sistemas de tipos anotados
Veriﬁcation of mutable linear data structures and iterator-based algorithms in Dafny.
(Elsevier, 2023-08) Blázquez Saborido, Jorge; Montenegro Montes, Manuel; Segura Díaz, Clara María
We address the veriﬁcation of mutable, heap-allocated abstract data types (ADTs) in Dafny, and their traversal via iterators. For this purpose, we devise a veriﬁcation methodology that makes it possible to implement ADTs based on already existing ones, while maintaining proper encapsulation. Then, we apply this methodology to the speciﬁcation and implementation of linear collections such as stacks, queues, deques, and lists with iterators. The approach introduced in this paper allows one to progressively reﬁne some aspects of the speciﬁcation such as iterator invalidation, so that clients of the library can reason about how structural changes to a list affect existing iterators. Finally, we extend our methodology to the veriﬁcation of client code (i.e., code that makes use of the implemented ADTs) and identify the boilerplate conditions common to all methods that receive and manipulate ADTs.
Una herramienta para el estudio de estructuras de datos y algoritmos
(Editorial Complutense, 2007) Segura Díaz, Clara María; Pita Andreu, María Isabel; Fernández-Valmayor Crespo, Alfredo; Fernández-Pampillón Cesteros, Ana María; Merino Granizo, Jorge
Presentamos una herramienta informática para la visualización interactiva de estructuras de datos y esquemas algorítmicos. Durante el presente curso hemos evaluado la parte de la herramienta dedicada a las estructuras de datos. Las distintas partes de la herramienta pretenden transmitir a los alumnos la separación entre especificación e implementación de una estructura de datos, así como proporcionar ejemplos de utilización de dichas estructuras. La evaluación de la herramienta se ha llevado a cabo mediante tests gestionados desde el Campus Virtual de la Universidad Complutense de Madrid. Presentamos los resultados obtenidos a partir de una experiencia en la que se proporcionó acceso libre a la herramienta para todos los alumnos.
La gamificación en la educación universitaria: aplicación a asignaturas de programación
(2019-10-23) Gómez Martín, Marco Antonio; Segura Díaz, Clara María; Ortega Mallén, Yolanda; Verdejo López, José Alberto; Martí Oliet, Narciso; Gómez Martín, Pedro Pablo; Carballa Corredoira, Boris; García Baameiro, Daniel; Martín Sánchez, Oscar; Domenech Arellano, Jesús Javier; Costero Valero, Luis María; Jacynycz García, Viktor Shamel
Informe sobre la experiencia de aplicar técnicas de gamificación en la asignatura “Estructura de Datos y Algoritmos”, obligatoria de 2º curso en los grados impartidos en la Facultad de Informática de la UCM.
Añadiendo mecanismos de ayuda en un juez on-line automático para soporte a mentorías académicas
(2019-01-14) Gómez Martín, Marco Antonio; Gómez Martín, Pedro Pablo; Verdejo López, José Alberto; Pita Andreu, María Isabel; Segura Díaz, Clara María; Gómez Albarrán, Mª De Las Mercedes; Hernández Bécares, Jénnifer; Domenech Arellano, Jesús Javier; Costero Valero, Luís María; Doménech Arellano, Pedro Pablo
Todos los jueces en línea, incluído en sus inicios ¡Acepta el reto! (https://www.aceptaelreto.com) desarrollado por profesores de la UCM, adolecen de un problema de realimentación al usuario: cuando el visitante hace un envío incorrecto el sistema no es capaz de dar información específica del error. El documento es la memoria final de un Proyecto de Innovación y Mejora de la Calidad Docente (PIMCD) de 2017/2018 en el que se puso en marcha un sistema de pistas en el juez.
Validación en línea de aspectos formales y corrección asistida de ejercicios en asignaturas con evaluación continua
(2017) Montenegro Montes, Manuel; Segura Díaz, Clara María; Rosa Velardo, Fernando; Saavedra López, Santiago; Hernando Serrano, Laura; Rossetto Bermejo, Daniel
Hacia una mejora en la corrección automática parcial de actividades/prácticas de los estudiantes
García-Magariño García, Iván; Arroyo Gallardo, Javier; Bravo Agapito, Javier; Galvez Gutiérrez, Daniel; Gómez Sanz, Jorge J.; González de Miguel, Ana M.; Hassan Collado, Samer; Herrero Desvoyes, Hugo; Lacuesta Gilaberte, Raquel; López Fernández, Marta; Nevzorov Oussenko, Aitor; Palero San Román, Inés; Pavón Mestras, Juan; Pita Andreu, Isabel; San Martín Doblado, Laura; Sánchez Hernández, Jaime; Segura Díaz, Clara María; Trillo Carreras, Juan; Vukotic de la Puente, Lucas; Yllana Santiago, Daniel
The evaluation of student learning is usually done through activities and exercises where students apply their acquired knowledge in the resolution of problems close to real life, but delimited by the teacher. In these activities and exercises the teacher can evaluate conceptual knowledge and procedural knowledge. In the application area of this project, it is common that in the programming exercises and activities (practices) both types of knowledge are evaluated, since, on the one hand, the application of algorithms (procedural knowledge) and what programming elements and structures are being used (conceptual knowledge) are evaluated. The teacher has the complex task of evaluating this knowledge by making an individualized correction of each practice. While individualized correction of each practice is usually unbeatable in terms of the quality of the correction, on the other hand, automating the evaluation of procedural knowledge provides certain advantages. Routine parts can be evaluated automatically and thus save valuable time for the teacher's correction of other aspects. One of the advantages of automatic correction is that it is immediately available to the students and allows guiding them in essential aspects. In this teaching innovation project, a new online judge called UnitJudge has been developed. This new judge allows automatically evaluating programming practices in a consistent way even when these are long. In the ability to evaluate long practices, it outperforms other existing judges, such as DomJudge, which are more appropriate for short exercises since they are based on global inputs and outputs without allowing students to know which part of the code is failing. The newly developed judge allows to test the different parts based on unit tests. It is implemented for both C++ and Java practices. The new UnitJudge was used in several groups of the Programming Fundamentals subject. Taking into account the averages of 29 students' responses to the validated USE (Usefulness, Satisfaction and Ease of Use) scale, it was concluded that UnitJudge was easy to learn to use (mean of 5.99 out of 7), useful for the students (mean of 5.62 out of 7), and satisfactory for them (mean of 5.12 out of 7). The results of this teaching innovation project have been presented in two papers at the international conference "The 10th International and the 16th National Conference on e-Learning and e-Teaching" (ICELET 2023), respectively about (1) the presentation of UnitJudge and the experiment with the students of Fundamentals of Programming, and (2) intrusion detection from the viewpoint of cybersecurity in online judges exemplified with UnitJudge.