Desafíos y Oportunidades de la Investigación en Métodos Formales Edgar SERNA M. Corporación Universitaria Remington. Facultad de Ciencias Básicas e Ingeniería [email protected] Medellín, Colombia.

Alexei SERNA A. Instituto Antioqueño de Investigación. Grupo de Investigación CCIS [email protected] Medellín, Colombia. RESUMEN La investigación teórica y tecnológica en métodos formales ha alcanzado recientemente significativos avances, lo que hace vislumbrar aplicaciones ambiciosas en las próximas décadas. En especial, será posible aplicarlos para apoyar rigurosos y coherentes planes de estudio en matemáticas, Ciencias Computacionales y algunas ingenierías, a las que se incorporarán para verificar hardware, software, algoritmos y protocolos, y para el modelado y el diseño de sistemas de software complejos. En la industria, se utilizarán para capturar requisitos y reglas de negocio, para generar casos de prueba y escenarios, para explorar diseños, para verificar protocolos y para producir casos seguros. En otras disciplinas científicas y de ingeniería se utilizarán para apoyar el modelado y el análisis a nivel de sistema. En los próximos años los métodos formales tendrán una comunidad de investigación mucho más amplia y cubrirán una mayor gama de disciplinas. En este artículo se describen los desafíos y oportunidades que debe afrontar la investigación en esta área del conocimiento para alcanzar estas metas, desde las visiones de la formación, la ciencia y la industria. Palabras clave: Métodos formales, Ciencias Computacionales, verificación formal, formación, lógica.

1. INTRODUCCIÓN Para explicar por qué funcionan o fallan las cosas se utiliza argumentos lógicos, pero para verificar la correctitud de un producto se utiliza argumentos formales, que están conformados por una estructura precisa de axiomas y reglas de inferencia. Mediante la codificación de estas reglas y utilizando un computador, se puede comprobar mecánicamente los argumentos formales de una especificación para verificar si es correcta. Las técnicas automatizadas de razonamiento formal también se utilizan para generar ejemplos de algunas limitaciones en matemáticas. El marco axiomático ha hecho parte del método científico desde Platón y el uso del razonamiento formal ha sido defendido desde las investigaciones de Raymond Lully [1] y Leibniz [2]. La investigación en métodos formales ha alcanzado significativos progresos en los últimos años, y como herramienta y teoría se utilizan cada vez más en una amplia variedad de formas en la industria. Muchos de los problemas desafiantes en la construcción de sistemas

software seguros, en la programación de procesadores multi-núcleo y en los sistemas ciber-físicos requieren el apoyo formal para su modelado y análisis. Po otro lado, existe un número creciente de aplicaciones para ellos en la investigación en Ciencias Computacionales (CC) y en otras disciplinas ingenieriles y científicas. Pero a pesar de sus logros y eficiencia demostrada, los métodos formales todavía no son una parte integral de los procesos formativos en CC, e incluso a nivel de postgrado pocos estudiantes siguen carreras de investigación en esta tecnología. En este trabajo se resume algunos de los desafíos que enfrentan los métodos formales para lograr una mayor utilización y aplicación en los procesos formativos, en la ciencia y en la industria, y se describe las oportunidades para sus aplicaciones. 2. CONTEXTO DE LOS MÉTODOS FORMALES Las Ciencias Computacionales se basan en la construcción y el estudio de la lógica y la abstracción puras. Aunque los computadores existen en la realidad física, la computación realmente se encarga de la representación y la manipulación de la información, que es algo inmaterial. Mientras las matemáticas tratan con las leyes de las entidades abstractas, como los números, los conjuntos, las superficies, los volúmenes, las relaciones, el álgebra y los homomorfismos, la computación se focaliza en la manipulación de la información representada en abstracciones, como los bits, los vectores-bit, las matrices, las tablas, las pilas, las colas, los árboles y las bases de datos. Las matemáticas se utilizan para representar y analizar la realidad física, pero la computación se puede utilizar para el modelado y la simulación. Mientras que las primeras tratan con operaciones con descripciones concisas, el hardware y el software de los sistemas computacionales son construcciones complejas. Los sistemas software son necesarios para que el hardware se desempeñe con precisión y fiabilidad, incluso al tratar con datos poco fiables, porque están propensos a fallos de sus componentes físicos. Un científico computacional debe desarrollar capacidad lógico-interpretativa y abstractiva [3] para

