A formalization of the Berlekamp-Zassenhaus factorization algorithm J Divasón, S Joosten, R Thiemann, A Yamada Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and …, 2017 | 20 | 2017 |
Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm J Aransay, J Divason Journal of Functional Programming 25, e9, 2015 | 17 | 2015 |
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL J Aransay, J Divasón Formal Aspects of Computing 28, 1005-1026, 2016 | 16 | 2016 |
Formalization and execution of Linear Algebra: from theorems to algorithms J Aransay, J Divasón Logic-Based Program Synthesis and Transformation: 23rd International …, 2014 | 12 | 2014 |
Efficient certification of complexity proofs: Formalizing the Perron–Frobenius theorem (invited talk paper) J Divasón, S Joosten, O Kunčar, R Thiemann, A Yamada Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018 | 11 | 2018 |
A verified implementation of the Berlekamp–Zassenhaus factorization algorithm J Divasón, SJC Joosten, R Thiemann, A Yamada Journal of Automated Reasoning 64 (4), 699-735, 2020 | 9 | 2020 |
A formalization of the LLL basis reduction algorithm J Divasón, S Joosten, R Thiemann, A Yamada Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018 | 9 | 2018 |
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem J Aransay, J Divasón Journal of Automated Reasoning 58 (4), 509-535, 2017 | 9 | 2017 |
Perron-Frobenius theorem for spectral radius analysis J Divasón, O Kuncar, R Thiemann, A Yamada Archive of Formal Proofs, 1-132, 2016 | 8 | 2016 |
Generalizing a mathematical analysis library in Isabelle/HOL J Aransay, J Divasón NASA Formal Methods Symposium, 415-421, 2015 | 8 | 2015 |
PSO-PARSIMONY: A method for finding parsimonious and accurate machine learning models with particle swarm optimization. Application for predicting force–displacement curves in … J Divasón, JF Ceniceros, A Sanz-Garcia, A Pernia-Espinoza, ... Neurocomputing 548, 126414, 2023 | 6 | 2023 |
A Kenzo interface for algebraic topology computations in SageMath J Cuevas-Rozo, J Divasón, M Marco-Buzunáriz, A Romero ACM Communications in Computer Algebra 53 (2), 61-64, 2019 | 6 | 2019 |
Gauss-Jordan algorithm and its applications J Divasón, J Aransay Archive of Formal Proofs, 2014 | 5 | 2014 |
Rank-nullity theorem in linear algebra J Divasón, J Aransay Archive of Formal Proofs, 2013 | 5 | 2013 |
A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and ACL2 J Aransay, J Divasón, J Heras, L Lambán, P Pascual, AL Rubio, J Rubio Technical report, 2012. http://wiki. portal. chalmers. se/cse/uploads …, 2012 | 5 | 2012 |
QR Decomposition. Archive of Formal Proofs, 2015 J Divasón, J Aransay | 5 | |
Using Krakatoa for teaching formal verification of Java programs J Divasón, A Romero Formal Methods Teaching: Third International Workshop and Tutorial, FMTea …, 2019 | 4 | 2019 |
Performance Analysis of a Verified Linear Algebra Program in SML J ús Aransay, J Divasón | 4 | 2013 |
HYB-PARSIMONY: A hybrid approach combining Particle Swarm Optimization and Genetic Algorithms to find parsimonious models in high-dimensional datasets J Divasón, A Pernia-Espinoza, FJ Martinez-de-Pison Neurocomputing 560, 126840, 2023 | 3 | 2023 |
Computing invariants for multipersistence via spectral systems and effective homology A Guidolin, J Divasón, A Romero, F Vaccarino Journal of Symbolic Computation 104, 724-753, 2021 | 3 | 2021 |