List of Accepted Papers

Fares Fraij and Steve Roach. Proof of Transitive Closure Property of Directed Acyclic Graphs
Rex Page. Computational Logic in the Undergraduate Curriculum
John Cowles and Ruben Gamboa. \triangle = \square
J Moore. Automatically Computing Functional Instantiations
Laurence Pierre, Renaud Clavel and Regis Leveugle. ACL2 for the Verification of Fault-Tolerance Properties: First Results
Matt Kaufmann, Jacob Kornerup and Mark Reitblatt. Formal Verification of LabVIEW Programs Using the ACL2 Theorem Prover
Ryan Ralston. ACL2-Certified AVL Trees
Freek Verbeek and julien schmaltz. Formal Validation of Deadlock Prevention in Networks-on-Chips
Tom van den Broek and julien schmaltz. A Generic Implementation Model for the Formal Verification of Networks-on-Chips
Antonio Garcia-Dominguez, Francisco Palomo-Lozano and Inmaculada Medina-Bulo. Hypertext Navigation of ACL2 Proofs with XMLEye
David Greve. Automated Reasoning With Quantified Formulae
David Greve. Assuming Termination
Robert Sumners. User Control and Direction of a More Efficient Simplifier in ACL2
David Rager. An Executable Model for Security Protocol JFKr
Robert S. Boyer and Warren A. Hunt, Jr.. Symbolic Simulation in ACL2
Ruben Gamboa and John Cowles. Inverse Functions in ACL2(r)
Matt Kaufmann. Abbreviated Output for Input in ACL2
Hanbing Liu. Proving A Specific Type Of Inequality Theorems in ACL2: a bind-free experience report
David Hardin and Samuel Hardin. Efficient, Formally VeriŽable Data Structures using ACL2 Single-Threaded Objects for High-Assurance Systems
Carl Eastlund. DoubleCheck Your Theorems
Carl Eastlund and Matthias Felleisen. Automatically Verified GUI Programs