Los mini-cursos serán realizados
en el campus de la Universidad Continental (Av. San Carlos 1980). Las fechas y horarios de los mini-cursos pueden ser consultadas en la pagina de Programacion del CSPC.
MC1 - Proyecto de Circuitos Digitales
(
Milton Romero) La síntesis de circuitos digitales combinatórios y secuenciales está basada en el álgebra de Bool. Este minicurso ilustra la metodologia de proyecto utilizando mapas de Karnaugh y lenguaje de descripción de hardware (VHDL com la herramienta Quartus versión estudiante) para la síntesis de circuitos digitales. Se utiliza un caso de estúdio para ilustrar la aplicación de la metodologia en casos prácticos para el proyecto de circuitos secuenciales (con memória) baseado em máquinas a estados finitos.
MC2 - Multi-Core Programming
(
Marco A. Alvarez) Computadores/procesadores con múltiples núcleos ya son comunes en los días de hoy, así como también están cambiando la forma de programar. En este mini-curso se expondrán aspectos fundamentales para el desarrollo de programas que puedan ser ejecutados en paralelo o concurrentemente. Se revisarán las técnicas necesarias para hacer un uso efectivo de máquinas con múltiples núcleos. Los alumnos tendrán la oportunidad de correr programas concurrentes utilizando los lenguajes de programación Java y C, además de ver diversos ejemplos con lenguajes como python y perl.
MC3 - Estructuras
de datos y algoritmos con programación genérica
(
Alex Cuadros) En este mini curso se presentaran y discutirán factores relacionados a la creación de estructuras de datos y algoritmos haciendo énfasis en aspectos de dinamismo, flexibilidad y rapidez. Se discutirán estructuras de datos desde simples hasta complejas. Se explicara, para este fin, conceptos de programación tales como: templates, traits, function-objects, iterators, circulators, punteros, threads; y se discutirá sobre las implicancias del uso de cada uno de estos conceptos en la implementación de estructuras de datos y algoritmos.
MC4 - Model Checking (Verificación formal de sistemas)
(
Pablo Barcelo) La verificacion de sistemas formales, que comunmente describen comportamientos del software o hardware, es especialmente relevante en ciertas aplicaciones criticas tales como sistemas complejos, medicina o disenho de procesadores, donde una falla en el comportamiento del sistema puede producir perdidas millonarias o costar vidas humanas. El "model checking" es la tecnica mas ampliamente aceptada para la verificacion automatica de sistemas formales. Su impacto ha sido tal que incluso sus creadores - Clarke, Emerson y Sifakis - recibieron por esta contribucion el "Turing award" en el anho 2007 (el equivalente al "Nobel" de Computacion).
En terminos abstractos el "model checking" se refiere al siguiente problema: Dado un modelo del sistema y una especificacion del comportamiento deseado, verificar automaticamente si el modelo satisface la especificacion. Para poder realizar este proceso algoritmicamente es necesario que tanto el modelo como la especificacion sean definidos en un lenguaje matematico preciso. Por ejemplo, la forma mas comun de especificar los modelos es usando "sistemas de transicion", i.e. grafos dirigidos en que cada nodo es etiquetado usando simbolos de un alfabeto. Por otro lado, la forma mas difundida de definir las especificaciones que se desea que los sistemas cumplan es mediante una formula en alguna "logica temporal".
En el curso estudiaremos lo siguiente: (1) Introduccion al model checking. (2) Especificacion de sistemas formales mediante sistemas de transicion. (3) Las logicas temporales mas utilizadas en verificacion: LTL, CTL, CTL*. (4) Algoritmos de verificacion eficientes para cada una de estos lenguajes.
