Note

This repository contains a technical report on CBMC (C Bounded Model Checker), developed as part of the Software Engineering II course of the Computer Science degree at FAMAF – Universidad Nacional de Córdoba.

All content is in Spanish, as it was written for academic use and submission.

Informe sobre CBMC (Bounded Model Checker para programas C y C++)

El presente repositorio contiene toda la información correspondiente el informe realizado sobre CBMC para la materia Ingeniería del Software II correspondiente a 5to año de la Licenciatura en Ciencias de la Computación de FAMAF durante el año 2025.

Miembros del equipo

El equipo encargado del presente informe está conformado por:

• Bratti, Juan.
• Herrador, Emanuel.
• Scavuzzo, Ignacio.

Contenidos

Aquí se podrá encontrar el informe correspondiente a CBMC con explicaciones respecto a su origen, objetivo, aplicaciones y funcionamiento (tanto técnico como por parte del usuario), más un caso de uso creado por nosotros que consta de solucionar un challenge de criptografía de un CTF (XtraORdinary del CTF picoMini). Más información respecto a la herramienta la podrá encontrar en el informe, y sobre el caso de uso aquí. Además, se incluye la presentación correspondiente al trabajo.