Journals

• Parsimony search in small high-dimensional datasets with HYB-PARSIMONY
  Jose Divasón, Alpha Pernía Espinoza, Ana Romero and Francisco Javier Martínez de Pisón
  Logic Journal of the IGPL. 2025.
  The final publication is available at Oxford Academic via https://doi.org/10.1093/jigpal/jzaf045
  
• An AI-based open-source software for Varroa mite fall analysis in honeybee colonies
  Jesús Yániz, Matías Casalongue, Francisco Javier Martínez de Pisón, Miguel Angel Silvestre, Beeguards Consortium, Pilar Santolaria and Jose Divasón
  Agriculture. 2025.
  The final publication is available at https://doi.org/10.3390/agriculture15090969
  
• Intelligent sensor software for robust and energy-sustainable decision-making in welding of steel reinforcement for concrete
  Javier Ferreiro-Cabello, Francisco Javier Martinez-de-Pison, Esteban Fraile-Garcia, Alpha Pernia-Espinoza and Jose Divasón
  Sensors. 2024.
  The final publication is available at https://doi.org/10.3390/s25010028
  
• Zigzag persistence for image processing: New software and applications
  Jose Divasón, Ana Romero, Pilar Santolaria and Jesús Yániz
  Pattern Recognition Letters. 2024.
  The final publication is available at Elsevier via https://doi.org/10.1016/j.patrec.2024.06.010
  
• Analysis of Varroa Mite Colony Infestation Level Using New Open Software Based on Deep Learning Techniques
  Jose Divasón, Ana Romero, Francisco Javier Martínez de Pisón, Matías Casalongue, Miguel A. Silvestre, Pilar Santolaria and Jesús Yániz
  Sensors. 2024.
  The final publication is available at https://doi.org/10.3390/s24123828
  
• HYB-PARSIMONY: A hybrid approach combining Particle Swarm Optimization and Genetic Algorithms to find parsimonious models in high-dimensional datasets
  Jose Divasón, Alpha Pernía Espinoza and Francisco Javier Martínez de Pisón
  Neurocomputing. 2023.
  The final publication is available at Elsevier via https://doi.org/10.1016/j.neucom.2023.126840
  
• Artificial Intelligence models for assessing the evaluation process of complex student projects
  Jose Divasón, Francisco Javier Martínez de Pisón, Ana Romero and Eduardo Sáenz de Cabezón
  IEEE Transactions on Learning Technologies. 2023.
  The final publication is available at IEEE via https://doi.org/10.1109/TLT.2023.3246589
  
• In vitro maintenance of drones and development of a new software for sperm quality analysis facilitate the study of honey bee reproductive quality
  Jose Divasón, Ana Romero, Miguel A. Silvestre, Pilar Santolaria and Jesús Yániz
  Journal of Apicultural Research. 2023.
  The final publication is available at Taylor & Francis via https://doi.org/10.1080/00218839.2023.2231673
  
• PSO-PARSIMONY: A method for finding parsimonious and accurate machine learning models with particle swarm optimization. Application for predicting force-displacement curves in T-stub steel connections
  Jose Divasón, Julio Fernández Ceniceros, Andrés Sanz García, Alpha Pernía Espinoza and Francisco Javier Martínez de Pisón
  Neurocomputing. 2023.
  The final publication is available at Elsevier via https://doi.org/10.1016/j.neucom.2023.126414
  
• A Formalization of the Smith Normal Form in Higher-Order Logic
  Jose Divasón and René Thiemann
  Journal of Automated Reasoning. 2022.
  The final publication is available at Springer via https://doi.org/10.1007/s10817-022-09631-5
  
• Integration of the Kenzo system within SageMath for new algebraic topology computations
  Julián Cuevas, Jose Divasón, Miguel Marco-Buzunáriz and Ana Romero
  Mathematics. 2021.
  The final publication is available at https://doi.org/10.3390/math9070722
  
• Computing invariants for multipersistence via spectral systems and effective homology
  Andrea Guidolin, Jose Divasón, Ana Romero and Francesco Vaccarino
  Journal of Symbolic Computation. 2020.
  The final publication is available at Elsevier via https://doi.org/10.1016/j.jsc.2020.09.007
  
• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL
  René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan Joosten, and Akihisa Yamada
  Journal of Automated Reasoning. 2020.
  The final publication is available at Springer via https://doi.org/10.1007/s10817-020-09552-1
  
• A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  Journal of Automated Reasoning. 2019.
  The final publication is available at Springer via https://doi.org/10.1007/s10817-019-09526-y
  
• A formalisation in HOL of the Fundamental Theorem of Linear Algebra and its application to the solution of the least squares problem
  Jesús Aransay and Jose Divasón
  Journal of Automated Reasoning Volume 58, Issue 4. 2017.
  The final publication is available at Springer via http://dx.doi.org/10.1007/s10817-016-9379-z
  
