Industrial-Strength Documentation for ACL2
The ACL2 theorem prover is a complex system. Its libraries are vast. Industrial verification efforts may extend this base with hundreds of thousands of lines of additional modeling tools, specifications, and proof scripts. High quality documentation is vital for teams that are working together on...
Main Authors: | , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2014-06-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1406.2266v1 |
id |
doaj-c42360ad19d545d2810911ce3297f9b5 |
---|---|
record_format |
Article |
spelling |
doaj-c42360ad19d545d2810911ce3297f9b52020-11-24T22:04:53ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-06-01152Proc. ACL2 201492510.4204/EPTCS.152.2:3Industrial-Strength Documentation for ACL2Jared Davis0Matt Kaufmann1 Centaur Technology University of Texas at Austin The ACL2 theorem prover is a complex system. Its libraries are vast. Industrial verification efforts may extend this base with hundreds of thousands of lines of additional modeling tools, specifications, and proof scripts. High quality documentation is vital for teams that are working together on projects of this scale. We have developed XDOC, a flexible, scalable documentation tool for ACL2 that can incorporate the documentation for ACL2 itself, the Community Books, and an organization's internal formal verification projects, and which has many features that help to keep the resulting manuals up to date. Using this tool, we have produced a comprehensive, publicly available ACL2+Books Manual that brings better documentation to all ACL2 users. We have also developed an extended manual for use within Centaur Technology that extends the public manual to cover Centaur's internal books. We expect that other organizations using ACL2 will wish to develop similarly extended manuals.http://arxiv.org/pdf/1406.2266v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Jared Davis Matt Kaufmann |
spellingShingle |
Jared Davis Matt Kaufmann Industrial-Strength Documentation for ACL2 Electronic Proceedings in Theoretical Computer Science |
author_facet |
Jared Davis Matt Kaufmann |
author_sort |
Jared Davis |
title |
Industrial-Strength Documentation for ACL2 |
title_short |
Industrial-Strength Documentation for ACL2 |
title_full |
Industrial-Strength Documentation for ACL2 |
title_fullStr |
Industrial-Strength Documentation for ACL2 |
title_full_unstemmed |
Industrial-Strength Documentation for ACL2 |
title_sort |
industrial-strength documentation for acl2 |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2014-06-01 |
description |
The ACL2 theorem prover is a complex system. Its libraries are vast. Industrial verification efforts may extend this base with hundreds of thousands of lines of additional modeling tools, specifications, and proof scripts. High quality documentation is vital for teams that are working together on projects of this scale. We have developed XDOC, a flexible, scalable documentation tool for ACL2 that can incorporate the documentation for ACL2 itself, the Community Books, and an organization's internal formal verification projects, and which has many features that help to keep the resulting manuals up to date. Using this tool, we have produced a comprehensive, publicly available ACL2+Books Manual that brings better documentation to all ACL2 users. We have also developed an extended manual for use within Centaur Technology that extends the public manual to cover Centaur's internal books. We expect that other organizations using ACL2 will wish to develop similarly extended manuals. |
url |
http://arxiv.org/pdf/1406.2266v1 |
work_keys_str_mv |
AT jareddavis industrialstrengthdocumentationforacl2 AT mattkaufmann industrialstrengthdocumentationforacl2 |
_version_ |
1725828281629933568 |