la

comprender los problemas y modelar las soluciones mediante abstracciones, con el fin de especificar formalmente los requisitos, construir representaciones de datos que sean eficaces y expresivas, diseñar algoritmos correctos y eficientes que funcionen con todas las entradas posibles, y moldear diseños en un código confiable. La lógica y la abstracción son importantes para formalizar el entorno en el que el software funcionará, para especificar los requisitos, para diseñar e implementar la arquitectura del sistema y los componentes, y para depurar y mantener el sistema en el tiempo. Estos científicos están constantemente solucionando problemas, generando representaciones de datos, algoritmos y protocolos, diseñando nueva programación y lenguajes descriptivos, y resolviendo conflictos de sincronización. En los últimos sesenta años las CC han logrado desarrollar un cuerpo de conocimientos lógico-abstractos para resolver esos problemas, entre los que se encuentra los métodos formales. Los sistemas computacionales tratan con la complejidad a todos los niveles, desde las plataformas hardware, los protocolos y las representaciones de datos hasta los sistemas ciber-físicos y las sofisticadas amenazas a la seguridad. Los métodos formales representan un enfoque para gestionar esta complejidad mediante el uso de representaciones simbólicas de abstracciones, extraídas como fórmulas lógicas desde las matemáticas y la computación. Estas fórmulas se pueden manipular de varias maneras para construir pruebas, a la vez que se ven como obstáculos a resolver. La computación trata con fenómenos dinámicos en autómatas y máquinas de estado, y para capturar el comportamiento y las propiedades computacionales se utilizan los formalismos expresivos de la lógica temporal. Los métodos formales se han desarrollado por más de cinco décadas, desde el trabajo pionero de McCarthy [4], y han introducido teorías como la programación funcional, la programación lógica, la semántica denotacional, la semántica operacional, la semántica axiomática, los sistemas tipos, la teoría de tipos, la invariancia, la terminación, la seguridad, la vida de conexión, la lógica modal, la lógica temporal, la lógica descriptiva, los lenguajes de especificación, el álgebra de procesos, la interpretación abstracta, la verificación en tiempo de ejecución, y otras innovaciones conceptuales influyentes. Casi una cuarta parte de los premios Turing [5] entregados entre 1966 y 2007 fueron reconocimientos a trabajos con un componente significativo de métodos formales. Actualmente, el campo de los métodos formales está en una encrucijada. En el lado positivo, la tecnología está bien desarrollada, existe un amplio número de aplicaciones interesantes y de importantes usuarios industriales. Sólo en Microsoft Research existe cerca de un centenar de investigadores trabajando en el desarrollo y uso de los métodos formales. Sin embargo, en el lado negativo, no se consideran un componente de la corriente principal de las Ciencias Computacionales. Existen pocos

