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 | 18 | 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, 2015 | 16 | 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 (6), 1005-1026, 2016 | 14 | 2016 |

Formalization and execution of Linear Algebra: from theorems to algorithms J Aransay, J Divasón International Symposium on Logic-Based Program Synthesis and Transformation …, 2013 | 12 | 2013 |

A formalization of the LLL basis reduction algorithm J Divasón, S Joosten, R Thiemann, A Yamada International Conference on Interactive Theorem Proving, 160-177, 2018 | 9 | 2018 |

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 | 9 | 2018 |

Generalizing a mathematical analysis library in Isabelle/HOL J Aransay, J Divasón NASA Formal Methods Symposium, 415-421, 2015 | 8 | 2015 |

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 | 7 | 2020 |

Perron-Frobenius theorem for spectral radius analysis J Divasón, O Kuncar, R Thiemann, A Yamada Archive of Formal Proofs, 2016 | 6 | 2016 |

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 | 5 | 2017 |

Gauss-Jordan algorithm and its applications J Divasón, J Aransay Archive of Formal Proofs, 2014 | 5 | 2014 |

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 | |

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 | 4 | 2019 |

Rank-nullity theorem in linear algebra J Divasón, J Aransay Archive of Formal Proofs, 2150, 2013 | 4 | 2013 |

Performance Analysis of a Verified Linear Algebra Program in SML J ús Aransay, J Divasón | 4 | 2013 |

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 |

Using Krakatoa for teaching formal verification of Java programs J Divasón, A Romero Formal Methods Teaching Workshop, 37-51, 2019 | 3 | 2019 |

Generating Persistence Structures for the Integration of Data and Control Aspects in Business Process Monitoring. E Domínguez, B Pérez, ÁL Rubio, MA Zapata, A Allué, A López ICEIS (2), 320-327, 2018 | 3 | 2018 |

La experiencia de un docente que hace no tanto era alumno J Divasón Actas del Simposio-Taller previo a las XXIII Jornadas de Enseñanza …, 2017 | 3 | 2017 |