Listar AD - CTG – Informática por fecha de publicación

Mostrando ítems 21-40 de 76

    • Tool Interoperability in the Maude Formal Environment 

      Durán, Francisco; Rocha, Camilo; Álvarez, José María (SpringerBerlín, 2011)
      We present the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can seamlessly interact with the Maude Termination Tool, the Maude Sufficient Completeness Checker, the ...

    • Proving Safety Properties of Rewrite Theories 

      Rocha, Camilo; Meseguer, José (SpringerBerlín, 2011)
      Rewrite theories are a general and expressive formalism for specifying concurrent systems in which states are axiomatized by equations and transitions among states are axiomatized by rewrite rules. We present a deductive ...

    • Intellifilter: sistema de filtrado parental soportado por aprendizaje maquinal supervisado 

      Cadavid Rengifo, Héctor Fabio; Cely Higuera, Jorge Humberto; García Segura, Juan Pablo (REDISColombia, 2011)
      En este artículo se presenta la herramienta Intellifilter para el filtrado de contenidos de internet no aptos para niños, basada en un conjunto de técnicas de aprendizaje supervisado1 para clasificación de texto e imágenes, ...

    • A Formal Interactive Verification Environment for the Plan Execution Interchange Language 

      Cadavid Rengifo, Hector Fabio; Rocha, Camilo; Muñoz, Cesar (Springer NatureUSA.Switzerland, 2012)
      The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive ...

    • A Formal Interactive Verification Environment for the Plan Execution Interchange Language 

      Rocha, Camilo; Cadavid, Héctor; Siminiceanu, Radu (© 2020 Springer Nature Switzerland AG.Springer, Berlin, Heidelberg., 2012)
      The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive ...

    • Order-Sorted Equality Enrichments Modulo Axioms 

      Gutiérrez, Raúl; Meseguer, José; Rocha, Camilo (SpringerBerlin., 2012)
      Built-in equality and inequality predicates based on comparison of canonical forms in algebraic specifications are frequently used because they are handy and efficient. However, their use places algebraic specifications ...

    • Learning from Corporate Memory and Best Practices 

      Matta, Nada (© 2012 The Author(s). Licensee IntechOpen.Rijeka, Croatia., 2012-03-02)
      Due to the development of mobile and Web 2.0 technology, knowledge transfer, storage and retrieval have become much more rapid. In recent years, there have been more and more new and interesting findings in the research ...

    • MUNDOS VIRTUALES INMERSIVOS PARA EDUCACIÓN, TRABAJO COLABORATIVO Y SIMULACIÓN 

      Álvarez Piñeiro, Claudia Patricia (ACOFIColombia, 2013)
      Being able to observe the customs of teenagers and young adults known as ``digital natives'' has helped in understanding how they enjoy playing in simulated worlds. During the virtual gatherings, they are ...

    • TRANSFORMACIÓN DE PRÁCTICAS PEDAGÓGICAS USANDO TIC Y RENATA: CONTEXTO Y CASOS DE ESTUDIO EN BIOMEDICINA Y ECONOMÍA 

      Álvarez Piñeiro, Olga Patricia; Cadavid-Rengifo, Héctor (© 2013 Asociación Colombiana de Facultades de Ingeniería (ACOFI), International Federation of Engineering Education Societies (IFEES), 2013)
      Este artículo presenta dos propuestas de transformación de las prácticas pedagógicas con apoyo de tecnología, diseñadas como parte del proyecto de investigación “Diseño de un modelo de transformación de prácticas educativas ...

    • Automatic proof-search heuristics in the Maude invariant analyzer tool 

      Rocha, Camilo (Switzerland, 2013)
      The Invariant Analyzer Tool is an interactive tool that mechanizes an inference system for proving safety properties of concurrent systems, which may be infinite-state or whose set of initial states may be infinite. This ...

    • Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool 

      Rocha, Camilo; Meseguer, José (Springer., 2014)
      The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a ...

    • SIMULADOR PARA EL APOYO AL PROCESO DE MEJORAMIENTO CONTINUO DE PYMES CON TOC 

      Cadavid-Rengifo, Héctor; Ospina Hernandez, Gerardo (Congresso Nacional de Excelência em Gestão, 2014)
      Una gran parte de las pequeñas y medianas empresas Colombianas han mostrado, de acuerdo con cifras oficiales, unos muy bajos índices de supervivencia tras sus primeros años de creación. Esto es especialmente grave dado que ...

    • Synchronous set relations in rewriting logic 

      Muñoz, César; Rocha Niño, Hernán Camilo (Elsevier, 2014)
      This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract ...

    • Tecnologías de Información como apoyo a la Estrategia De las Instituciones Prestadoras de Salud en Colombia 

      Cerinza, Daniel; Ospina, Victoria Eugenia (Colombia., 2015)
      La tecnología al servicio del negocio, no el negocio al servicio de la tecnología. Es importante tener clara esta relación para que las tecnologías de Información (TI) son un generador de beneficios en las organizaciones. ...

    • M-health system backend supported by an actors model 

      Corredor Acosta, Manuel Alejandro; Cadavid Rengifo, Hector Fabio (IEEE XploreNew Jersey, USA., 2015)
      Given the serious impact that cardiovascular diseases are having in Colombia's deaths, the Colombian School of Engineering has been developing a platform for remote, real time, cardiac signals processing. One of the main ...

    • Consideraciones tecnológicas como resultado de la construcción de la arquitectura empresarial para una institución de educación superior 

      Santiago Cely, Claudia Patricia; Castillo Navetty, Oswaldo (Editorial Escuela Colombiana de Ingeniería Julio GaravitoBogotá, 2015)
      Las tecnologías de la información y la telecomunicación (TIC) permean todos los ámbitos de cualquier organización y por ello es clave aprovechar al máximo su uso. Basándose en las necesidades y modo de operación de una ...

    • The Formal System of Dijkstra and Scholten 

      Rocha, Camilo (Springer.Springer, Cham., 2015)
      The logic of E.W. Dijkstra and C.S. Scholten has been shown to be useful in program correctness proofs and has attracted a substantial following in research, teaching, and programming. However, there is confusion regarding ...

    • Tecnologías de Información como apoyo a la estrategia de las instituciones prestadoras de salud en Colombia 

      Ospina-Becerra, Victoria Eugenia; Cerinza Mejía, Daniel Ricardo (Orlando, Florida, E.E.U.U., 2015)
      La tecnología al servicio del negocio, no el negocio al servicio de la tecnología. Es importante tener clara esta relación para que las tecnologías de Información (TI) son un generador de beneficios en las organizaciones. ...

    • ¿Es OPENLDAP una buena solución libre para la centralización de usuarios? 

      Gómez Sarmiento, Tatiana Marcela; Morera González, María Alejandra; Muñoz Moreno, Aura María; Santiago Cely, Claudia Patricia (LACCEIBoca Raton, Florida – USA., 2015)
      This article establishes the state of the art about existing solutions in the market, free or licensed that allow the centralization of users, independent to the operating system they use (OS X, Windows, Linux); all of the ...

    • Propuesta de evaluación de herramientas de monitoreo para plataformas tipo nube 

      Rodríguez Chona, Andrés Ricardo; Patiño Arias, Andrés Mauricio; Santiago Cely, Claudia Patricia (Escuela Colombiana de IngenieríaColombia, 2016)
      A lo largo de este articulo se presenta una metodología para la evaluación de herramientas de monitoreo para la nube que se basa en una matriz de evaluación. Dicha matriz de evaluación se compone de dos dimensiones: la ...