profesores universitarios trabajando en el área, la oferta de cursos a nivel de pregrado o postgrado es escasa, difícilmente se desarrollan proyectos importantes, y sólo un pequeño número de graduados de doctorado los acogen como fuente de investigación y trabajo. Además, la capacidad lógico-interpretativa y abstractiva de los estudiantes a nivel de pregrado y postgrado y no se desarrolla [6], y por el contrario parece haber disminuido en los últimos años, a la vez que los planes de estudios en CC generan cada vez más fobia hacia cuestiones relacionadas con ella y las matemáticas [7]. La tecnología de los métodos formales es emocionante y cada vez más relevante. Con el incremento del poder computacional de la última década es el momento de llevar las Ciencias Computacionales a la esfera semántica de los modelos y la inferencia, lo que posibilitará una serie de nuevas aplicaciones en los procesos formativos y en la industria. Como por ejemplo en los modelos de hardware digital y analógico, las teorías matemáticas, los sistemas físicos estáticos y dinámicos, las redes biológicas, los sistemas software complejos, e incluso la psicología, la filosofía y las interacciones sociales [8]. La formación a todos los niveles se puede beneficiar del modelado y el análisis formal y del uso de metáforas computacionales. Actualmente, los procesos formativos en diversas áreas se desarrollan en términos de tareas de procesamiento de información de bajo nivel, mientras que la percepción real se obtiene mediante el uso de modelos computacionales y de CC. Por ejemplo, los autómatas finitos pueden servir como metáfora para una serie de tareas, como el funcionamiento de una máquina expendedora, los analizadores de lenguajes, o los videojuegos, y los juegos interactivos en sí constituyen otra metáfora computacional. Los sistemas dinámicos se pueden utilizar para modelar flujos continuos, como los vehículos en movimiento, los proyectiles, los niveles de fluidos, los reguladores de velocidad, los circuitos analógicos y los péndulos. Los sistemas híbridos combinan cambios de estados discretos y continuos, y se pueden utilizar para termostatos modelo, sistemas de control de navegación y sistemas biológicos y económicos. Los modelos computacionales, las metáforas y la tecnología pueden enriquecer los procesos formativos a todos los niveles en las Ciencias Computacionales, ya sea mediante el apoyo a la formación, el desarrollo de competencias, o la colaboración y la comunicación. La aceptación industrial de los métodos formales también se puede ampliar. Actualmente, algunas industrias son productoras y consumidoras de herramientas formales. Por ejemplo, Intel y AMD los utilizan para controlar la equivalencia de circuitos, generar secuencias de prueba, controlar modelos de controladores de estado finito, y para demostrar teoremas acerca de algoritmos aritméticos de punto flotante. Microsoft tiene una serie de proyectos que utilizan software de comprobación de modelos y

razonamiento automatizado para analizar el código secuencial para terminación, correctitud asercional y la ausencia de vías y callejones sin salida. Rockwell-Collins utiliza el razonamiento automatizado para la verificación de software. Empresas de diseño electrónico automatizado, como Synopsys, Cadence y Mentor Graphics, venden herramientas para el control de modelos y de equivalencias, y Matlab aplica un verificador de diseño Simulink para generar casos de prueba y verificar propiedades. Sin embargo, estos esfuerzos son relativamente modestos en comparación con el uso sistemático que se le puede dar a las herramientas formales en cualquiera tipo de proceso. Aunque la tecnología formal todavía no está lista para uso masificado, hoy se tiene un marco amplio para pensar en aplicaciones no tradicionales más ambiciosas. Se necesita innovaciones audaces que aprovechen la potencia de las herramientas y técnicas formales modernas para transformar radicalmente los procesos formativos, tanto en computación como en otras disciplinas que valoran las metáforas computacionales. También se tiene una oportunidad para aprovechar los métodos formales en el modelado asistido por computador y en el diseño de sistemas complejos. 3. COMPONENTES DE LOS MÉTODOS FORMALES La idea de colocar a las matemáticas y a la ciencia sobre una base axiomática se remonta a Pitágoras, Platón, Aristóteles y Euclides [9]. El uso de un lenguaje formal soportado en un razonamiento mecanizado fue defendido por primera vez por Raymon Lully en el siglo XIII [1] y más tarde por Gottfried Leibniz en el siglo XVII [2]. Refiriéndose al uso de la tecnología computacional para gestionar grandes volúmenes de información, Vannevar Bush [10] sugirió que la lógica puede llegar a ser muy difícil, y sin duda sería muy conveniente generar más seguridad en su uso. Es posible que algún día hagamos clic sobre las opciones operativas de una máquina con la misma seguridad que hoy registramos las ventas en una caja registradora (p. 12). Hoy, con el incremento de la potencia computacional y el desarrollo de potentes herramientas software para el razonamiento formal, la ciencia está mucho más cerca de alcanzar los objetivos que se trazaron estos pensadores visionarios. La terminación y la invariancia son dos componentes importantes de los métodos formales para verificar código secuencial. Por ejemplo, considere una bolsa con n pelotas blancas y negras y con un suministro ilimitado de pelotas por fuera de la bolsa. Partiendo de que existen por lo menos dos bolas en la bolsa, el proceso consiste en tomar, cada vez, dos bolas de la bolsa e introducir una. Si las dos bolas que se toman tienen el mismo color se inserta una bola negra, y si es diferente se inserta una bola blanca, y así sucesivamente. ¿Es posible asegurar que este procedimiento terminará en algún momento?

