Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarJose Divasón
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2020
[d10]Jose Divasón:
A verified algorithm for computing the Smith normal form of a matrix. Arch. Formal Proofs 2020 (2020)- [j5]Jose Divasón
, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Verified Implementation of the Berlekamp-Zassenhaus Factorization Algorithm. J. Autom. Reasoning 64(4): 699-735 (2020)
2010 – 2019
- 2019
- [j4]Julián Cuevas-Rozo, Jose Divasón, Miguel Marco-Buzunáriz, Ana Romero:
A Kenzo interface for algebraic topology computations in SageMath. ACM Commun. Comput. Algebra 53(2): 61-64 (2019) - [c10]Andrea Guidolin, Jose Divasón, Ana Romero, Francesco Vaccarino:
Computing Multipersistence by Means of Spectral Systems. ISSAC 2019: 195-202 - [c9]Jose Divasón, Ana Romero:
Using Krakatoa for Teaching Formal Verification of Java Programs. FMTea 2019: 37-51 - 2018
- [d9]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified LLL algorithm. Arch. Formal Proofs 2018 (2018) - [d8]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A verified factorization algorithm for integer polynomials with polynomial complexity. Arch. Formal Proofs 2018 (2018) - [c8]Jose Divasón, Jesús Aransay:
A Formal Proof of the Computation of Hermite Normal Form in a General Setting. AISC 2018: 37-53 - [c7]Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper). CPP 2018: 2-13 - [c6]Ana Romero, Jose Divasón:
Experiences and new alternatives for teaching formal verification of Java programs. ITiCSE 2018: 383 - [c5]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A Formalization of the LLL Basis Reduction Algorithm. ITP 2018: 160-177 - 2017
- [j3]Jesús Aransay, Jose Divasón:
A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem. J. Autom. Reasoning 58(4): 509-535 (2017) - [c4]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP 2017: 17-29 - 2016
- [d7]Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
The Factorization Algorithm of Berlekamp and Zassenhaus. Arch. Formal Proofs 2016 (2016) - [d6]Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Perron-Frobenius Theorem for Spectral Radius Analysis. Arch. Formal Proofs 2016 (2016) - [j2]Jesús Aransay, Jose Divasón:
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. Formal Asp. Comput. 28(6): 1005-1026 (2016) - 2015
- [d5]Jose Divasón, Jesús Aransay:
QR Decomposition. Arch. Formal Proofs 2015 (2015) - [d4]Jose Divasón, Jesús Aransay:
Echelon Form. Arch. Formal Proofs 2015 (2015) - [d3]Jose Divasón, Jesús Aransay:
Hermite Normal Form. Arch. Formal Proofs 2015 (2015) - [j1]Jesús Aransay, Jose Divasón:
Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm. J. Funct. Program. 25 (2015) - [c3]Jesús Aransay, Jose Divasón:
Generalizing a Mathematical Analysis Library in Isabelle/HOL. NFM 2015: 415-421 - 2014
- [d2]Jose Divasón, Jesús Aransay:
Gauss-Jordan Algorithm and Its Applications. Arch. Formal Proofs 2014 (2014) - [c2]Jesús Aransay-Azofra, Jose Divasón, Jónathan Heras, Laureano Lambán, María Vico Pascual, Ángel Luis Rubio, Julio Rubio:
Obtaining an ACL2 Specification from an Isabelle/HOL Theory. AISC 2014: 49-63 - [i1]Jesús Aransay, Jose Divasón:
Applications of the Gauss-Jordan algorithm, done right. CoRR abs/1401.5910 (2014) - 2013
- [d1]Jose Divasón, Jesús Aransay:
Rank-Nullity Theorem in Linear Algebra. Arch. Formal Proofs 2013 (2013) - [c1]Jesús Aransay, Jose Divasón:
Formalization and Execution of Linear Algebra: From Theorems to Algorithms. LOPSTR 2013: 1-18
Coauthor Index
aka: Jesús Aransay-Azofra
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org and opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy.
Citation data
Add a list of citing articles from to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy.
Tweets on dblp homepage
Show tweets from 
on the dblp homepage.
Privacy notice: By enabling the option above, your browser will contact twitter.com and twimg.com to load tweets curated by our Twitter accout. At the same time, Twitter will persitently store several cookies with your web browser. While we did signal Twitter to not track our users by setting the "dnt" flag, we do not have any control over how Twitter uses your data. So please proceed with care and consider checking the Twitter privacy policy.
last updated on 2020-06-17 01:17 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
