Semblanza

Artículos

Publicaciones en revistas, conferencias internacionales y revisor en revista internacional.

1. Design and evaluation of indoor wireless ad hoc network using BATMAN-adv with mobile robots.
DOI: http://dx.doi.org/10.1109/iciea54703.2022.10006011

2. Mu-Calculus Satisfiability with Arithmetic Constraints.
DOI: https://doi.org/10.15514/ISPRAS-2021-33(2)-12

3.Regular Expressions for Web Advertising Detection based on an Automatic Sliding Algorithm.
DOI: https://doi.org/10.15514/ISPRAS-2021-33(2)-3

4. Database Management System Verification with Separation Logics.
DOI: http://dx.doi.org/10.1134/s036176882108017x

5. Statistical Analysis of the Effects of Institutions on the Economic Growth of France in Recent Years.
DOI: http://www.scopus.com/inward/record.url?eid=2-s2.0-85081297547&partnerID=MN8TOARS.

6. Towards the processes discovery in the medical treatment of mexican-origin women diagnosed with breast cancer.
DOI: http://www.scopus.com/inward/record.url?eid=2-s2.0-85062906036&partnerID=MN8TOARS

7. A Note on Constructive Interpolation for the Multi-Modal Logic K.
DOI: http://dx.doi.org/10.1016/j.entcs.2020.10.002

8. Formal Verification of a Database Management System.
DOI: http://dx.doi.org/10.1109/conisoft50191.2020.00024

9. Analysis of Academic Achievement in Higher-Middle Education in Mexico through Data Clustering Methods.
DOI: http://dx.doi.org/10.5772/intechopen.84744

10. A Satisfiability Algorithm For The Mu-Calculus For Trees With Presburger Constraints.
DOI: http://dx.doi.org/10.1109/conisoft.2019.00020

11. Data Fusion of Physical Variables as Bearing for User Thermal Comfort Analysis in Closed Environments.
DOI: http://dx.doi.org/10.1109/icev.2019.8920459

12. Craig interpolation on the logic of knowledge.
DOI: http://www.scopus.com/inward/record.url?eid=2-s2.0-85058649501&partnerID=MN8TOARS

13. Data Clustering: An Approach for Evaluating the Adequate Number of Groups in Partitioned Techniques.
DOI: http://dx.doi.org/10.15640/jcsit.v5n1a3

14. Static Reception Results of DRM+ Field Trials in VHF Band II in Brazil.
DOI: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6571211&isnumber=6585784

Ocultar

Mu-Calculus Satisfiability with Arithmetic Constraints

The propositional modal μ-calculus is a well-known specification language for labeled transition systems. In this work, we study an extension of this logic with converse modalities and Presburger arithmetic constraints, interpreted over tree models. We describe a satisfiability algorithm based on breadth-first construction of Fischer-Lardner models. An implementation together several experiments are also reported. Furthermore, we also describe an application of the algorithm to solve static analysis problems over semi-structured data.

• Modal Logics,
• Automated Reasoning,
• Formal Verification

Journal:Proceedings of the Institute for System Programming of the RAS

DOI:10.15514/ISPRAS-2021-33(2)-12

AUTHORS:Yensen Limón-Priego; Ismael Everardo Bárcenas-Patiño; Edgard Iván Benítez-Guerrero; Guillermo Gilberto Molero-Castillo; Alejandro Velazquez-Mena

YEAR:2021

Ocultar

Regular Expressions for Web Advertising Detection based on an Automatic Sliding Algorithm

This paper presents the automation of a Web advertising recognition algorithm, using regular expressions. Currently, the use of regular expressions, optical character recognition, Databases, and automation tests have been critical for multiple Software implementations. The tests were carried out in three Web browsers. As a result, the detection of advertisements in Spanish, that distract attention and that above all extract information from users was achieved. The main feature of the algorithm is that automatic and versatile execution does not require access to the code of the page in question and that in the future it can be an application with background operation. In addition, being supported by optical character recognition gives us acceptable efficiency in detecting advertising.

• Digital Marketing,
• Optical Character Recognition,
• Regular Expressions

Journal:Proceedings of the Institute for System Programming of the RAS

DOI:10.15514/ISPRAS-2021-33(2)-3

Authors:Donovan Riaño Enriquez; Rodrigo Pinon-Ayala; Guillermo Molero-Castillo; Everardo Barcenas; Alejandro Velazquez-Mena

Year:2021

Ocultar

Formal Verification of a Database Management System

Assertion based program verification is a well-known formal approach to (dis)prove correctness of algorithms associated to software systems. Assertions are input and output properties a correct program must satisfy. These properties are traditionally written in a specification language based on classical logic. Associated classical reasoning (inference) systems are then used to (dis)prove program correctness. However, when programs manipulate mutable data structures such as pointers, classical logical operators have been unable to successfully model syntactically unrelated expressions. In this article, we study separation logics, which are equipped with specially-purposed operators to model mutable data structures. We describe the use of this logic as a specification language in the verification of a database management system (DMS). In particular, we detect several bugs in two DMS libraries regarding heap manipulation. We describe these bugs in detail and propose solutions.

• Computer bugs,
• Data structures,
• Resource management

CONFERENCE:8th International Conference in Software Engineering Research and Innovation (CONISOFT)

DOI:10.1109/conisoft50191.2020.00024

AUTHORS:Diego Medina-Martínez; Everardo Bárcenas; Guillermo Molero-Castillo; Alejandro Velazquez-Mena

YEAR:2020

Ocultar

Design and evaluation of indoor wireless ad hoc network using BATMAN-adv with mobile robots

The mesh networks are one alternative because it has three essential characteristics: scalable, cooperative work, and self-organization. This type of network can solve problems of load assignment, distribution of tasks, and resources. One alternative to wireless networks (WLAN) is possible to communicate with multiple nodes, but the mesh networks can have connectivity with all nodes. However, it has been observed that in the literature, there is no implementation of this version (B.A.T.M.A.N. version V) of the protocol in indoor situations. Therefore, in this article, a mesh wireless network with heterogeneous devices is proposed to testbed the protocol with conditions in areas with different levels of obstructions applying teleoperation.

• Wireless Mesh Network,
• Mobile Robot,
• B.A.T.M.A.N.

Conference:2022 IEEE 17th Conference on Industrial Electronics and Applications (ICIEA)

DOI:
10.1109/iciea54703.2022.10006011

Authors:Alejandro Velazquez-Mena; Hector Benitez-Perez; Rita C. Rodriguez-Martinez; Ricardo F. Villarreal-Martinez

Year:2022