¿Qué se puede afirmar acerca del color de la bola que queda en la bolsa con respecto al contenido inicial? Otro ejemplo es el problema del simple recuento de votos para determinar si en una elección alguno de los candidatos obtuvo la mayoría. La solución propuesta en el algoritmo de Boyer y Moore [11] funciona mediante la eliminación de pares de votos para candidatos diferentes, hasta que los que queden sean para un sólo candidato. El otro deberá ser el ganador, si alguien tiene la mayoría. Es posible que ninguno de los candidatos obtenga más de la mitad de los votos. ¿Por qué funciona este algoritmo? La explicación radica en su prueba. En líneas generales, si un candidato V tiene mayoría, entonces no importa cómo, los votos de V, se aparean y eliminen con los de los otros candidatos, porque no habrá votos para V que se queden sin pareja. Esta intuición se formaliza tanto en el algoritmo como en la prueba, pero en ambos casos los detalles de la formalización no son triviales. Estas pruebas formalizadas son útiles para descubrir, diseñar e implementar algoritmos correctos, así como en la demostración de que son correctos. La semántica formal explica la interpretación matemática de un fragmento de texto, o una propiedad del programa, y las técnicas de sondeo propuestas para el razonamiento acerca de los programas y sus propiedades. Es un prerequisito para la aplicación exitosa de los métodos formales. La composición es un desafío clave en la semántica formal, porque es conveniente desarrollar las propiedades de los programas en términos de los subprogramas constituyentes. Los recientes avances en semántica de programas han permitido formalizar su comportamiento con almacenamiento dinámico, programas orientados a objetos y programas concurrentes. La automatización juega un rol importante en la aplicación exitosa de los métodos formales, debido a que para verificar el comportamiento del software y el hardware de estado finito se puede utilizar, con una cantidad limitada de esfuerzo, la comprobación de modelos para anotar los estados con sus propiedades de comportamiento. Por ejemplo, para una determinada propiedad esto se puede hacer en un tiempo lineal en el tamaño del espacio de estado del sistema. Por supuesto, ese espacio puede ser enorme, porque incluso un sistema con n bits de estado tiene 2n estados posibles. El problema de explosión de estados en la comprobación de modelos se ha abordado de diversas formas mediante el uso de representaciones simbólicas, abstracciones y reducciones de orden parcial. La comprobación de modelos se ha extendido a los sistemas de estado infinito, como los paramétricos, los de tiempo real y los híbridos lineales. La satisfacibilidad booleana mediante la verificación limitada de modelos también se utiliza para representar y razonar acerca de estos sistemas. En los últimos años se han hecho