• Formalisation of the Computation of the Echelon Form of a Matrix in Isabelle/HOL
  Jesús Aransay and Jose Divasón
  Formal Aspects of Computing Volume 28. 2016.
  The final publication is available at Springer via http://dx.doi.org/10.1007/s00165-016-0383-1
  
• Formalisation in Higher-Order Logic and code generation to functional languages of the Gauss-Jordan algorithm
  Jesús Aransay and Jose Divasón
  Journal of Functional Programming Volume 25. 2015.
  © Cambridge Journals
  

---

Conference Papers

• BatNoiseDL: Discrimination of bat signals through an ensemble of deep learning models
  Jose Divasón, Francisco Javier Martínez de Pisón and Félix González
  Proceedings of the 19th International Conference on Hybrid Artificial Intelligence Systems (HAIS 2024)
  
• Hybrid intelligent parsimony search in small high-dimensional datasets
  Jose Divasón, Alpha Pernía Espinoza, Ana Romero and Francisco Javier Martínez de Pisón
  Proceedings of the 18th International Conference on Hybrid Artificial Intelligence Systems (HAIS 2023)
  
• Varroa mite detection using deep learning techniques
  Jose Divasón, Francisco Javier Martínez de Pisón, Ana Romero, Pilar Santolaria and Jesús Yániz
  Proceedings of the 18th International Conference on Hybrid Artificial Intelligence Systems (HAIS 2023)
  
• Robustness analysis of a methodology to detect biases, inconsistencies and discrepancies in the evaluation process
  Jose Divasón, Francisco Javier Martínez de Pisón, Ana Romero and Eduardo Sáenz de Cabezón
  Proceedings of the 14th International Conference on EUropean Transnational Educational (ICEUTE 2023)
  
• Sensitivity analysis of discrete preference functions using Koszul simplicial complexes
  Jose Divasón, Fatemeh Mohammadi, Henry P. Wynn and Eduardo Sáenz de Cabezón
  Proceedings of the 48th International Symposium on Symbolic and Algebraic Computation (ISSAC 2023)
  
• Effective homology of universal covers
  Miguel Marco-Buzunáriz, Jose Divasón and Ana Romero
  Proceedings of the the software demostration session of the 48th International Symposium on Symbolic and Algebraic Computation (ISSAC 2023)
  
• CASABee: el primer sistema de análisis espermático asistido por ordenador desarrollado específicamente para insectos
  Jose Divasón, Ana Romero Pilar Santolaria and Jesús Yániz
  Actas de las XX Jornadas sobre Producción Animal (AIDA 2023)
  
• New Hybrid Methodology Based on Particle Swarm Optimization with Genetic Algorithms to Improve the Search of Parsimonious Models in High-Dimensional Databases
  Jose Divasón, Alpha Pernía Espinoza and Francisco Javier Martínez de Pisón
  Proceedings of the 17th International Conference on Hybrid Artificial Intelligence Systems (HAIS 2022)
  
• Faster Kenzo computations via SageMath, and vice versa
  Jose Divasón, Miguel Marco-Buzunáriz and Ana Romero
  Proceedings of the XVII Spanish Meeting on Computer Algebra and Applications (EACA 2022)
  
• Q-learning and MCTS techniques for improving an algorithm to compute discrete vector fields on finite topological spaces
  Julián Cuevas-Rozo, Jose Divasón, Laureano Lambán and Ana Romero
  Proceedings of the 9th International Symposium on Symbolic Computation in Software Science (SCSS 2021)
  
• A Kenzo Interface for Algebraic Topology Computations in SageMath
  Julián Cuevas, Jose Divasón, Miguel Marco-Buzunáriz and Ana Romero
  Proceedings of the software demostration session of the 44th International Symposium on Symbolic and Algebraic Computation (ISSAC 2019)
  Best software presentation award!! See the slides in an interactive environment
  
• Computing Multipersistence by Means of Spectral Systems
  Andrea Guidolin, Jose Divasón, Ana Romero and Francesco Vaccarino
  Proceedings of the 44th International Symposium on Symbolic and Algebraic Computation (ISSAC 2019)
  
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting
  Jose Divasón and Jesús Aransay
  Proceedings of the 13th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2018)
  
• A Formalization of the LLL Basis Reduction Algorithm
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  Proceedings of the 9th International Conference on Interactive Theorem Proving (ITP 2018)
  
• Towards a verified Smith normal form algorithm in Isabelle/HOL
  Jose Divasón and Jesús Aransay
  Proceedings of the XVI Spanish Meeting on Computer Algebra and Applications (EACA 2018)
  
• Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
  Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann and Akihisa Yamada
  Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018)
  
• A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017)
  
• Verified Computer Linear Algebra
  Jesús Aransay and Jose Divasón
  Proceedings of the XV Spanish Meeting on Computer Algebra and Applications (EACA 2016)
  
• Generalizing a Mathematical Analysis library in Isabelle/HOL
  Jesús Aransay and Jose Divasón
  Proceedings of the Seventh NASA Formal Methods Symposium (NFM 2015)
  The final publication will be available at http://link.springer.com
