Repositorio de producción científica de la Universidad de Sevilla

Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms

 

Advanced Search
 
Opened Access Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms
Cites

Show item statistics
Icon
Export to
Author: Lambán Pardo, Laureano
Martín Mateos, Francisco Jesús
Rubio, Julio
Ruiz Reina, José Luis
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2017
Published in: ITP 2017: 8th International Conference on Interactive Theorem Proving (2017), p 354-370
ISBN/ISSN: 978-3-319-66106-3
0302-9743
Document type: Presentation
Abstract: 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.
Cite: Lambán Pardo, L., Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2017). Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. En ITP 2017: 8th International Conference on Interactive Theorem Proving (354-370), Brasília, Brazil: Springer.
Size: 147.0Kb
Format: PDF

URI: https://hdl.handle.net/11441/86421

DOI: 10.1007/978-3-319-66107-0_23

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)