importantes mejoras algorítmicas en estos procedimientos, que han sido explotadas por los solucionadores de restricciones procedentes de una mezcla de teorías, como las de la aritmética, los arreglos, los vectores de bits y los tipos de datos recursivos. Los procedimientos de satisfacción se pueden utilizar para comprobar que una fórmula extensa no se puede satisfacer, o para generar contraejemplos, casos de prueba, o calendarios, cuando la fórmula en realidad se puede satisfacer. 4. DESAFÍOS Y OPORTUNIDADES En este siglo no existe duda acerca de que los métodos formales se deben utilizar más ampliamente en la academia y la industria, y muchos de los problemas de complejidad que se presentan en la Ingeniería de Software moderna, como los relacionados con los procesadores de múltiples núcleos, las máquinas virtuales múltiples, los requisitos para mayor seguridad y los sistemas distribuidos globalmente, no se resuelven eficientemente con los métodos existentes, porque son densos en las pruebas. También se puede argumentar que la formación en Ciencias Computacionales se podría beneficiar con la introducción de herramientas y técnicas formales al currículo; sin embargo, existen algunos desafíos que se deben abordar antes que los beneficios de los métodos formales sean un caso convincente. 1. Los lenguajes de programación utilizados en el desarrollo de software a gran escala tienen una semántica formal compleja. Parte de ella es innecesaria e inútil, pero las herramientas formales tendrán que hacer frente a la complejidad de características como el flujo de información, las interrupciones, las discusiones y la concurrencia. 2. La aplicación exitosa de los métodos formales requiere habilidad e ingenio, incluso con una automatización amplia, pero los usuarios potenciales podrían no estar dispuestos a invertir tiempo y dinero en una tecnología sin tener una idea clara de los beneficios. 3. El costo de la aplicación de los métodos formales en un proyecto de desarrollo de software puede ser alto, y no se realmente hasta qué punto su aplicación puede reducir los costos de las pruebas. 4. Las herramientas formales no son lo suficientemente amigables con el usuario como para pensar en un uso más amplio. En particular, cuando falla un proceso de verificación no se obtiene una respuesta útil; además, el mantenimiento de un desarrollo formal es una tarea de grandes proporciones, comparable a las del mantenimiento de software. 5. Existen diversas herramientas formales eficientes, pero a menudo los problemas difíciles requieren una

combinación de varias de ellas. La interoperabilidad es un desafío para estas herramientas, porque presentan sutiles diferencias semánticas que se deben superar. La comunidad de investigadores de los métodos formales ya han comenzado a trabajar algunos de estos desafíos, y mucho de ese esfuerzo tecnológico está orientado para hacer que su funcionamiento sea transparente al usuario [12]. El costo de la aplicación de los métodos formales bajará a medida que las herramientas sean más potentes y más integradas. La ley de Moore proporciona una fuerte aceleración en el poder de las herramientas formales, y a medida que la tecnología se estabiliza el desarrollo de interfaces de usuario amigables se convertirá en una prioridad. Sea cual sea el futuro, la investigación en métodos formales de hoy enfrenta una serie de desafíos, los cuales de resumen a continuación. 4.1 En los procesos formativos Los métodos formales deben estar plenamente integrados en la formación de un científico computacional. La formación en temas como matemática discreta, lógica computacional, teoría de la computación, algoritmos, bases de datos, compiladores, sistemas operativos, arquitectura de computadores, lenguajes de programación, Inteligencia Artificial y análisis numérico se puede lograr con mayor eficacia si se utilizan métodos y herramientas de modelado y análisis formal. Estos cursos carecen actualmente de formalidad, y los programas en Ciencias Computacionales e Ingeniería son cada vez más alérgicos a las matemáticas. Esto significa que los egresados de estos programas no están significativamente mejor calificados, en áreas como la lógica y la abstracción, de lo que están los egresados en otras disciplinas. Existen algunos esfuerzos preliminares en esta dirección, como el uso de herramientas para la formación en Ingeniería de Software y en pruebas formales, que están dando resultado; la propuesta de Wing [13] puede servir como modelo para la incorporación en los cursos de computación e ingeniería de los métodos formales y las herramientas de verificación; el proyecto TeachScheme! [14] experimenta con el demostrador de teoremas ACL2, para formar a estudiantes de primer año en programación; además, herramientas como Alloy y Coq se aplican con buenos resultados en procesos formativos en Ingeniería de Software. Otras disciplinas también se pueden beneficiar de la utilización de los métodos formales. Debido al éxito de la verificación formal del hardware, los estudiantes de ingeniería eléctrica y electrónica están cada vez más necesitados de aplicar el razonamiento booleano y la lógica temporal. Muchos cursos de ingeniería utilizan el framework de MATLAB en el modelado y la simulación. Estos modelos son formalizables y a partir de la integración del razonamiento y la simulación se puede

