Hoja de vida

Nombre Hernán Camilo Rocha Niño
Nombre en citaciones Camilo Rocha
Nacionalidad Colombiana
Sexo Masculino

Redes sociales académicas

Google Scholar
ResearchGate
Repositorios disciplinares (Directorio Exit, eLIS, etc.)

Identificadores de autor

Autor ID (Scopus)
Open Researcher and Contributor ID (ORCID)

Formación Académica

  •  
  • Doctorado UNIVERSITY OF ILLINOIS
    Computer Science
    Agostode2006 - Diciembrede 2012
    Symbolic Reachability Analysis for Rewrite Threories
  •  
  • Maestría/Magister UNIVERSITY OF ILLINOIS
    Mathematics
    Agostode2010 - Diciembrede 2012
    N/A
  •  
  • Maestría/Magister UNIVERSIDAD DE LOS ANDES
    Magister en Ingeniería de Sistemas y Computación
    Juniode2003 - Septiembrede 2005
    Una semántica de ensamblaje de servicios y composición de componentes
  •  
  • Pregrado/Universitario UNIVERSIDAD DE LOS ANDES
    Ingeniería de Sistemas y Computación
    Enerode1997 - Septiembrede 2002
    Java-: un estudio semántico de un subconjunto de java concurrente

    Experiencia profesional

  •  
  • PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI
    Dedicación: 40 horas Semanales Enero de 2016 Enero de

  •  
  • ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO
    Dedicación: 40 horas Semanales Agosto de 2003 Diciembre de 2015

    Actividades de administración
    -  Miembro de consejo de centro - Cargo: Profesor de Planta e Investigador Agosto de 2003 de
    -  Miembro de consejo de centro - Cargo: Profesor de Cátedra Agosto de 2002 Agosto de 2003
  •  
  • Datum Ltda
    Dedicación: 48 horas Mensuales Julio de 2002 Agosto de 2003

    Actividades de administración
    -  Miembro de consejo de centro - Cargo: Analista Senior Julio de 2002 Agosto de 2003
    Actividades de investigación
    -   Investigación y Desarrollo - Titulo:  ERP Datum SUITE - Web Enable Enero 2003 Agosto 2003
    -   Investigación y Desarrollo - Titulo:  Sistema Único de Información (www.sui.gov.co) Julio 2002 Diciembre 2002

    Áreas de actuación

  •  Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación
  •  Ciencias Naturales -- Matemática -- Matemáticas Puras
  • Idiomas

      Habla Escribe Lee Entiende
  •  Inglés
  • Bueno Bueno Bueno Bueno
  •  Español
  • Bueno Bueno Bueno Bueno

    Líneas de investigación

  •  Métodos formales y lógica de reescritura, Activa:Si
  •  Algoritmos y grafos para analítica de datos, Activa:Si
  •  OpenIDAMS, Activa:No
  • Reconocimientos

  • Best paper award of FASE 2017, - Octubrede 2017
  • Best paper award FACS 2017, - Octubrede 2017
  • Tesis meritoria,PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI - Noviembrede 2018
  • Una de las mejores ponencias del 8o Congreso Colombiano de Computación, - Agostode 2013
  • Una de las cinco mejores ponencias del 2do Congreso Colombiano de Computación, - Abrilde 2007
  •  
    Los ítems de producción con la marca corresponden a productos avalados y validados para la última Convocatoria Nacional para el Reconocimiento y Medición de Grupos de Investigación, Desarrollo Tecnológico o de Innovación y para el Reconocimiento de Investigadores del SNCTeI

    Cursos de corta duración

  • Producción técnica - Cursos de corta duración dictados - Extensión extracurricular
  • HERNAN CAMILO ROCHA NINO, Symbolic Reachability Analysis for Rewrite Theories, Finalidad: Curso avanzado en reescritura (el curso duró una semana, y yo dicté excatamente 6 horas) . En: Chile  ,2014,  ,.  participación: Docente , 1 semanas 

    Trabajos dirigidos/tutorías

  • Trabajos dirigidos/Tutorías - Trabajos de grado de pregrado
  • HERNAN CAMILO ROCHA NINO, AGEVI: Agenda Virtual, un proceso integral de desarrollo de software  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis en curso  Proyecto de Grado,  2004. Dirigió como: ,   Persona(s) orientada(s):  Andrea Moreno, Marcela Moreno, Mauricio Niño  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
    Sectores:
    Desarrollo de programas (software) y prestación de servicios en informática - Desarrollo de programas (software),
  • Trabajos dirigidos/Tutorías - Trabajos de grado de pregrado
  • HERNAN CAMILO ROCHA NINO, PLAP: Plataforma de Pruebas para un Laboratorio de Ingeniería de Software  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis en curso  Proyecto de Grado,  2005. Dirigió como: ,   Persona(s) orientada(s):  Dagoberto Borda, Juan Carlos Martinez, Diego Neira  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
    Sectores:
    Desarrollo de programas (software) y prestación de servicios en informática - Desarrollo de programas (software),
  • Trabajos dirigidos/Tutorías - Trabajos de grado de pregrado
  • HERNAN CAMILO ROCHA NINO, ATOMS: Un modelo de componentes confiables  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis en curso  Proyecto de Grado,  2005. Dirigió como: ,   Persona(s) orientada(s):  Diego Labrador, Juan David Millán, Hugo Rey, Jimena Torres  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
    Sectores:
    Desarrollo de programas (software) y prestación de servicios en informática - Desarrollo de programas (software),
  • Trabajos dirigidos/Tutorías - Trabajos de grado de pregrado
  • HERNAN CAMILO ROCHA NINO, Una semántica ejecutable en lógica de reescritura para programación espacial concurrente por restricciones (SCCP)  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis concluida  Ingeniería de Sistemas y Computación,  2016. Dirigió como: Tutor principal,   Persona(s) orientada(s):  Miguel Angel Romero González  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
  • Trabajos dirigidos/Tutorías - Trabajos dirigidos/Tutorías de otro tipo
  • HERNAN CAMILO ROCHA NINO, Library Management for PVS  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis concluida  Ingeniería de Sistemas,  2015. Dirigió como: Tutor principal,   Persona(s) orientada(s):  Miguel Angel Romero González  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
  • Trabajos dirigidos/Tutorías - Trabajos dirigidos/Tutorías de otro tipo
  • HERNAN CAMILO ROCHA NINO, Double-spend Attack Models with Time Advantange for Bitcoin  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis concluida  Matemáticas,  2016. Dirigió como: Tutor principal,   Persona(s) orientada(s):  Carlos Antonio Pinzón Henao  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
  • Trabajos dirigidos/Tutorías - Trabajos de grado de pregrado
  • HERNAN CAMILO ROCHA NINO, Especificación formal y verificación de invariantes para un protocolo de coherencia del caché  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis concluida  Matemáticas,  2015. Dirigió como: Tutor principal,   Persona(s) orientada(s):  Sergio Steven Ramírez Rico  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
  • Trabajos dirigidos/Tutorías - Trabajos de grado de pregrado
  • HERNAN CAMILO ROCHA NINO, Una semántica formal para Apache Spark en lógica de reescritura  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis concluida  Matemáticas,  2018. Dirigió como: Tutor principal,   Persona(s) orientada(s):  Mateo Sanabria  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO,
    Areas:
    Ciencias Naturales -- Matemática -- Matemáticas Aplicadas,
  • Trabajos dirigidos/Tutorías - Trabajo de grado de maestría o especialidad clínica
  • HERNAN CAMILO ROCHA NINO, Estimating Formation Mechanisms and Degree Distributions in Mixed Attachment Networks  PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI  Estado: Tesis concluida  Maestría en Ingeniería,  2017. Dirigió como: Coturor/asesor,   Persona(s) orientada(s):  Jan Medina  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO , JORGE FINKE,
    Areas:
    Ciencias Naturales -- Matemática -- Estadísticas y Probabilidades (Investigación en Metodologías),
  • Trabajos dirigidos/Tutorías - Trabajo de grado de maestría o especialidad clínica
  • HERNAN CAMILO ROCHA NINO, Towards an Algorithmic Selection of Spreaders in Twitter  PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI  Estado: Tesis concluida  Maestría en Ingeniería,  2017. Dirigió como: Tutor principal,   Persona(s) orientada(s):  Arturo Duque Marón  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO , JORGE FINKE,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Trabajos dirigidos/Tutorías - Trabajo de grado de maestría o especialidad clínica
  • HERNAN CAMILO ROCHA NINO, Modelos de optimización del programa de intercambio de riñones con múltiples etapas  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis concluida  Maestría en Ingeniería Industrial,  2017. Dirigió como: Coturor/asesor,   Persona(s) orientada(s):  Edna Rocío Pérez Malaver  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO , VICTORIA EUGENIA OSPINA BECERRA , WILLIAM JAVIER GUERRERO RUEDA,
    Areas:
    Ingeniería y Tecnología -- Biotecnología Industrial -- Biotecnología Industrial,
  • Trabajos dirigidos/Tutorías - Trabajos de grado de pregrado
  • HERNAN CAMILO ROCHA NINO, EB2Python-Traducción automática de especificaciones Event-B en Rodin a Python  ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO  Estado: Tesis concluida  Ingeniería de Sistemas,  2018. Dirigió como: Tutor principal,   Persona(s) orientada(s):  Hernán Felipe Losada  Tutor(es)/Cotutor(es): HERNAN CAMILO ROCHA NINO , WILMER GARZON ALFONSO,
    Areas:
    Ingeniería y Tecnología -- Ingenierías Eléctrica, Electrónica e Informática -- Ingeniería de Sistemas y Comunicaciones,
     

    Jurado en comités de evaluación

  • Datos complementarios - Jurado/Comisiones evaluadoras de trabajo de grado - Doctorado
  • HERNAN CAMILO ROCHA NINO, Titulo: Opinions, lies and knowledge. An algebraic approach to mobility of information and processes Tipo de trabajo presentado: Trabajo de grado/tesis en:  Ecole Polytechnique  programa académico PhD in Computer Science  Nombre del orientado: Yamil Samil Perchy  
  • Datos complementarios - Jurado/Comisiones evaluadoras de trabajo de grado - Doctorado
  • HERNAN CAMILO ROCHA NINO, Titulo: AN APPROACH TO FORMAL MODELING OF GRID COMPUTING Tipo de trabajo presentado: Trabajo de grado/tesis en:  UNIVERSIDAD DEL VALLE  programa académico Doctorado en Ingeniería  Nombre del orientado: Carlos Alberto Ramírez Restrepo  
  • Datos complementarios - Jurado/Comisiones evaluadoras de trabajo de grado - Pregrado
  • HERNAN CAMILO ROCHA NINO, Titulo: CRE2+: USO DE LA LIBRERÍA DE RESTRICCIONES GECODE PARA UNA RE IMPLEMENTACIÓN MAS EFICIENTE Y USABLE DEL MODELO DE RESTRICCIONES CRE2 Tipo de trabajo presentado: Proyecto de grado/Tesis en:  PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI  programa académico Ingeniería de Sistemas y Computación  Nombre del orientado: ALEJANDRO CARDONA RECALDE; DANIEL MONTENEGRO CORDERO  

    Par evaluador

    Ámbito: Nacional  Par evaluador de: Proyecto  Institución: Ministerio de Ciencia, Tecnología e Innovación.,  2010,  Diciembre  
    Ámbito: Internacional  Par evaluador de: Material para publicación científica  Revista: Journal of Logical and Algebraic Methods in Programming,  2015,  Mayo  
    Ámbito: Internacional  Par evaluador de: Material para publicación científica  Revista: Science of Computer Programming,  2013,  Diciembre  
    Ámbito: Nacional  Par evaluador de: Proyecto  Institución: Ministerio de Ciencia, Tecnología e Innovación.,  2011,  Abril  
    Ámbito: Internacional  Par evaluador de: Material para publicación científica  Revista: Journal of Automated Reasoning,  2016,  Febrero  
    Ámbito: Internacional  Par evaluador de: Material para publicación científica  Revista: Science of Computer Programming,  2015,  Mayo  
    Ámbito: Nacional  Par evaluador de: Proyecto  Institución: Ministerio de Ciencia, Tecnología e Innovación.,  2015,  Febrero  

    Eventos científicos

    1 Nombre del evento: 10th Computing Colombian Conference (10CCC)  Tipo de evento: Congreso  Ámbito: Nacional  Realizado el:2015-09-22 00:00:00.0,  2015-09-25 00:00:00.0   en BOGOTÁ, D.C.   - Universidad de los Andes  
    Productos asociados
    • Nombre del producto:Executable Calculational Specifications Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Executable Calculational Specifications Tipo de producto:Producción técnica - Presentación de trabajo - Conferencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: FRANCISCO JOSE CHAVES ALONSO Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente , Organizador , Ponente
    2 Nombre del evento: 4th Conference on Algebra and Coalgebra in Computer Science (CALCO2011)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2011-08-23 00:00:00.0,  2011-08-27 00:00:00.0   en Winchester   - Winchester, Inglaterra  
    Productos asociados
    • Nombre del producto:Proving Safety Properties of Rewrite Theories Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Proving Safety Properties of Rewrite Theories Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    3 Nombre del evento: 10th Computing Colombian Conference (10CCC)  Tipo de evento: Congreso  Ámbito: Nacional  Realizado el:2015-09-22 00:00:00.0,  2015-09-26 00:00:00.0   en BOGOTÁ, D.C.   - Universidad de los Andes  
    Productos asociados
    • Nombre del producto:Formal verification of safety properties for a cache coherence protocol Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Formal Verification of Safety Properties for a Cache Coherence Protocol Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente , Organizador , Ponente
    • Nombre: SERGIO STEVEN RAMIREZ RICO Rol en el evento: Ponente
    4 Nombre del evento: Specification, Algebra, and Software; A Festschrift Symposium in Honor of Kokichi Futatsugi (SAS2014)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2014-04-10 00:00:00.0,  2014-04-12 00:00:00.0   en Kanazawa   - Japan Advance Institute of Science and Technology  
    Productos asociados
    • Nombre del producto:Mechanical Analysis of Reliable Communication Using the Maude Invariant Analyzer Tool in the Alternating Bit Protocol Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Mechanical Analysis of Reliable Communication Using the Maude Invariant Analyzer Tool in the Alternating Bit Protocol Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    5 Nombre del evento: Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday (FCT)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2011-11-24 00:00:00.0,  2011-11-26 00:00:00.0   en Menlo Park   - Menlo Park, Estados Unidos  
    Productos asociados
    • Nombre del producto:Towards a Maude Formal Environment Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Towards a Maude Formal Environment Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    6 Nombre del evento: 9th International Workshop on Rewriting Logic and its Applications (WRLA12)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2012-03-15 00:00:00.0,  2012-03-17 00:00:00.0   en Tallinn   - Tallinn, Estonia  
    Productos asociados
    • Nombre del producto:Order-Sorted Equality Enrichments Modulo Axioms Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Order-Sorted Equality Enrichments Modulo Axioms Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    7 Nombre del evento: 4th Conference on Algebra and Coalgebra in Computer Science (CALCO-Tools2011)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2011-08-23 00:00:00.0,  2011-08-27 00:00:00.0   en Winchester   - Winchester, Inglaterra  
    Productos asociados
    • Nombre del producto:Tool Interoperability in the Maude Formal Environment Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Tool Interoperability in the Maude Formal Environment Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    8 Nombre del evento: 9th International Conference on Integrated Formal Methods (iFM2012)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2012-06-18 00:00:00.0,  2012-06-23 00:00:00.0   en Pisa   - Pisa, Italia  
    Productos asociados
    • Nombre del producto:A Formal Interactive Verification Environment for the Plan Execution Interchange Language Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:A Formal Interactive Verification Environment for the Plan Execution Interchange Language Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    9 Nombre del evento: 17th International Conference on Logic Programming, Artificial Intelligence and Reasoning (LPAR17)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2010-10-26 00:00:00.0,  2010-10-30 00:00:00.0   en Yogyakarta   - Yogyakarta, Indonesia  
    Productos asociados
    • Nombre del producto:Constructors, Sufficient Completeness and Deadlock Freedom of Rewrite Theories Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Constructors, Sufficient Completeness and Deadlock Freedom of Rewrite Theories Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    10 Nombre del evento: 14th Brazilian Symposium on Formal Methods (SBMF2011)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2011-09-13 00:00:00.0,  2011-09-17 00:00:00.0   en São Paulo   - Sao Paulo, Brasil  
    Productos asociados
    • Nombre del producto:Simulation and Verification of Synchronous Set Relations in Rewriting Logic Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Simulation and Verification of Synchronous Set Relations in Rewriting Logic Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    11 Nombre del evento: Congreso Colombiano de Computación (8CCC)  Tipo de evento: Congreso  Ámbito: Nacional  Realizado el:2013-08-28 00:00:00.0,  2013-08-31 00:00:00.0   en ARMENIA   - Armenia, Colombia  
    Productos asociados
    • Nombre del producto:Automatic Proof-Search Heuristics in the Maude Invariant Analyzer Tool Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Automatic Proof-Search Heuristics in the Maude Invariant Analyzer Tool Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    12 Nombre del evento: 10th International Workshop on Rewriting Techniques and Applications (WRLA2014)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2014-04-03 00:00:00.0,  2014-04-05 00:00:00.0   en Grennoble   - Grennoble, Francia  
    Productos asociados
    • Nombre del producto:Rewriting Modulo SMT and Open System Analysis Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Rewriting Modulo SMT and Open System Analysis Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:ESCUELA COLOMBIANA DE INGENIERIA JULIO GARAVITO Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    13 Nombre del evento: SEGUNDO CONGRESO COLOMBIANO DE COMPUTACION 2CCC  Tipo de evento: Congreso  Ámbito:   Realizado el:2007-01-01 00:00:00.0,    en BOGOTÁ, D.C.   -  
    Productos asociados
    • Nombre del producto:A Rewriting Decision Procedure for Dijkstra-Scholten¿s Syllogistic Logic with Complements Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente
    14 Nombre del evento: 6TH INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY BASED HIGHER EDUCATION AND TRAININNIG  Tipo de evento: Otro  Ámbito:   Realizado el:2005-01-01 00:00:00.0,    en SANTO DOMINGO   -  
    Productos asociados
    • Nombre del producto:Towards the Effective Use of Formal Logic in the Teaching of Discrete Math Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente
    15 Nombre del evento: IDEAS 2006 9O WORKSHOP IBEROAMERICANO DE INGENIERIA DE REQUISITOS Y AMBIENTES DE SOFTWARE  Tipo de evento: Otro  Ámbito:   Realizado el:2006-01-01 00:00:00.0,    en La Plata, Argentina   -  
    Productos asociados
    • Nombre del producto:Una Semántica de Ensamblaje y Composición de Servicios y Componentes Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente
    16 Nombre del evento: 10TH INTERNATIONAL CONFERENCE ON RELATIONAL METHODS IN COMPUTER SCIENCE/5TH INTERNATIONAL CONFERENCE ON APPLICATIONS OF KLEENE ALGEBRA  Tipo de evento: Otro  Ámbito:   Realizado el:2008-04-01 00:00:00.0,    en CALI   -  
    Productos asociados
    • Nombre del producto:Theorem Proving Modulo Based on Boolean Equational Procedures Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente
    17 Nombre del evento: 11th Computing Colombian Conference (11CCC)  Tipo de evento: Congreso  Ámbito: Nacional  Realizado el:2016-09-28 00:00:00.0,  2016-09-30 00:00:00.0   en POPAYÁN   - Fundación Universitaria de Popayán  
    Productos asociados
    • Nombre del producto:Library Management for PVS Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: MIGUEL ANGEL ROMERO GONZALEZ Rol en el evento: Ponente
    18 Nombre del evento: Latin American Symposium on Theory of Computation (in CLEI 2016)   Tipo de evento: Simposio  Ámbito: Internacional  Realizado el:2016-10-10 00:00:00.0,  2016-10-14 00:00:00.0   en Viña del mar   - Pontificia Universidad Católica de Valparaiso  
    Productos asociados
    • Nombre del producto:Double-spend Attack Models with Time Advantage for Bitcoin Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: CARLOS ANTONIO PINZON HENAO Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    19 Nombre del evento: Congreso Latino-Iberoamericano de Investigación Operativa CLAIO 2016  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2016-10-02 00:00:00.0,  2016-10-06 00:00:00.0   en Santiago   - Optimización de ciclos de intercambio voluntario de riñones con múltiples etapas y escenarios de falla usando programación entera mixta  
    Productos asociados
    • Nombre del producto:Optimización de ciclos de intercambio voluntario de riñones con múltiples etapas y escenarios de falla usando programación entera mixta Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: WILLIAM JAVIER GUERRERO RUEDA Rol en el evento: Ponente
    20 Nombre del evento: International SPIN Symposium on Model Checking of Software (SPIN 2017).  Tipo de evento: Simposio  Ámbito: Internacional  Realizado el:2017-07-13 00:00:00.0,  2017-07-14 00:00:00.0   en Santa Barbara   - University of California, Santa Barbara  
    Productos asociados
    • Nombre del producto:Verification-driven Development of ICAROUS Based on Automatic Reachability Analysis. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente , Ponente
    21 Nombre del evento: 8th International Conference on Complex Networks and Their Applications (COMPLEX NETWORKS 2019).  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2019-12-10 00:00:00.0,  2019-12-12 00:00:00.0   en Lisbon   -  
    Productos asociados
    • Nombre del producto:In-silico Gene Annotation Prediction Using the Co-expression Network Structure. Tipo de producto:Demás trabajos - Demás trabajos - Póster
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: JORGE FINKE Rol en el evento: Ponente
    • Nombre: MAURICIO ALBERTO QUIMBAYA GOMEZ Rol en el evento: Ponente
    • Nombre: MIGUEL ANGEL ROMERO GONZALEZ Rol en el evento: Ponente
    22 Nombre del evento: 8th International Conference on Complex Networks and Their Applications (COMPLEX NETWORKS 2019).  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2019-12-10 00:00:00.0,  2019-12-12 00:00:00.0   en Lisbon   -  
    Productos asociados
    • Nombre del producto:Spectral Evolution of Twitter Mention Networks. Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: JORGE FINKE Rol en el evento: Ponente
    • Nombre: MIGUEL ANGEL ROMERO GONZALEZ Rol en el evento: Ponente
    23 Nombre del evento: 13th International Workshop on Rewriting Logic and its Applications (WRLA 2020).  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2020-10-20 00:00:00.0,  2020-10-22 00:00:00.0   en Dublin   -  
    Productos asociados
    • Nombre del producto:Analysis of the Runtime Resource Provisioning of BPMN Processes Using Maude. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: FRANCISCO DURAN Rol en el evento: Ponente
    • Nombre: GWEN SALAUN Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    24 Nombre del evento: 23rd International Conference on Fundamental Approaches to Software Engineering (FASE 2020).  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2020-04-25 00:00:00.0,  2020-04-30 00:00:00.0   en Dublin   - Royal Marine Hotel  
    Productos asociados
    • Nombre del producto:Algorithmic Analysis of Blockchain Efficiency with Communication Delay. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: CARLOS ANTONIO PINZON HENAO Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: JORGE FINKE Rol en el evento: Ponente
    25 Nombre del evento: International SPIN Symposium on Model Checking of Software (SPIN 2017).  Tipo de evento: Simposio  Ámbito: Internacional  Realizado el:2017-07-13 00:00:00.0,  2017-07-14 00:00:00.0   en Santa Barbara   - University of California, Santa Barbara  
    Productos asociados
    • Nombre del producto:Verification-driven development of ICAROUS based on automatic reachability analysis: a preliminary case study. Tipo de producto:Producción técnica - Presentación de trabajo - Otro
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    26 Nombre del evento: 13th International Workshop on Rewriting Logic and its Applications (WRLA 2020).  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2020-10-20 00:00:00.0,  2020-10-22 00:00:00.0   en Dublin   -  
    Productos asociados
    • Nombre del producto:Verification of the IBOS Browser Security Properties in Reachability Logic. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: JOSE MESEGUER Rol en el evento: Ponente
    27 Nombre del evento: 17th International Conference Service-Oriented Computing (ICSOC 2019).  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2019-10-28 00:00:00.0,  2019-10-31 00:00:00.0   en Toulouse   -  
    Productos asociados
    • Nombre del producto:Analysis of Resource Allocation of BPMN Processes. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: FRANCISCO DURAN Rol en el evento: Ponente
    • Nombre: GWEN SALAUN Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    28 Nombre del evento: Logic, Rewriting, and Concurrency (LRC2015)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2015-09-23 00:00:00.0,  2015-09-25 00:00:00.0   en Urbana, IL   - University of Illinois at Urbana-Champaign, USA.  
    Productos asociados
    • Nombre del producto:The Formal System of Dijkstra and Scholten Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:The Formal System of Dijkstra and Scholten Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    29 Nombre del evento: 14th International Conference on Formal Aspects of Component Software (FACS 2017)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2017-10-10 00:00:00.0,  2017-10-13 00:00:00.0   en Braga   - D. Diogo Museum of Archeology and Arts  
    Productos asociados
    • Nombre del producto:Guarded Terms for Rewriting Modulo SMT Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Guarded Terms for Rewriting Modulo SMT Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    30 Nombre del evento: STAF Workshops 2018 (STAF 2018)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2018-04-11 00:00:00.0,  2018-04-13 00:00:00.0   en Toulouse   - Four Points by Sheraton San Rafael, CA  
    Productos asociados
    • Nombre del producto:Computing the Parallelism Degree of Timed BPMN Processes. Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Computing the Parallelism Degree of Timed BPMN Processes. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: FRANCISCO DURAN Rol en el evento: Ponente
    • Nombre: GWEN SALAUN Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    31 Nombre del evento: 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2018-04-14 00:00:00.0,  2018-04-14 00:00:00.0   en Thessaloniki   -  
    Productos asociados
    • Nombre del producto:Proving Structural Properties of Sequent Systems in Rewriting Logic Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Proving Structural Properties of Sequent Systems in Rewriting Logic Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: CARLOS ALBERTO OLARTE VEGA Rol en el evento: Ponente
    • Nombre: ELAINE GOUVEA PIMENTEL Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    32 Nombre del evento: 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2018-04-14 00:00:00.0,  2018-04-15 00:00:00.0   en Thessaloniki   -  
    Productos asociados
    • Nombre del producto:Real-Time Rewriting Logic Semantics for Spatial Concurrent Constraint Programming. Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Real-Time Rewriting Logic Semantics for Spatial Concurrent Constraint Programming. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: FRANK VALENCIA Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: MIGUEL ANGEL ROMERO GONZALEZ Rol en el evento: Ponente
    • Nombre: SERGIO STEVEN RAMIREZ RICO Rol en el evento: Ponente
    33 Nombre del evento: 10th NASA Formal Methods Symposium (NFM 2018)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2018-04-17 00:00:00.0,  2018-04-19 00:00:00.0   en Hampton   - Newport News Marriott at City Center  
    Productos asociados
    • Nombre del producto:Symbolic Execution and Reachability Analysis using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Symbolic Execution and Reachability Analysis using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: MIGUEL ANGEL ROMERO GONZALEZ Rol en el evento: Ponente
    34 Nombre del evento: 12th Colombian Conference on Computing (12CCC)  Tipo de evento: Congreso  Ámbito: Nacional  Realizado el:2017-09-19 00:00:00.0,  2017-09-22 00:00:00.0   en CALI   - Universidad Autónoma de Occidente  
    Productos asociados
    • Nombre del producto:Axiomatic Set Theory à la Dijkstra and Scholten Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Axiomatic Set Theory à la Dijkstra and Scholten Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: BERNARDA ALDANA GOMEZ Rol en el evento: Ponente
    • Nombre: ERNESTO ACOSTA GEMPELER Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: JAIME ALEJANDRO BOHORQUEZ VILLAMIZAR Rol en el evento: Ponente
    35 Nombre del evento: 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2018-04-14 00:00:00.0,  2018-04-15 00:00:00.0   en Thessaloniki   -  
    Productos asociados
    • Nombre del producto:Proving Ground Confluence of Equational Specifications Modulo Axioms. Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Proving Ground Confluence of Equational Specifications Modulo Axioms. Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: FRANCISCO DURAN Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    • Nombre: JOSE MESEGUER Rol en el evento: Ponente
    36 Nombre del evento: 12th International Workshop on Rewriting Logic and its Applications (WRLA 2018)  Tipo de evento: Congreso  Ámbito: Internacional  Realizado el:2018-04-14 00:00:00.0,  2018-04-15 00:00:00.0   en Thessaloniki   -  
    Productos asociados
    • Nombre del producto:Symbolic Specification and Verification of Data-Aware BPMN Processes Using Rewriting Modulo SMT Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Symbolic Specification and Verification of Data-Aware BPMN Processes Using Rewriting Modulo SMT Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: FRANCISCO DURAN Rol en el evento: Ponente
    • Nombre: GWEN SALAUN Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    37 Nombre del evento: 12th Colombian Conference on Computing (12CCC)  Tipo de evento: Congreso  Ámbito: Nacional  Realizado el:2017-09-19 00:00:00.0,  2017-09-22 00:00:00.0   en CALI   - Universidad Autónoma de Occidente  
    Productos asociados
    • Nombre del producto:Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots Tipo de producto:Producción bibliográfica - Trabajos en eventos (Capítulos de memoria) - Completo
    • Nombre del producto:Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots Tipo de producto:Producción técnica - Presentación de trabajo - Ponencia
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HECTOR CADAVID RENGIFO Rol en el evento: Ponente
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Ponente
    38 Nombre del evento: 10th International School on Rewriting  Tipo de evento: Seminario  Ámbito: Internacional  Realizado el:2018-07-30 00:00:00.0,  2018-08-03 00:00:00.0   en CALI   - Pontificia Universidad Javeriana Cali  
    Instituciones asociadas
    • Nombre de la institución:PONTIFICIA UNIVERSIDAD JAVERIANA - PUJ - SEDE CALI Tipo de vinculaciónPatrocinadora
    Participantes
    • Nombre: HERNAN CAMILO ROCHA NINO Rol en el evento: Asistente , Organizador , Ponente

    Redes de conocimiento especializado

    Nombre de la red Colombian Collegiate Programming League (CCPL)  Tipo de redVirtual,  Creada el:2014-01-01 00:00:00.0,    en CALI   con participantes 
    Nombre de la red PacificTic  Tipo de redReal,  Creada el:2020-02-01 00:00:00.0,    en CALI   con participantes 

    Estrategias pedagógicas para el fomento a la CTI

    Nombre de la estrategia Semillero de Investigación en Algoritmos y Programación  Inicio enEnero - 2017,  Finalizó en :Diciembre - 2017, 
    Nombre de la estrategia Semillero Grupo de Algoritmia  Inicio enEnero - 2014,  Finalizó en :Diciembre - 2016, 
    Nombre de la estrategia Semillero Glecix  Inicio enEnero - 2013,  Finalizó en :Diciembre - 2016, 

    Artículos

  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, "A Rewriting Decision Procedure for Dijkstra-Scholten's Syllogistic Logic with Complements" . En: Colombia 
    Revista Colombiana De Computación  ISSN: 1657-2831  ed: Universidad Autónoma de Bucaramanga - Oficina de Publicaciones
    v.8 fasc.2 p.1 - 16 ,2007,  DOI: 10.13140/2.1.2451.5361
    Palabras:
    rewriting logic, Syllogistic Logic, Propositional Logic, decision procedure, Boolean algebra, Formal Methods,
    Sectores:
    Desarrollo de programas (software) y prestación de servicios en informática, Desarrollo de programas (software) y prestación de servicios en informática - Otro,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, "The Formal System of Dijkstra and Scholten" . En: Estados Unidos 
    Lecture Notes In Computer Science  ISSN: 1611-3349  ed: Springer-Verlag GmbH and Co. KG
    v.9200 fasc. p.580 - 597 ,2015,  DOI: 10.1007/978-3-319-23165-5_27
    Palabras:
    logic, rewriting logic, theorem proving, Boolean algebra, Maude, propositional logic, first order logic, decision procedure,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • RAUL GUTIERREZ, JOSE MESEGUER, HERNAN CAMILO ROCHA NINO, "Order-sorted equality enrichments modulo axioms" . En: Estados Unidos 
    Science of Computer Programming  ISSN: 0167-6423  ed: Elsevier Science Bv
    v.99 fasc.N/A p.235 - 261 ,2015,  DOI: 10.1016/j.scico.2014.07.003
    Palabras:
    algebra, decision procedure, symbol manipulation, theorem proving, logic,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, CESAR MUNOZ, "Rewriting Modulo SMT and Open System Analysis" . En: Francia 
    Lecture Notes In Computer Science  ISSN: 1611-3349  ed: Springer-Verlag GmbH and Co. KG
    v.8663 fasc.N/A p.247 - 262 ,2014,  DOI: 10.1007/978-3-319-12904-4_14
    Palabras:
    Maude, logic, rewriting logic, formal environment, invariants, safety properties, symbol manipulation, symbolic reachability, theorem proving, satisfiability modulo theories (SMT),
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, "Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool" . En: Japón 
    Lecture Notes In Computer Science  ISSN: 1611-3349  ed: Springer-Verlag GmbH and Co. KG
    v.8373 fasc.N/A p.603 - 629 ,2014,  DOI: 10.1007/978-3-642-54624-2_30
    Palabras:
    logic, Maude Invariant Analyzer - InvA, Maude, rewriting logic, invariants, safety properties, symbol manipulation, symbolic reachability, theorem proving,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, CESAR MUNOZ, "Synchronous set relations in rewriting logic" . En: Estados Unidos 
    Science of Computer Programming  ISSN: 0167-6423  ed: Elsevier Science Bv
    v.92 fasc.B p.211 - 228 ,2014,  DOI: 10.1016/j.scico.2013.07.008
    Palabras:
    Maude, rewriting logic, invariants, open source software development, plan execution, set relations, synchronous languages, theorem proving,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, CESAR MUNOZ, GILLES DOWEK, "Rewriting Logic Semantics of a Plan Execution Language" . En: Estados Unidos 
    Electronic Notes in Theoretical Computer Science  ISSN: 1571-0661  ed: Elsevier Bv
    v.18 fasc.N/A p.77 - 91 ,2010,  DOI: 10.4204/EPTCS.18.6
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, CESAR MUNOZ, GILLES DOWEK, "A Formal Library of Set Relations and its Application to Synchronous Languages" . En: Estados Unidos 
    Theoretical Computer Science  ISSN: 0304-3975  ed: Elsevier Science Bv
    v.412 fasc.37 p.4853 - 4866 ,2011,  DOI: 10.1016/j.tcs.2011.01.027
    Palabras:
    set relations, synchronous languages, small-step semantics, rewriting logic semantics, plan execution,
    Sectores:
    Aeronáutica y espacio,
  • Producción bibliográfica - Artículo - Corto (Resumen)
  • FRANCISCO DURAN, HERNAN CAMILO ROCHA NINO, JOSE MARIA ALVAREZ, "Tool Interoperability in the Maude Formal Environment" . En: Inglaterra 
    Lecture Notes in Computer Science  ISSN: 0302-9743  ed: Springer-Verlag London Ltd.
    v.6859 fasc.N/A p.400 - 406 ,2011,  DOI: 10.1007/978-3-642-22944-2_30
    Palabras:
    rewriting logic, open source software development,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, HECTOR CADAVID RENGIFO, CESAR MUNOZ, RADU SIMINICEANU, "A Formal Interactive Verification Environment for the Plan Execution Interchange Language" . En: Italia 
    Lecture Notes in Computer Science  ISSN: 0302-9743  ed: Springer-Verlag London Ltd.
    v.7321 fasc.N/A p.343 - 357 ,2012,  DOI: 10.1007/978-3-642-30729-4_24
    Palabras:
    PLEXIL-Plan Execution Interchange Language, formal environment, plan execution, rewriting logic, synchronous languages, open source software development,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, "Proving Safety Properties of Rewrite Theories" . En: Inglaterra 
    Lecture Notes in Computer Science  ISSN: 0302-9743  ed: Springer-Verlag London Ltd.
    v.6859 fasc.N/A p.314 - 328 ,2011,  DOI: 10.1007/978-3-642-22944-2_22
    Palabras:
    safety properties, invariants, theorem proving, open source software development,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, CESAR MUNOZ, "Simulation and Verification of Synchronous Set Relations in Rewriting Logic" . En: Brasil 
    Lecture Notes in Computer Science  ISSN: 0302-9743  ed: Springer-Verlag London Ltd.
    v.7021 fasc.N/A p.60 - 75 ,2011,  DOI: 10.1007/978-3-642-25032-3_5
    Palabras:
    synchronous languages, set relations, rewriting logic, rewriting logic semantics, open source software development,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, "Constructors, Sufficient Completeness and Deadlock Freedom of Rewrite Theories" . En: Indonesia 
    Lecture Notes in Computer Science  ISSN: 0302-9743  ed: Springer-Verlag London Ltd.
    v.6397 fasc.N/A p.594 - 609 ,2010,  DOI: 10.1007/978-3-642-16242-8_42
    Palabras:
    rewriting logic, propositional tree automata, deadlock freedom, sufficient completeness, decision procedure, symbol manipulation,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • RAUL GUTIERREZ, JOSE MESEGUER, HERNAN CAMILO ROCHA NINO, "Order-Sorted Equality Enrichments Modulo Axioms" . En: Estonia 
    Lecture Notes in Computer Science  ISSN: 0302-9743  ed: Springer-Verlag London Ltd.
    v.7571 fasc.N/A p.162 - 181 ,2012,  DOI: 10.1007/978-3-642-34005-5_9
    Palabras:
    algebra, rewriting logic, symbol manipulation, theorem proving,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • FRANCISCO DURAN, HERNAN CAMILO ROCHA NINO, JOSE MARIA ALVAREZ, "Towards a Maude Formal Environment" . En: Estados Unidos 
    Lecture Notes in Computer Science  ISSN: 0302-9743  ed: Springer-Verlag London Ltd.
    v.7000 fasc.N/A p.329 - 351 ,2011,  DOI: 10.1007/978-3-642-24933-4_17
    Palabras:
    rewriting logic, Maude, open source software development,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, "Automatic Proof-Search Heuristics in the Maude Invariant Analyzer Tool" . En: Colombia 
    Revista Colombiana De Computación  ISSN: 1657-2831  ed: Universidad Autónoma de Bucaramanga - Oficina de Publicaciones
    v.14 fasc.2 p.1 - 6 ,2013,  DOI: 
    Palabras:
    Formal Methods, logic, Maude, Maude Invariant Analyzer - InvA, rewriting logic, decision procedure, invariants, safety properties, symbolic reachability, theorem proving,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • CARLOS ANTONIO PINZON HENAO, HERNAN CAMILO ROCHA NINO, "Double-spend attack models with time advantange for Bitcoin" . En: Países Bajos 
    Electronic Notes in Theoretical Computer Science  ISSN: 1571-0661  ed: Elsevier Bv
    v.329 fasc.N/A p.79 - 103 ,2016,  DOI: 10.1016/j.entcs.2016.12.006
    Palabras:
    algorithms, empirical networks, graph theory, networks,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, CESAR MUNOZ, "Rewriting modulo SMT and open system analysis" . En: Países Bajos 
    Journal of Logical and Algebraic Methods in Programming  ISSN: 2352-2208  ed: Elsevier Bv
    v.86 fasc.1 p.269 - 297 ,2017,  DOI: 10.1016/j.jlamp.2016.10.001
    Palabras:
    algebra, Formal Methods, logic, Métodos Formales, rewriting logic, symbolic reachability, satisfiability modulo theories (SMT),
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • JORGE FINKE, MIGUEL ANGEL ROMERO GONZALEZ, HERNAN CAMILO ROCHA NINO, LUIS EDUARDO TOBON LLANO, "Spectral Evolution with Approximated Eigenvalue Trajectories for Link Prediction" . En: Austria 
    Social Network Analysis and Mining  ISSN: 1869-5450  ed: Springer-Verlag Wien
    v.10 fasc.60 p.1 - 10 ,2020,  DOI: 10.1007/s13278-020-00674-3
    Palabras:
    algorithms, dynamic networks, empirical networks, graph theory, networks,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, "Theorem Proving Modulo Based on Boolean Equational Procedures" . En: Alemania 
    Lecture Notes In Computer Science  ISSN: 1611-3349  ed: Springer-Verlag GmbH and Co. KG
    v.4988 fasc.N/A p.337 - 351 ,2008,  DOI: 10.1007/978-3-540-78913-0_25
    Palabras:
    theorem proving, rewriting logic, Boolean algebra, decision procedure,
    Sectores:
    Desarrollo de programas (software) y prestación de servicios en informática - Desarrollo de programas (software),
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • FRANCISCO DURAN, JOSE MESEGUER, HERNAN CAMILO ROCHA NINO, "Ground confluence of order-sorted conditional specifications modulo axioms" . En: Países Bajos 
    Journal of Logical and Algebraic Methods in Programming  ISSN: 2352-2208  ed: Elsevier Bv
    v.111 fasc.100513 p.1 - 117 ,2020,  DOI: 10.1016/j.jlamp.2019.100513
    Palabras:
    algebra, logic, Métodos Formales, rewriting logic, symbolic reachability, theorem proving,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • HERNAN CAMILO ROCHA NINO, FRANCISCO DURAN, GWEN SALAUN, "A rewriting logic approach to resource allocation analysis in business process models" . En: Países Bajos 
    Science of Computer Programming  ISSN: 0167-6423  ed: Elsevier Science Bv
    v.178 fasc.N/A p.1 - 15 ,2019,  DOI: 10.1016/j.scico.2019.102303
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • KYUNGMIN BAE, HERNAN CAMILO ROCHA NINO, "Symbolic state space reduction with guarded terms for rewriting modulo SMT" . En: Países Bajos 
    Science of Computer Programming  ISSN: 0167-6423  ed: Elsevier Science Bv
    v.178 fasc. p.20 - 42 ,2019,  DOI: 10.1016/j.scico.2019.03.006
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • JAN ALEJANDRO MEDINA LOPEZ, JORGE FINKE, HERNAN CAMILO ROCHA NINO, "Estimating formation mechanisms and degree distributions in mixed attachment networks" . En: Inglaterra 
    Journal of Physics A: Mathematical and Theoretical  ISSN: 1751-8113  ed: Institute of Physics Publishing (IOP)
    v.52 fasc.9 p.1 - 21 ,2019,  DOI: 10.1088/1751-8121/aaffeb
    Palabras:
    dynamic networks, empirical networks, graph theory, algorithms, networks,
  • Producción bibliográfica - Artículo - Publicado en revista especializada
  • FRANCISCO DURAN, HERNAN CAMILO ROCHA NINO, GWEN SALAUN, "Stochastic analysis of BPMN with time in rewriting logic" . En: Países Bajos 
    Science of Computer Programming  ISSN: 0167-6423  ed: Elsevier Science Bv
    v.168 fasc.NA p.1 - 17 ,2018,  DOI: 10.1016/j.scico.2018.08.007
    Palabras:
    Maude, rewriting logic,

    Capitulos de libro

  • Tipo: Capítulo de libro
    FRANCISCO DURAN, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    GWEN SALAUN, "Computing the Parallelism Degree of Timed BPMN Processes" Software Technologies: Applications and Foundations. STAF 2018 . En: Estados Unidos  ISBN: 978-3-030-04770-2  ed: Springer Publishing Company, Inc. , v. , p.320 - 335  ,2018
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    FRANCISCO DURAN, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    GWEN SALAUN, "Symbolic Specification and Verification of Data-Aware BPMN Processes Using Rewriting Modulo SMT" Rewriting Logic and Its Applications. WRLA 2018. Lecture Notes in Computer Science . En: Estados Unidos  ISBN: 978-3-319-99839-8  ed: Springer Publishing Company, Inc. , v. , p.76 - 97  ,2018
    Palabras:
    formal environment, Formal Methods, Maude, rewriting logic, Software Testing,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    SERGIO STEVEN RAMIREZ RICO, Tipo: Capítulo de libro
    MIGUEL ANGEL ROMERO GONZALEZ, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    FRANK VALENCIA, "Real-Time Rewriting Logic Semantics for Spatial Concurrent Constraint Programming" Rewriting Logic and Its Applications. WRLA 2018. Lecture Notes in Computer Science . En: Estados Unidos  ISBN: 978-3-319-99839-8  ed: Springer Publishing Company, Inc. , v. , p.226 - 244  ,2018
  • Tipo: Capítulo de libro
    CARLOS ALBERTO OLARTE VEGA, Tipo: Capítulo de libro
    ELAINE GOUVEA PIMENTEL, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Proving Structural Properties of Sequent Systems in Rewriting Logic" Rewriting Logic and Its Applications. WRLA 2018. Lecture Notes in Computer Science . En: Estados Unidos  ISBN: 978-3-319-99839-8  ed: Springer Publishing Company, Inc. , v. , p.115 - 135  ,2018
  • Tipo: Capítulo de libro
    FRANCISCO DURAN, Tipo: Capítulo de libro
    JOSE MESEGUER, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Proving Ground Confluence of Equational Specifications Modulo Axioms" Rewriting Logic and Its Applications. WRLA 2018. Lecture Notes in Computer Science . En: Estados Unidos  ISBN: 978-3-319-99839-8  ed: Springer Publishing Company, Inc. , v. , p.184 - 204  ,2018
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    MIGUEL ANGEL ROMERO GONZALEZ, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Symbolic Execution and Reachability Analysis Using Rewriting Modulo SMT for Spatial Concurrent Constraint Systems with Extrusion" NASA Formal Methods. NFM 2018. Lecture Notes in Computer Science . En: Estados Unidos  ISBN: 978-3-319-77934-8  ed: Springer Publishing Company, Inc. , v. , p.435 - 451  ,2018
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    JOSE MESEGUER, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Theorem Proving Modulo Based on Boolean Equational Procedures" Lecture Notes In Computer Science . En: Colombia  ISBN: 978-3-540-78912-3  ed: Springer Publishing Company, Inc. , v. , p.337 - 351  ,2008
    Palabras:
    theorem proving, rewriting logic, Boolean algebra, decision procedure,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Analysis of Resource Allocation of BPMN Processes" Lecture Notes in Computer Science . En: Países Bajos  ISBN: 978-3-030-33701-8  ed: Springer-Verlag Berlin/Heidelberg , v. , p.452 - 457  11895 ,2019
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    MIGUEL ANGEL ROMERO GONZALEZ, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    JORGE FINKE, "Spectral Evolution of Twitter Mention Networks" Complex Networks and Their Applications VIII . En: Países Bajos  ISBN: 978-3-030-36686-5  ed: Springer-Verlag Berlin/Heidelberg , v. , p.532 - 542  881 ,2019
  • Tipo: Capítulo de libro
    MIGUEL ANGEL ROMERO GONZALEZ, Tipo: Capítulo de libro
    JORGE FINKE, Tipo: Capítulo de libro
    MAURICIO ALBERTO QUIMBAYA GOMEZ, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "In-silico Gene Annotation Prediction Using the Co-expression Network Structure" Complex Networks and Their Applications VIII . En: Países Bajos  ISBN: 978-3-030-36686-5  ed: Springer-Verlag Berlin/Heidelberg , v. , p.802 - 812  882 ,2019
  • Tipo: Capítulo de libro
    KYUNGMIN BAE, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Guarded Terms for Rewriting Modulo SMT " Formal Aspects of Component Software . En: Estados Unidos  ISBN: 978-3-319-68033-0  ed: Springer Publishing Company, Inc. , v. , p.78 - 97  10487 ,2017
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    BERNARDA ALDANA GOMEZ, Tipo: Capítulo de libro
    JAIME ALEJANDRO BOHORQUEZ, Tipo: Capítulo de libro
    ERNESTO ACOSTA GEMPELER, "Axiomatic Set Theory à la Dijkstra and Scholten" Advances in Computing . En: Estados Unidos  ISBN: 978-3-319-66561-0  ed: Springer Publishing Company, Inc. , v. , p.775 - 791  ,2017
    Areas:
    Ciencias Naturales -- Matemática -- Matemáticas Puras,
  • Tipo: Capítulo de libro
    HECTOR CADAVID RENGIFO, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Reliable Control Architecture with PLEXIL and ROS for Autonomous Wheeled Robots" Advances in Computing . En: Estados Unidos  ISBN: 978-3-319-66561-0  ed: Springer Publishing Company, Inc. , v. , p.611 - 626  N/A ,2017
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    FRANCISCO DURAN, Tipo: Capítulo de libro
    JOSE MARIA ALVAREZ, "Towards a Maude Formal Environment" Formal Modeling: Actors, Open Systems, Biological Systems . En: Estados Unidos  ISBN: 978-3-642-24932-7  ed: Springer Publishing Company, Inc. , v. , p.329 - 351  ,2011
    Palabras:
    rewriting logic, Maude, open source software development,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    RAUL GUTIERREZ, Tipo: Capítulo de libro
    JOSE MESEGUER, "Order-Sorted Equality Enrichments Modulo Axioms " Rewriting Logic and Its Applications . En: Estados Unidos  ISBN: 978-3-642-34004-8  ed: Springer Publishing Company, Inc. , v. , p.162 - 181  ,2012
    Palabras:
    algebra, rewriting logic, symbol manipulation, theorem proving,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    JOSE MESEGUER, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Constructors, Sufficient Completeness and Deadlock Freedom of Rewrite Theories " Logic for Programming, Artificial Intelligence, and Reasoning . En: Estados Unidos  ISBN: 978-3-642-16241-1  ed: Springer Publishing Company, Inc. , v. , p.594 - 609  ,2010
    Palabras:
    rewriting logic, propositional tree automata, deadlock freedom, sufficient completeness, decision procedure, symbol manipulation,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    CESAR MUNOZ, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Simulation and Verification of Synchronous Set Relations in Rewriting Logic " Formal Methods, Foundations and Applications . En: Estados Unidos  ISBN: 978-3-642-25031-6  ed: Springer Publishing Company, Inc. , v. , p.60 - 75  ,2011
    Palabras:
    synchronous languages, set relations, rewriting logic, rewriting logic semantics, open source software development,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    FRANCISCO DURAN, Tipo: Capítulo de libro
    JOSE MARIA ALVAREZ, "Tool Interoperability in the Maude Formal Environment" Algebra and Coalgebra in Computer Science . En: Estados Unidos  ISBN: 978-3-642-22943-5  ed: Springer Publishing Company, Inc. , v. , p.400 - 406  ,2011
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    JOSE MESEGUER, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Proving Safety Properties of Rewrite Theories" Algebra and Coalgebra in Computer Science . En: Estados Unidos  ISBN: 978-3-642-22943-5  ed: Springer Publishing Company, Inc. , v. , p.314 - 328  ,2011
    Palabras:
    safety properties, invariants, theorem proving, open source software development,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    HECTOR CADAVID RENGIFO, Tipo: Capítulo de libro
    CESAR MUNOZ, Tipo: Capítulo de libro
    RADU SIMINICEANU, "A Formal Interactive Verification Environment for the Plan Execution Interchange Language " Integrated Formal Methods . En: Estados Unidos  ISBN: 978-3-642-30728-7  ed: Springer Publishing Company, Inc. , v. , p.343 - 357  ,2012
    Palabras:
    PLEXIL-Plan Execution Interchange Language, formal environment, plan execution, rewriting logic, synchronous languages, open source software development,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    JOSE MESEGUER, Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool " Specification, Algebra, and Software . En: Estados Unidos  ISBN: 978-3-642-54623-5  ed: Springer Publishing Company, Inc. , v. , p.603 - 629  ,2014
    Palabras:
    logic, Maude Invariant Analyzer - InvA, Maude, rewriting logic, invariants, safety properties, symbol manipulation, symbolic reachability, theorem proving,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, Tipo: Capítulo de libro
    JOSE MESEGUER, Tipo: Capítulo de libro
    CESAR MUNOZ, "Rewriting Modulo SMT and Open System Analysis" Rewriting Logic and Its Applications . En: Estados Unidos  ISBN: 978-3-319-12903-7  ed: Springer Publishing Company, Inc. , v. , p.247 - 262  ,2014
    Palabras:
    Maude, logic, rewriting logic, formal environment, invariants, safety properties, symbol manipulation, symbolic reachability, theorem proving, satisfiability modulo theories (SMT),
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación, Ciencias Naturales -- Matemática -- Matemáticas Puras,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "The Formal System of Dijkstra and Scholten" Logic, Rewriting, and Concurrency . En: Estados Unidos  ISBN: 978-3-319-23164-8  ed: Springer Publishing Company, Inc. , v. , p.580 - 597  ,2015
    Palabras:
    logic, rewriting logic, theorem proving, Boolean algebra, Maude, propositional logic, first order logic, decision procedure,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Analysis of the Runtime Resource Provisioning of BPMN Processes Using Maude" Rewriting Logic and Its Applications . En: Suiza  ISBN: 978-3-030-63594-7  ed: Springer Publishing Company, Inc. , v. , p.38 - 56  12328 ,2020
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Verification of the IBOS Browser Security Properties in Reachability Logic" Rewriting Logic and Its Applications . En: Suiza  ISBN: 978-3-030-63594-7  ed: Springer Publishing Company, Inc. , v. , p.179 - 196  12328 ,2020
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Algorithmic Analysis of Blockchain Efficiency with Communication Delay" Fundamental Approaches to Software Engineering . En: Suiza  ISBN: 978-3-030-45233-9  ed: Springer Publishing Company, Inc. , v. , p.400 - 419  12076 ,2020
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Automatic proof-search heuristics in the Maude invariant analyzer tool" Proceedings Of Computing Colombian Conference (8ccc), 2013 8th . En: Estados Unidos  ISBN: 978-1-4799-1054-0  ed: IEEE Publications , v. , p.1 - 6  ,2013
    Palabras:
    Maude, Maude Invariant Analyzer - InvA, decision procedure, invariants, open source software development, safety properties, satisfiability modulo theories (SMT), symbol manipulation, symbolic reachability, theorem proving, rewriting logic,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Tipo: Capítulo de libro
    HERNAN CAMILO ROCHA NINO, "Verification-driven development of ICAROUS based on automatic reachability analysis: a preliminary case study" Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software . En: Estados Unidos  ISBN: 978-1-4503-5077-8  ed: ACM Press (Association of Computing Machinery) , v. , p.94 - 97  ,2017
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Documentos de trabajo

    Producción bibliográfica - Documento de trabajo (Working Paper)
    HERNAN CAMILO ROCHA NINO, "Symbolic Reachability Analysis for Rewrite Theories" En: . 2012. p.
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,

    Softwares

    Producción técnica - Softwares - Computacional
    HERNAN CAMILO ROCHA NINO, Symbolic Reachability Analysis for NASA's Plan Execution Interchange Language - PLEXIL, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2012,  .plataforma: ,  .ambiente: ,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
    Sectores:
    Aeronáutica y espacio,
    Producción técnica - Softwares - Computacional
    HERNAN CAMILO ROCHA NINO, The Maude Invariant Analyzer Tool, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2010,  .plataforma: Varias,  .ambiente: Varias,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación, Ciencias Naturales -- Matemática -- Matemáticas Aplicadas,
    Producción técnica - Softwares - Computacional
    HERNAN CAMILO ROCHA NINO, A rewriting logic semantics for NASA's Plan Execution Interchange Language - PLEXIL, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2009,  .plataforma: ,  .ambiente: ,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
    Sectores:
    Aeronáutica y espacio,
    Producción técnica - Softwares - Computacional
    HERNAN CAMILO ROCHA NINO, SMaude, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2011,  .plataforma: Varios,  .ambiente: Varios,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación, Ciencias Naturales -- Matemática -- Matemáticas Aplicadas,
    Sectores:
    Aeronáutica y espacio,
    Producción técnica - Softwares - Computacional
    HERNAN CAMILO ROCHA NINO, FRANCISCO DURAN, JOSE MARIA ALVAREZ, The Maude Formal Environment, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2011,  .plataforma: ,  .ambiente: ,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
    Sectores:
    Desarrollo de programas (software) y prestación de servicios en informática - Consultoría en sistemas de informática,
    Producción técnica - Softwares - Computacional
    HERNAN CAMILO ROCHA NINO, Extension to the Maude Sufficient Completeness Checker, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2010,  .plataforma: ,  .ambiente: ,
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,

    Productos tecnológicos

  • Producción técnica - Productos tecnológicos - Otro
  • JAIME ALEJANDRO BOHORQUEZ, ALFONSO MELENDEZ, HERNAN CAMILO ROCHA NINO, Diseñador de Pruebas de Lógica Ecuacional, Nombre comercial: , contrato/registro: , . En: Colombia,  ,2003, 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,

    Informes técnicos

  • Producción técnica - Consultoría Científico Tecnológica e Informe Técnico - Informe técnico
  • HERNAN CAMILO ROCHA NINO, YOSSI SHEFFI, Five Isomorphic Boolean Theories and Four Decision Procedures, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2007,  12 meses   p.66 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Producción técnica - Consultoría Científico Tecnológica e Informe Técnico - Informe técnico
  • HERNAN CAMILO ROCHA NINO, GILLES DOWEK, CESAR MUNOZ, Rewriting Logic Semantics of a Plan Execution Language, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2013,  0 meses   p.25 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Producción técnica - Consultoría Científico Tecnológica e Informe Técnico - Informe técnico
  • HERNAN CAMILO ROCHA NINO, YOSSI SHEFFI, Proving Safety Properties of Rewrite Theories, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2010,  0 meses   p.29 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Producción técnica - Consultoría Científico Tecnológica e Informe Técnico - Informe técnico
  • HERNAN CAMILO ROCHA NINO, YOSSI SHEFFI, Theorem Proving Modulo Based on Boolean Procedures, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2007,  0 meses   p.29 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Producción técnica - Consultoría Científico Tecnológica e Informe Técnico - Informe técnico
  • HERNAN CAMILO ROCHA NINO, YOSSI SHEFFI, CESAR MUNOZ, Rewriting Modulo SMT, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2013,  0 meses   p.27 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Producción técnica - Consultoría Científico Tecnológica e Informe Técnico - Informe técnico
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, Constructors, Sufficient Completeness and Deadlock Freedom of Generalized Rewrite Theories, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2010,  0 meses   p.39 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,
  • Producción técnica - Consultoría Científico Tecnológica e Informe Técnico - Informe técnico
  • HERNAN CAMILO ROCHA NINO, RAUL GUTIERREZ, YOSSI SHEFFI, Order-sorted Equality Enrichments Modulo Axioms, Nombre comercial: , contrato/registro: , . En: Estados Unidos,  ,2011,  0 meses   p.41 
    Areas:
    Ciencias Naturales -- Computación y Ciencias de la Información -- Ciencias de la Computación,

    Informes de investigación

  • Producción técnica - Informes de investigación
  • FRANCISCO JOSE CHAVES ALONSO, HERNAN CAMILO ROCHA NINO, Executable Calculational Expressions . En: ,  ,2015, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, CESAR MUNOZ, GILLES DOWEK, Rewriting Logic Semantics of a Plan Execution Language . En: ,  ,2009, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, Theorem Proving Modulo Based on Boolean Procedures . En: ,  ,2007, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, Constructors, Sufficient Completeness and Deadlock Freedom of Generalized Rewrite Theories . En: ,  ,2010, 
  • Producción técnica - Informes de investigación
  • RAUL GUTIERREZ, JOSE MESEGUER, HERNAN CAMILO ROCHA NINO, Order-sorted Equality Enrichments Modulo Axioms . En: ,  ,2011, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, CESAR MUNOZ, Rewriting Modulo SMT . En: ,  ,2013, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, Proving Safety Properties of Rewrite Theories . En: ,  ,2010, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, Five Isomorphic Boolean Theories and Four Decision Procedures . En: ,  ,2007, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, JOSE MESEGUER, A Rewriting Decision Procedure for Dijkstra-Scholten¿s Syllogistic Logic with Complements . En: ,  ,2007, 
  • Producción técnica - Informes de investigación
  • JOSE MESEGUER, HERNAN CAMILO ROCHA NINO, Verification of the IBOS Browser Security Properties in Reachability Logic. . En: ,  ,2020, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, SERGIO STEVEN RAMIREZ RICO, MIGUEL ANGEL ROMERO GONZALEZ, FRANK VALENCIA, A Rewriting Logic Approach to Stochastic and Spatial Constraint System Specification and Verification. . En: ,  ,2019, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, CARLOS ANTONIO PINZON HENAO, JORGE FINKE, A Random Network Model for the Analysis of Blockchain Designs with Communication Delay. . En: ,  ,2019, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, JORGE FINKE, MIGUEL ANGEL ROMERO GONZALEZ, LUIS EDUARDO TOBON LLANO, Spectral Evolution with Approximated Eigenvalue Trajectories for Link Prediction. . En: ,  ,2020, 
  • Producción técnica - Informes de investigación
  • JORGE FINKE, HERNAN CAMILO ROCHA NINO, Using Overlapping Communities and Network Structure for Identifying Reduced Groups of Stress Responsive Genes. . En: ,  ,2020, 
  • Producción técnica - Informes de investigación
  • ELAINE GOUVEA PIMENTEL, HERNAN CAMILO ROCHA NINO, CARLOS ALBERTO OLARTE VEGA, A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems. . En: ,  ,2021, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, Reachability Analysis for Spatial Concurrent Constraint Systems with Extrusion . En: ,  ,2018, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, Reachability Analysis for Spatial Concurrent Constraint Systems with Extrusion . En: ,  ,2018, 
  • Producción técnica - Informes de investigación
  • MIGUEL ANGEL ROMERO GONZALEZ, HERNAN CAMILO ROCHA NINO, Reachability Analysis for Spatial Concurrent Constraint Systems with Extrusion . En: ,  ,2018, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, JORGE FINKE, JAN ALEJANDRO MEDINA LOPEZ, Estimating Formation Mechanisms and Degree Distributions in Mixed Attachment Networks . En: ,  ,2018, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, CESAR MUNOZ, JOSE MESEGUER, Rewriting Modulo SMT and Open System Analysis . En: ,  ,2016, 
  • Producción técnica - Informes de investigación
  • CARLOS ANTONIO PINZON HENAO, HERNAN CAMILO ROCHA NINO, Double-spend Attack Models with Time Advantage for Bitcoin. . En: ,  ,2016, 
  • Producción técnica - Informes de investigación
  • MIGUEL ANGEL ROMERO GONZALEZ, HERNAN CAMILO ROCHA NINO, Library Management for PVS. . En: ,  ,2016, 
  • Producción técnica - Informes de investigación
  • HERNAN CAMILO ROCHA NINO, FRANCISCO DURAN, JOSE MESEGUER, Proving Ground Confluence of Equational Specifications Modulo Axioms . En: ,  ,2018, 

    Proyectos

    Tipo de proyecto: Investigación, desarrollo e Innovación 
    Teoría de Conjuntos desde una perspectiva calculatoria
    Inicio: Enero  2016 Fin: Enero  2017 Duración 
    Resumen

    El propósito del proyecto es explorar las ventajas del estilo calculatorio de Dijkstra y Scholten en la presentación de la Teoría axiomática de Conjuntos, en términos de la precisión en las definiciones, eficiencia y elegancia en las demostraciones de los teoremas, y también desde el punto de vista de la didáctica y la dinámica en el aula de clases. En resumen, el proyecto consiste en escribir los fundamentos de la Teoría de Conjuntos usando el estilo calculatorio de Dijkstra y Scholten, para así poder ofrecer a los estudiantes de Matemáticas e Ingeniería de Sistemas alternativas de aprendizaje de áreas comunes de su formación.

    Tipo de proyecto: Investigación, desarrollo e Innovación 
    Stochastic Concurrency in Rewrite-based Probabilistic Models (SCORES)
    Inicio: Enero  2018 Fin: Diciembre  2018 Duración 
    Resumen

    This project takes up the task of developing an executable semantics for the precise specification of probabilistic behavior (i.e., behavior resulting from probabilistic choice) in reactive systems, where both internal and external non-determinism play a central role. More precisely, the main goal of this proposal is to develop computational techniques and tools for reactive systems that will enable the quantitative analysis of properties for PNTCC. The main challenge is that concurrent systems in this setting can exhibit any combination of probabilistic choice and flow of private and public information. In the end, the state of the art will be advanced in different domains including probabilistic concurrent systems, probabilistic rewriting logic specification, and automated analysis. This may enable a systematic and automatic approach to the analysis of quantitative aspects of today's reactive and ubiquitous systems such as cloud-based computation, social networking, and mission-critical applications.

    Tipo de proyecto: Investigación, desarrollo e Innovación 
    OMICAS: Optimización Multiescala In-silico de Cultivos Agrícolas Sostenibles (infraestructura y validación en arroz y caña de azúcar)
    Inicio: Octubre  2018 Duración 
    Resumen

    Alto impacto para la agricultura. Como se observó en la revolución verde para los cereales, esta estrategia puede ser motor de desarrollo para la agricultura si se realiza combinando el acceso a recursos genéticos y nuevas tecnologías. Una revolución verde en Colombia debe generar variedades que incrementen la productividad y competitividad, mejoren la seguridad alimentaria y promuevan el desarrollo de sistemas ambientalmente sostenibles.

    Tipo de proyecto: Investigación y desarrollo 
    EPistemic Interactive Concurrency (EPIC)
    Inicio: Enero  2017 Duración 
    Resumen

    The aim of the project is to coherently combine and advance the state of the art of domains such as concurrency theory, mathematical logic, order theory, information theory and rewriting systems for reasoning about today¿s distributed and multi­-agent systems.

    Tipo de proyecto: Investigación y desarrollo 
    Nuevos Doctores 2016
    Inicio: Julio  2016 Fin: Diciembre  2016 Duración 
    Resumen

    The goals of this proposal are twofold: * It aims at wrapping up the mathematical foundations and tool support of rewriting modulo SMT for synchronous systems such as PLEXIL. * It aims at developing interesting case studies using the synchronous language PLEXIL for showcasing the features and main advantages of rewriting modulo SMT.

    Tipo de proyecto: Investigación y desarrollo 
    Casos de estudio en el modelaje y análisis formal de sistemas de software complejos
    Inicio: Enero  2014 Fin: Diciembre  2014 Duración 
    Resumen

    El objetivo principal del proyecto es desarrollar y documentar casos de estudio significativos sobre el uso de métodos formales en el modelaje, simulación y análsis de sistemas complejos. Los objetivos específicos del proyecto son: * identificar sistemas complejos que pueden ser del interés de la industria de software regional * modelar algunos de estos sistemas usando técnicas de métodos formales * simular y analizar estos sistemas * demostrar propiedades de interés de estos sistemas * documentar las experiencias anteriores dentro de un catálogo de casos de estudio

    Tipo de proyecto: Investigación, desarrollo e Innovación 
    Impacto del Uso de Tecnologías de Información en el Desempeño de los Programas de Intercambio Voluntario de Riñones
    Inicio: Enero  2016 Fin: Enero  2017 Duración 
    Resumen

    Desarrollar un modelo de Optimización basado en Programación Entera y métodos de solución para el problema de emparejamiento de Donantes y Receptores en un programa de donación voluntaria de Riñones considerando restricciones de robustez.

    Tipo de proyecto: Investigación, desarrollo e Innovación 
    Implantación de planes confiables para automatizar tareas de agricultura de precisión
    Inicio: Enero  2017 Fin: Diciembre  2017 Duración 
    Resumen

    La tecnología para la construcción de robots ha tenido un desarrollo vertiginoso en los últimos años, tanto a nivel eléctrico-mecánico con sensores y actuadores cada vez más avanzados, como a nivel lógico y de control mediante el desarrollo de frameworks que estandarizan y simplifican la interacción con los componentes electro-mecánicos de los robots. Aunque estos desarrollos han aportado significativamente a la masificación de los proyectos en robótica en el sector académico e industrial, en este proyecto se plantea la posibilidad de potenciarlos aún más al incorporar a este entorno conceptos y tecnologías usados casi exclusivamente en sistemas de misión crítica -como los usados en misiones espaciales-. Específicamente, se quiere evaluar la posibilidad de integrar lenguajes de programación síncronos/reactivos, y fáciles de verificar formalmente como Plexil a las arquitecturas de control de robots más comunmente usadas en el sector (como las basdas en ROS/Robot Operating System). Con esto, y aprovechando las propiedades matemáticas de dichos lenguajes, se implementará una solución de automatización real que incluya una fase de verificación y validación formal de los algoritmos asociados a dicha solución, buscando aumentar la confiabilidad de dicha solución. Como caso de aplicación, se plantea continuar trabajando en escenario identificado a través del proyecto Evaluación de la Tecnología PLEXIL en Ambientes Robóticos del Contexto Nacional: la Agricultura de Precisión.

    Tipo de proyecto: Investigación, desarrollo e Innovación 
    Symbolic Reachability Analysis for Rewrite Theories (Part 2)
    Inicio: Enero  2013 Fin: Enero  2016 Duración 
    Resumen

    This project presents a significant step forward in automatic and semi-automatic reasoning for reachability properties of rewriting logic specifications, a major research goal in the current state of the art. In particular, this work develops deductive techniques for reasoning symbolically about specifications with initial model semantics, including: (i) new constructor-based notions for reachability analysis, (ii) a proof system for the task of proving safety properties, and (iii) a novel method for symbolic reachability analysis of rewrite theories with constrained built-ins. These three new techniques are not just theoretical developments: each of them has been implemented in freely available tools for the automated reasoning presented in this thesis and are validated through case studies. These case studies include: (i) a reliable communication protocol, (ii) a secure-by-design browser system, and (iii) a NASA language for robotic machines. One main characteristic of the methods developed in this dissertation is that they are suitable for wide classes of rewrite theories and are highly generic, so that they can be used over many different instance languages and application domains.

    Tipo de proyecto: Investigación, desarrollo e Innovación 
    Symbolic Reachability Analysis for Rewrite Theories (Part 1)
    Inicio: Agosto  2006 Fin: Diciembre  2012 Duración 
    Resumen

    This project presents a significant step forward in automatic and semi-automatic reasoning for reachability properties of rewriting logic specifications, a major research goal in the current state of the art. In particular, this work develops deductive techniques for reasoning symbolically about specifications with initial model semantics, including: (i) new constructor-based notions for reachability analysis, (ii) a proof system for the task of proving safety properties, and (iii) a novel method for symbolic reachability analysis of rewrite theories with constrained built-ins. These three new techniques are not just theoretical developments: each of them has been implemented in freely available tools for the automated reasoning presented in this thesis and are validated through case studies. These case studies include: (i) a reliable communication protocol, (ii) a secure-by-design browser system, and (iii) a NASA language for robotic machines. One main characteristic of the methods developed in this dissertation is that they are suitable for wide classes of rewrite theories and are highly generic, so that they can be used over many different instance languages and application domains.