Note
This repository contains theoretical notes, practical exercises, and a final project developed for the Software Engineering II course of the Computer Science degree at FAMAF – Universidad Nacional de Córdoba.
All materials are in Spanish, as they were created for academic use and course submission.
El presente repositorio contiene todo el material correspondiente a la cursada de la materia de Ingeniería del Software II de 5to año de la Licenciatura en Ciencias de la Computación de FAMAF durante el año 2025.
Los temas que trata la materia se pueden ver en el programa de la misma. Respecto al material, este está basado en los siguientes libros:
- J. Magee y J. Kramer. Concurrency: State Models & Java Programs, 2nd edition. Wiley 2006.
- C. Baier y J.-P. Katoen. Principles of Model Checking. MIT Press, 2008.
- D. Jackson. Software Abstractions: Logic, Language, and Analysis (Revised Edition). MIT Press, 2016.
- D. Kroening y O. Strichman. Decision Procedures: An Algorithmic Point of View. 2nd. edition. Springer, 2016.
- A. Biere, M. Heule, H. van Maaren, y T. Walsh (eds.). Handbook of Satisfiability. 2nd edition. IOS press, 2021.
- M. Müller-Olm, D. Schmidt, B. Steffen. Model Checking: A Tutorial Introduction. En A. Cortesi, G. Filé (Eds.), Procs. Of SAS'99, LNCS 1694, pp. 330-354. Springer 1999.
El equipo docente está únicamente conformado por Pedro Ruben D'Argenio.
| Temas | Descripción | Filminas | Libro/Apunte |
|---|---|---|---|
| Introducción | Burocracia A qué apunta la materia |
Magee & Kramer (1) | |
| Programación concurrente | Repaso Transición de estados Semántica de FSP |
Magee & Kramer (2, 3) | |
| Sincronización de procesos concurrentes | Interferencia y exclusión mutua Monitores, semáforos y buffers Simulación y bisimulación Pasaje de mensajes |
Magee & Jramer (4, 5, 10) Notas de clase |
|
| Propiedades de los sistemas reactivos y su análisis | Lenguajes Safety y liveness Vista en FSP |
Magee & Kramer (6, 7) Alpern & Schneider (21:182-185) Baier & Katoen (3, 4) |
|
| Lógica temporal lineal | LTL Safety, liveness y fairness |
Baier & Katoen (4, 5) | |
| Model Checking | Autómatas de Büchi SPIN y SMV |
Müller-Olm (1, 2, 4.2, 4.4) | |
| Especificación de sistemas | Especificación SAT solving (idea) Álgebra de relaciones |
||
| El lenguaje de especificación Alloy | Signaturas Predicados Hechos, aserciones y predicados Cambios de estado y trazas Elección de cotas y cuantificadores universales no acotados |
D. Jackson 2006 (1, 2, 3, 4) Ejemplos |
|
| Algoritmos para verificar satisfactibilidad en lógica proposicional | Tablas de verdad Método de tableaux Tablas de verdad reconsideradas Transformación de Tseitin (CNF equisatisfactible) Resolución Cláusulas de Horn DPLL |
A.R. Bradley & Z. Manna 2007 (The Calculus of Computation) |
La información específica sobre el proyecto con sus pautas se puede encontrar en esta presentación. El proyecto consistió en investigar y realizar un informe acerca de una herramienta de Model Checking elegida al azar (en base a nuestras preferencias) por el profesor. En nuestro caso, se trató sobre CBMC.
Nuestro proyecto se enfoca en CBMC (C Bounded Model Checking), su origen, objetivo, usos, interfaz, estructura, comparaciones, casos de estudio y un caso de uso hecho por nosotros usando esta herramienta de verificación para romper un cifrado personalizado (resolver un problema de un CTF) para demostrar su potencial y versatilidad. El informe y la presentación se pueden encontrar en este repositorio público.