lograr muchos beneficios pedagógicos. Mathematica es una herramienta popular para el álgebra computacional y un medio para desarrollar cursos [15, 16], que junto a otros sistemas de álgebra computacional se pueden mejorar para el desarrollo de pruebas, como se ha hecho con REDLOG [17]. La combinación del modelado, la construcción de pruebas y las herramientas de álgebra computacional puede sustituir a los libros de texto por livebooks, que combinen la información con el software para apoyar la experimentación, la visualización y la prueba. Las herramientas de abstracción que se aplican durante un curso determinado pueden llegar a hacer parte de las herramientas cotidianas del estudiante. 4.2 En la ciencia Los modelos formales y las técnicas de análisis se utilizan en algunas ciencias para lograr la comprensión a nivel de sistema. Por ejemplo, las redes reguladoras de genes se pueden modelar como redes booleanas, sistemas híbridos, o sistemas estocásticos, y utilizando la deducción y la verificación de modelos se puede analizar sus propiedades. La iniciativa de Systems X [18] logra una visión de diferentes procesos naturales y artificiales a nivel de sistema. Estos modelos capturan algunas abstracciones del sistema destino real utilizando máquinas de estado y limitaciones. Las técnicas formales se pueden utilizar para deducir las propiedades de estos modelos, y el análisis para las teorías de prueba, el diagnóstico de problemas y para hacer predicciones. 4.3 En la industria Microsoft cuenta con cerca de un centenar de investigadores que trabajan en métodos formales. Otras compañías tecnológicas, como Intel, AMD, Rockwell Collins y The MathWorks, desarrollan y utilizan activamente herramientas formales. Algunos proveedores de automatización de diseño electrónico, como Cadence, Mentor Graphics y Synopsys, cuentan con importantes productos de verificación formal en su suite de herramientas. Microsoft trabaja en cerca de una decena de grandes proyectos en desarrollo formal de herramientas de Ingeniería de Software, para la especificación, la notación, la generación de pruebas, la verificación de modelos y la comprobación de seguridad, y varios se centran en la construcción de un motor para deducir y explorar modelos simbólicos. Se necesitan herramientas en dominios con estrictos requisitos de seguridad, mientras que las automatizadas se pueden insertar en entornos de desarrollo integrados IDEs y en compiladores. Un desafío particular para los métodos formales es el desarrollo de sistemas ultra-grandes, los cuales integran componentes de software y de hardware desde diversas fuentes.

