Everardo Bárcenas

Associate Professor 

Computing Engineering Department 

National University of Mexico (UNAM)  

Research interests

• Logic: modal logics, proof theory, automated reasoning, description logics, model checking

• Artificial intelligence: knowledge representation, planning, computer vision

Publications

Activities

• • National Researcher (SNII 2) Secretary of Science, Humanities, Technology and Innovation in Mexico

  • Coordinator of the Artificial Intelligence Microsoft Lab 

  • Editorial board member of the Journal of Reliable Intelligent Environments

  • Organizing committee member:

    • Latin American New Methods of Reasoning Workshop (LANMR) 24-22

  • Program committee member:

    • International Conference on Intelligent Environments (IE) (26 - 21)

    • Workshop on the Reliability of Intelligent Environments (25-21)

    • Latin American New Methods of Reasoning Workshop (LANMR) 20, 19 

    •  Mexican Conference on Pattern Recognition Student's Meeting (MCPR-SM) 20, 19, 18, 17

Projects

• • Automated reasoning for non-classical logics. PAPIIT (2022-2023)

  • Modal characterization of separation logics. PAPIIT (2020-2021)

  • Path planning with model checking. PROMEP (2013-2014)

Career

• Assistant Professor National University of Mexico (UNAM)  

• Associate Professor University of Veracruz - National Science and Technology Council (CONACYT)

• Assistant Professor Universidad Politécnica de Puebla

• Postdoc Rice University

• Ph.D. Université de Grenoble, Institut National de Recherche en Informatique et en Automatique (INRIA) 

• M.Sc. Technische Universität Wien, Universidade NOVA de Lisboa

• B.Sc. Universidad Autónoma de Puebla

Teaching

• • Ingeniería en computación: Inteligencia Artificial,  Estructura de Datos y Algoritmos I

  • Maestría en computación: Lógica computacional

Advising

• • Postdocs

    • Miguel Pérez. Algebraic methods for paraconsistent logics. 

  • PhD

    • René Dávila. Formal verification of smart contracts with description logics.

    • Ricardo López. Proof theory for program synthesis.

    • Yensen Limón (co-advisor: E. Benítez). Automated reasoning for context-aware systems with modal logics. 

  • MSc

    • Emil García. Formal verification of consensus protocols in Blockchain systems.

    • Luis Quispe. Formal verification of IoT systems.

    • Alejandro May. LLM reasoning framework for description logics.

    • Ricardo López. Tree hypersequents for modal logic with graded modalities. 

    • Diego Medina. A satisfiability algorithm for modal logic with converse.

    • Diego Carrillo. A proof theory of multi-modal logics with converse.

    • René Dávila (co-advisor: R. Aldeco). Formal verification of blockchain tender systems. 

    • Rolando Ramírez (co-advisor: C. Mezura). Semantic reasoning for context-aware systems.

    •  Ari Rodríguez (co-advisor: E. Benítez). Gaze pattern recognition with model checking. 

    • Yensen Limón (co-advisor: E. Benítez). Independent analysis for semi-structured data.  

  • BEng 

    • Chistian Leyva. An AI based FinTech platform.

    • Sandra Pérez. Model checking for UAV (drones) path planning.

    • Brandon Silva. Classification algorithm for rethinopaty detection.

    • Pablo Fernández. Path planning with model checking. 

    •  Diego Medina. Program verification with separation logics.