• Obtaining an ACL2 specification from an Isabelle/HOL theory
  Jesús Aransay, Jose Divasón, Jónathan Heras, Laureano Lambán, Vico Pascual, Angel Luis Rubio and Julio Rubio
  Proceedings of the Artificial Intelligence and Symbolic Computation (AISC 2014)
  The final publication is available at http://link.springer.com
• Formalization and execution of Linear Algebra: from theorems to algorithms
  Jesús Aransay and Jose Divasón
  Revised Selected Papers of the Logic-Based Program Synthesis and Transformation (LOPSTR 2013)
  The final publication is available at http://link.springer.com
• Formalization and execution of Linear Algebra: from theorems to algorithms
  Jesús Aransay and Jose Divasón
  Proceedings of the Logic-Based Program Synthesis and Transformation (LOPSTR 2013)
• Performance Analysis of a Verified Linear Algebra Program in SML
  Jesús Aransay and Jose Divasón
  Proceedings of the XII Jornadas sobre Programación y Lenguajes (PROLE 2013) y V Taller de Programación Funcional (TPF 2013)
• Formalizing an abstract algebra textbook in Isabelle/HOL
  Jesús Aransay and Jose Divasón
  Proceedings of the XIII Spanish Meeting on Computer Algebra and Applications (EACA 2012)

---

Archive of Formal Proofs

• Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
  Ralph Bottesch, Jose Divasón and René Thiemann
  March 2021. Archive of Formal Proofs
• A verified algorithm for computing the Smith normal form of a matrix
  Jose Divasón
  May 2020. Archive of Formal Proofs
• A verified factorization algorithm for integer polynomials with polynomial complexity
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  January 2018. Archive of Formal Proofs
• A verified LLL algorithm
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  January 2018. Archive of Formal Proofs
• The Factorization Algorithm of Berlekamp and Zassenhaus
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  October 2016. Archive of Formal Proofs
• Perron-Frobenius Theorem for Spectral Radius Analysis
  Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada
  May 2016. Archive of Formal Proofs
• Hermite Normal Form
  Jesús Aransay and Jose Divasón
  July 2015. Archive of Formal Proofs
• Echelon Form
  Jesús Aransay and Jose Divasón
  January 2015. Archive of Formal Proofs
• QR Decomposition
  Jesús Aransay and Jose Divasón
  January 2015. Archive of Formal Proofs
• Gauss-Jordan Algorithm and Its Applications
  Jesús Aransay and Jose Divasón
  August 2014. Archive of Formal Proofs
• Rank-Nullity Theorem in Linear Algebra
  Jesús Aransay and Jose Divasón
  January 2013. Archive of Formal Proofs

---

Theses

• Formalisation and execution of Linear Algebra: theorems and algorithms
  Jose Divasón supervised by Julio Rubio and Jesús Aransay
  PhD thesis. Universidad de La Rioja. June 2016
• Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL
  Jose Divasón supervised by Jesús Aransay
  Degree's thesis. Universidad de La Rioja. October 2011

---

Workshop papers and technical reports

• A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  16th International Workshop on Termination (WST 2018)
  
• Certifying exact complexity bounds for matrix interpretations
  Jose Divasón, Sebastiaan Joosten, Ondřej Kunčar, René Thiemann and Akihisa Yamada
  Proceedings of the 16th International Workshop on Logic and Computational Complexity (LCC 2016)
  
• A Formalization of Berlekamp's Factorization Algorithm
  Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada
  Isabelle Workshop 2016
  
• Transforming (almost) without programming: a case of interoperability among theorem provers
  Jesús Aransay, Jose Divasón, Jónathan Heras, Laureano Lambán, Vico Pascual, Angel Luis Rubio and Julio Rubio
  Technical report. June 2013
• A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and ACL2
  Jesús Aransay, Jose Divasón, Jónathan Heras, Laureano Lambán, Vico Pascual, Angel Luis Rubio and Julio Rubio
  Technical report. February 2013

---

Education papers

• Modelos de inteligencia artificial para asesorar el proceso evaluador de trabajos informáticos complejos
  Jose Divasón, Francisco Javier Martínez de Pisón, Ana Romero and Eduardo Sáenz de Cabezón
  Actas de las XXVII Jornadas sobre la Enseñanza Universitaria de la Informática (JENUI 2021)
  Best work award!!
  
• Using Krakatoa for teaching formal verification of Java programs
  Jose Divasón and Ana Romero
  Proceedings of the Formal Methods Teaching Workshop and Tutorial (FMTea 2019)
  
• Experiences and New Alternatives for Teaching Formal Verification of Java Programs
  Ana Romero and Jose Divasón
  Proceedings of the 23rd Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2018)
  
• Experiencia con una herramienta para automatizar la comprobación de requisitos de los trabajos HTML-CSS de Sistemas Informáticos
  Jose Divasón, Ana Romero and Eduardo Sáenz de Cabezón
  Actas de las XXIV Jornadas sobre la Enseñanza Universitaria de la Informática (JENUI 2018)
  

Links

• ForMath Project