Using abstract stobjs in ACL2 to compute matrix normal forms

  1. Lambán, L. 2
  2. Martín-Mateos, F.J. 1
  3. Rubio, J. 2
  4. Ruiz-Reina, J.-L. 1
  1. 1 Universidad de Sevilla
    info

    Universidad de Sevilla

    Sevilla, España

    ROR https://ror.org/03yxnpp24

  2. 2 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2017

Volumen: 10499 LNCS

Páginas: 354-370

Tipo: Artículo

beta Ver similares en nube de resultados
DOI: 10.1007/978-3-319-66107-0_23 SCOPUS: 2-s2.0-85029505235 GOOGLE SCHOLAR

Otras publicaciones en: Lecture Notes in Computer Science

Resumen

We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define a formally verified algorithm that given a matrix with elements in the ring of integers, computes an equivalent matrix in column echelon form. Abstract stobjs allow us to define a sound logical interface between matrices defined as lists of lists, convenient for reasoning but inefficient, and matrices represented as unidimensional stobjs arrays, which implement accesses and (destructive) updates in constant time. Also, by means of the abstract stobjs mechanism, we use a more convenient logical representation of the transformation matrix, as a sequence of elemental transformations. Although we describe here a particular normalization algorithm, we think this approach could be useful to obtain formally verified and efficient executable implementations of a number of matrix normal form algorithms. © 2017, Springer International Publishing AG.