fiabilidad y seguridad, es posible esperar que la implementación de los métodos formales en la industria se incremente. También se espera que los laboratorios de investigación industrial logren importantes resultados de investigación, así como en prototipos. 5. CONCLUSIONES Las décadas entre 1975 y 2005 se pueden considerar como la época dorada de la investigación en métodos formales. El trabajo de estos años produjo una serie de avances significativos en lógica y semántica de programas, lenguajes de especificación y programación, metodologías de diseño, técnicas de análisis estático, razonamiento automatizado, herramientas de verificación de modelos y asistentes de prueba interactivos. Se espera que en los próximos decenios la tecnología de los métodos formales expanda su campo de aplicación y audiencia, tal como se observa la tendencia actual [8]. Pero se espera: 1) que estas técnicas sean lo suficientemente potentes para ser utilizadas sin ningún tipo de esfuerzo intelectual manifiesto y 2) que la complementariedad entre la percepción y el juicio humano, y el cálculo soportado en computador y la inferencia se puedan aprovechar como herramientas clave en la gestión de la complejidad de la información. Se puede esperar que los métodos formales enriquezcan no sólo las Ciencias Computacionales sino otras disciplinas, las cuales se beneficiarán de la formalización y de la inferencia. Uno de los desafíos más importantes para la investigación en métodos formales será lograr impactar suficientemente los programas de formación, tanto a nivel de pregrado como de postgrado. Actualmente ya no es secreto que se necesitan más profesionales en Ciencias Computacionales y en Ingeniería, con una capacidad lógico-interpretativa y abstractiva lo suficientemente desarrollada como para presentar soluciones eficientes y eficaces a los complejos problemas de este siglo. Una sólida formación en métodos formales, matemática y lógica es la clave para superar este desafío. La esperanza es que se logré pronto materializar el sueño de Leibniz: de que en lugar de recurrir a argumentos técnicos seamos capaces de sentarnos frente a un computador y decir: Vamos a calcular. 6. REFERENCIAS [1] [2]

[3] [4]

Con la creciente conciencia en las capacidades de las herramientas formales y de requisitos más estrictos en

[5]

Waite, A. E. (2010). Raymund Lully The Illuminated Doctor Of Majorca. Kessinger Publishing. Bennett, J. (2003). Learning from Six Philosophers: Descartes, Spinoza, Leibniz, Locke, Berkeley, Hume. Oxford University Press. Serna, M. E. (2012). El Desarrollo de la Capacidad Lógico-Interpretativa y Abstractiva. Reporte Técnico: USBMED-FIDI-ESM-0112. McCarthy, J. (1959). Programs with Common Sense. Online [Feb. 2012]. http://amturing.acm.org/ [Jan. 2012].

[6]

Serna, M. E. (2011). Abstraction as a critical component in Computer Science training. Avances en Sistemas e Informática, 8(3), pp. 79-83. [7] Tucker, A. B.; Kelemen, C. F. & Bruce, K. B. (2001). Our curriculum has become Math-Phobic! ACM Sigcse Bulletin, 33(1), pp. 243-247. [8] Serna M. E. Métodos Formales: Perspectiva y Aplicación Futura. En H. Pérez G. et al. (Eds.), III Jornadas de Investigación Facultad de Ingenierías JOIN 2011, pp. 6468. [9] Boyer, C. B.; Merzbach, U. C. & Asimov, I. (1991). A History of Mathematics. Wiley. [10] Bush, V. (1945). As We May Think. The Atlantic Monthly, 1(1-2), pp. 1-18. [11] Boyer, R. S. & Moore, J. S. (1981). MJRTY – a fast majority vote algorithm. Technical Report 32. Institute for Computing Science, The University of Texas. [12] Tiwari, A.; Rushby, J. & Shankar, N. 2003. Invisible formal methods for embedded control systems. Proceedings of the IEEE, 91(1), pp. 29-39.

[13] Wing, J. M. (2000). Weaving formal methods into the undergraduate computer science curriculum. Lecture Notes in Computer Science, 1816, pp. 2-9. [14] Eastlund, C.; Vaillancourt, D. & Felleisen, M. ACL2 for freshmen: First experiences. Seventh International Workshop on the ACL2 Theorem Prover and its Applications, pp. 1-9. Austin, Texas, Nov. 15-16. [15] Kaltofen, E. (1997). Teaching computational abstract algebra. Journal of Symbolic Computation, 23(5-6), pp. 503-515. [16] Scott, D. S. (1991). Exploration with Mathematica. En: Rashid, R. F. (Ed.), CMU Computer Science: A 25th Anniversary Commemorative. Assn for Computing Machinery, p. 505-519. [17] Dolzmann, A. & Sturm, T. (1997). REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin, 31(2), pp. 2-9. [18] http://www.systemsx.ch/ [May 2012].