Follow
Jose Divasón
Jose Divasón
Verified email at unirioja.es - Homepage
Title
Cited by
Cited by
Year
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
202017
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
172015
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
152016
Formalization and execution of Linear Algebra: from theorems to algorithms
J Aransay, J Divasón
Logic-Based Program Synthesis and Transformation: 23rd International …, 2014
122014
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
112018
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
92020
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
92018
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
92017
Perron-Frobenius theorem for spectral radius analysis
J Divasón, O Kuncar, R Thiemann, A Yamada
Archive of Formal Proofs, 1-132, 2016
82016
Generalizing a mathematical analysis library in Isabelle/HOL
J Aransay, J Divasón
NASA Formal Methods Symposium, 415-421, 2015
82015
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
62023
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
52019
Gauss-Jordan algorithm and its applications
J Divasón, J Aransay
Archive of Formal Proofs, 2014
52014
Rank-nullity theorem in linear algebra
J Divasón, J Aransay
Archive of Formal Proofs, 2013
52013
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
52012
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
42019
Performance Analysis of a Verified Linear Algebra Program in SML
J ús Aransay, J Divasón
42013
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
32021
Integration of the Kenzo system within SageMath for new algebraic topology computations
J Cuevas-Rozo, J Divasón, M Marco-Buzunáriz, A Romero
Mathematics 9 (7), 722, 2021
32021
The system can't perform the operation now. Try again later.
Articles 1–20