Formal Reasoning about Efficient Data Structures: A Case Study in ACL2

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús

doi:10.1007/978-3-540-25938-1_7

Ponencia

dc.creator	Ruiz Reina, José Luis	es
dc.creator	Alonso Jiménez, José Antonio	es
dc.creator	Hidalgo Doblado, María José	es
dc.creator	Martín Mateos, Francisco Jesús	es
dc.date.accessioned	2019-05-09T09:57:28Z
dc.date.available	2019-05-09T09:57:28Z
dc.date.issued	2003
dc.identifier.citation	Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2003). Formal Reasoning about Efficient Data Structures: A Case Study in ACL2. En LOPSTR 2003: 13th International Symposium on Logic-Based Program Synthesis and Transformation (75-91), Uppsala, Sweden: Springer.
dc.identifier.isbn	978-3-540-22174-6	es
dc.identifier.issn	0302-9743	es
dc.identifier.uri	https://hdl.handle.net/11441/86267
dc.description.abstract	We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms are represented as directed acyclic graphs (dags) and these graphs are stored in a single-threaded object (stobj). The use of stobjs allows destructive operations on data (thus improving the performance of the algorithm), while maintaining the applicative semantics of ACL2. We intend to show how ACL2 provides an environment where execution of algorithms with efficient data structures and formal reasoning about them can be carried out.	es
dc.description.sponsorship	Ministerio de Ciencia y Tecnología TIC2000-1368-C03-02	es
dc.format	application/pdf	es
dc.language.iso	eng	es
dc.publisher	Springer	es
dc.relation.ispartof	LOPSTR 2003: 13th International Symposium on Logic-Based Program Synthesis and Transformation (2003), p 75-91
dc.rights	Attribution-NonCommercial-NoDerivatives 4.0 Internacional	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc-nd/4.0/	*
dc.title	Formal Reasoning about Efficient Data Structures: A Case Study in ACL2	es
dc.type	info:eu-repo/semantics/conferenceObject	es
dcterms.identifier	https://ror.org/03yxnpp24
dc.type.version	info:eu-repo/semantics/submittedVersion	es
dc.rights.accessRights	info:eu-repo/semantics/openAccess	es
dc.contributor.affiliation	Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial	es
dc.relation.projectID	TIC2000-1368-C03-02	es
dc.relation.publisherversion	https://link.springer.com/chapter/10.1007/978-3-540-25938-1_7	es
dc.identifier.doi	10.1007/978-3-540-25938-1_7	es
dc.contributor.group	Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento	es
idus.format.extent	17	es
dc.publication.initialPage	75	es
dc.publication.endPage	91	es
dc.eventtitle	LOPSTR 2003: 13th International Symposium on Logic-Based Program Synthesis and Transformation	es
dc.eventinstitution	Uppsala, Sweden	es
dc.relation.publicationplace	Berlin	es
dc.identifier.sisius	6532083	es

Ficheros	Tamaño	Formato	Ver	Descripción
Formal Reasoning about Efficient ...	409.2Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Ponencias (Ciencias de la Computación e Inteligencia Artificial)

Mostrar el registro sencillo del ítem

Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional