Reasoning about ACL2 File Input

Unicode ACL2 File Input

This is an ACL2 library for reasoning about the file input routines, particularly read-byte$. It also allows you to efficiently read UTF-8 files.

This library is free software released under the terms of the GNU General Public License.

Download

Download Version 0.3
GZipped Tar File; 55 KB
Note: You may already have this library installed. It is distributed in the books/unicode directory of ACL2 3.0.

Documentation

PDF Reasoning about ACL2 File Input
To appear in ACL2 '06
PDF; 109 KB

Presentations

Movie ACL2 '06 Movie
WMV; 37 MB; 26 Minutes
PDF ACL2 '06 Slides
PDF; 600 KB

Source Code

Code Browse Source (Stable version)
This is just an Apache file listing.