Many scripting languages are object-based and have weak, dynamic type systems to simplify the development of short programs. As larger programs are built with scripting languages, static type systems and analyses become important tools for detecting programming errors.
We define such a type system based on an imperative object-based calculus that models essential features of the JavaScript language, as an example of a typical and widely used scripting language. The calculus supports objects as property tables, type change during object initialization, and precise support for JavaScript's prototype mechanism.
Our work transfers the idea of recency abstraction from abstract interpretation to a type system. The corresponding feature in our system, the precise object pointer, enables strong, type changing updates on object types during a generalized initialization phase. The same precise object pointers enable an accurate treatment of the prototype mechanism. Unlike linear types, precise object pointers can be nested and mixed arbitrarily with imprecise object pointers in the description of a data structure.
We have proved type soundness of the system and we have defined and implemented a typing algorithm.
La programación a nivel de sistema es una tarea difícil. Por ejemplo, aprender conceptos de sistemas operativos programando en áreas como manejo de interrupciones o segmentación/paginación de memoria en un host nativo es una tarea riesgosa y que requiere mucho tiempo de aprendizaje. Una alternativa es la de programar dentro de un kernel preexistente que ejecute como guest dentro de una máquina virtual. Esto no hace la tarea más fácil: se reduce el riesgo de dañar el host nativo, pero el programador se encuentra desarrollando dentro de todo un kernel que ya tiene sus propios mecanismos de segmentación/paginado/interrupciones, etc, mecanismos que se deben entender en detalle para poder hacer modificaciones exitosas. ¡Pero el programador los está usando precisamente para aprender!
Por otro lado, la infraestructura de virtualización del kernel de Linux (KVM) permite crear muy fácilmente máquinas virtuales que semejen una plataforma "nativa" justo en el estado en que se encuentra luego de encenderse. Esto permite escribir mini-kernels para que ejecuten dentro de esas máquinas virtuales "crudas" y así probar código que realice operaciones sensitivas de bajo nivel como manipulación de tablas de páginas y similares sin preocuparnos por que se pueda dañar el host y sin tener que entender la forma en que lo hace un kernel preexistente. En esta presentación se mostrará cómo usar KVM para crear un lanzador de máquinas virtuales, así como un kernel de 16-bit en modo real y otro de 32-bit en modo protegido. Ambos ejemplos son fácilmente extensibles a kernels más sofisticados que prueben todo tipo de características de bajo nivel de la plataforma, incluso a sistemas operativos pequeños con fines pedagógicos.
El razonamiento local posibilitado por la Separation Logic ha demostrado ser una gran herramienta para la verificación de programas con un manejo complejo de punteros. Sin embargo el poder de esta lógica encuentra su limite en situaciones en las que es necesario especificar diversas estructuras que comparten el heap, ya sea por la dificultad de especificarlas de manera disjunta, ya sea por la imposibilidad de hacerlo sin romper las abstracciones que estas estructuras proveen. En esta charla presentamos una generalización de la Separation Logic que permite especificar precisamente estructuras complejas en el heap, relaciones de sharing entre ellas, y un sistema de prueba composi cional asociado para verificar programas de forma modular bajo ciertas condiciones, aun cuando no es posible garantizar una completa separación espacial de las estructuras manipuladas.
Manuel Sadosky (1914-2005) fue el introductor de la Computación universitaria en la Argentina y Uruguay. Su accionar tuvo también amplia repercusión en Latinoamérica.
En 1960, trajo al país la primera computadora "Clementina", que se incorporó al Instituto de Cálculo de la Facultad de Ciencias Exactas de la UBA iniciando un acelerado proceso de desarrollo académico.
En 1986, siendo Secretario de Ciencia y Técnica de la Nación, fundó la ESLAI, Escuela Latinoamericana de Informática.
Generaciones de ingenieros y técnicos estudiaron por sus libros de cálculo diferencial conocido en la jerga estudiantil como "Sadosky Guber".
Fue hijo de un modesto zapatero, se recibió de Maestro Normal, luego de Doctor en Matemática en la UBA y después completo sus estudios en Europa. Jamás perdió su humildad ni su entusiasmo, pese a que muchos de sus exitosos proyectos académicos quedaron truncos por cambios políticos. Su entusiasmo renacía fortalecido luego de cada frustración para continuar bregando por sus propósitos.
Se verá, mediante algunos ejemplos, que su honestidad, compromiso social y bonhomía, trascendieron los límites imaginables.
Bajo la sombra de su obra crecieron las Carreras de Computación argentinas y uruguayas.
La teoría de la computabilidad estudia los límites de los "métodos efectivos". Pero ¿qué es un método efectivo? Ahora es fácil responder a esa pregunta: lo efectivo es lo computable, es decir, lo que se pueda resolver usando una computadora. Sin embargo, comenzaron a pensar en esta noción mucho antes de que existieran las computadoras. En la primera parte de la charla voy a contarles cuáles fueron las primeras intuiciones, los primeros intentos para capturar la noción de método efectivo, y algunos resultados importantes del área.
Dentro de la teoría de la computabilidad, el estudio de la aleatoriedad despertó mucho interés en los últimos años. En la segunda parte de la charla voy a hablar sobre esto. ¿Cómo se puede definir la aleatoriedad? Supongamos que tiramos una moneda 30 veces y anotamos 0 si sale cara y 1 si sale ceca. ¿Por qué no me creen si les digo que salió 101010101010101010101010101010, pero sí me creen si les digo 110001010011001101000110100110? Las dos secuencias tienen longitud 30, de modo que las dos son igual de probables... Vamos a ver dos formas distintas de definir la noción de "secuencia aleatoria", una basada en apuestas en ruletas y otra en grados de compresión. Las dos definiciones van a estar basadas en computadoras y van a usar resultados de la teoría de la computabilidad.
Los que aguanten hasta el final de la charla se llevan como premio un método infalible para ganar a la ruleta.
El objetivo de esta charla es presentar un análisis preliminar de las experiencias y vivencias de estudiantes que ingresan a la universidad para cursar la carrera de Ciencias de la Computación en la Facultad de Matemática, Astronomía y Física de la Universidad Nacional de Córdoba. En el primer año de esta carrera el nivel de deserción y fracaso es elevado. El interés de esta presentación, que comenta parte una investigación en curso, es observar, caracterizar y analizar cómo se realiza el encuentro entre los alumnos recién llegados y la comunidad de la facultad a la que los estudiantes pretenden integrarse.
Durante el primer año de la carrera los estudiantes deben cursar materias introductorias de programación. Esta tarea es abordada desde una perspectiva formal, los programas son vistos como fórmulas matemáticas largas las cuales se construyen y demuestran utilizando la inducción matemática. En síntesis, los alumnos deben aprender una nueva notación, un lenguaje de axiomas y reglas de construcción y el significado de demostrar una proposición -por inducción, reducción al absurdo, análisis de casos, contraejemplo-.
Simultáneamente, los estudiantes comienzan a vivenciar la presencia de valores y convenciones sociales que sostiene la comunidad. Estas normas implícitas están relacionadas con las características que debe reunir un alumno exitoso, el comportamiento y las actitudes que deben adoptarse, el status de los conocimientos previos del alumno y las relaciones de poder entre profesores y alumnos.
Este complejo y difícil proceso de ingreso a la comunidad involucra la creación, modificación y renegociación del lenguaje, los valores y los conocimientos previos de los aprendices. El éxito en este proceso de iniciación permitirá a los estudiantes lograr una participación cada vez mayor en la comunidad.
A través de una metodología de investigación cualitativa, basada en entrevistas y observaciones de clases se intenta delinear cómo las características de las prácticas áulicas organizan y constituyen el aprendizaje. También se analiza cómo se construyen, de manera situada dentro del aula, las nociones de demostración, abstracción y formalización, consideradas centrales para lograr una participación legítima en la comunidad.
En los casos en que algunos componentes de un sistema tienen un funcionamiento imperfecto (por ejemplo, cuando un medio de transmisión puede perder datos con cierta probabilidad) es interesante calcular cuál es la probabilidad de que el sistema funcione correctamente. Además, algunas de las fallas no tienen un comportamiento probabilístico, por lo que se introducen decisiones no deterministas.
En esta charla explicaremos cómo las decisiones probabilistas y no deterministas interactúan en procesos concurrentes.
El estudio de esta interacción es útil para la verificación de protocolos de comunicación, tolerancia a fallas, scheduling, criptografía. Se analizarán ejemplos de este tipo de sistemas.
El Centro Internacional Franco Argentino de Ciencias de la Información y de Sistemas, CIFASIS, es el séptimo y también el más joven de los institutos de investigación del CONICET que están localizados en Rosario. Además, el CIFASIS es el primer centro creado en el área de informática dentro del sistema de institutos del CONICET. El centro fue creado en Julio de 2007 como resultado de un convenio firmado entre la Universidad Nacional de Rosario, el CONICET y la Universidad Paul Cézanne Aix-Marseille III, Francia.
En esta presentación se comentará sobre las distintas acciones y programas que se están llevando a cabo en el CIFASIS o con su apoyo y también los planes para el futuro próximo.
Desde su nacimiento, la Computación ha estado íntimamente ligada a la Lógica. Hoy en día, el interés por la Lógica es impulsado en mucha mayor medida desde la Computación que desde otras disciplinas históricamente afines, como la Matemática o la Filosofía. Actualmente la Computación abarca un número muy diverso de áreas de interés, y en cada una de ellas ciertas lógicas se adecúan mejor que otras. Los criterios a la hora de elegir una lógica son principalmente: un lenguaje acorde al dominio de uso, poder expresivo suficientemente alto y, en la medida de lo posible, un bajo costo computacional. En esta charla vamos a presentar de manera intuitiva algunos resultados sobre propiedades teóricas y computacionales de diferentes lógicas modales e híbridas y algunas herramientas de demostración automática desarrolladas.
Presentaremos los fundamento y datos experimentales detras de la herramienta ParAlloy. ParAlloy permite analizar modelos relacionales escritos en el lenguaje de modelado Alloy utilizando SAT-solving distribuido. ParAlloy incorpora tecnicas novedosas de SAT-solving distribuido, utilizado información sobre los modelos relacionales.
La verificación formal de programas es una práctica habitual en el campo de la ciencia computacional. Sin embargo, algunos filósofos y científicos han argumentado que esta práctica no podría ser justificada. Para sostener esta posición se han propuesto argumentos sociológicos (De Millo, Lipton) y argumentos filosóficos (Fetzer). En gran medida estos argumentos suponen una distincion entre algoritmos y programas. Así Fetzer sostiene que una verificación formal "completa" sólo se puede hacer sobre algoritmos, no sobre programas. En el presente trabajo discutiremos algunos de los supuestos de los argumentos contra la verificación formal.
DEVS es un formalismo que permite representar y simular sistemas de eventos discretos generales. En esta charla, presentaremos los principios del formalismo y sus principales extensiones y aplicaciones, mostrando también algunos de los resultados obtenidos por nuestro grupo. Entre estos últimos, veremos el software PowerDEVS, un simulador DEVS de propósito general desarrollado por el grupo con capacidad para realizar las simulaciones en tiempo real.