ACL2 2014 PROCEEDINGS: KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A C D E F G H L M N P R S T V W X

A
ACL2	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (PDF, talk) Industrial-Strength Documentation for ACL2 (PDF, talk) Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (PDF, talk) Modeling Algorithms in SystemC and ACL2 (PDF, talk) Development of a Translator from LLVM to ACL2 (PDF, talk)
ACL2(r)	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis (PDF, talk)
arctangent	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent (PDF, talk)
auction strategy	On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics (PDF, talk)
automated reasoning	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (PDF, talk)
automated theorem proving	Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (PDF, talk)
automation	Data Definitions in ACL2 Sedan (PDF, talk)
C
Clustering	ACL2(ml): Machine-Learning for ACL2 (PDF, talk)
concurrency	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory (PDF, talk)
D
Documentation	Industrial-Strength Documentation for ACL2 (PDF, talk)
E
enumerators	Data Definitions in ACL2 Sedan (PDF, talk)
Executable Formal Models	Development of a Translator from LLVM to ACL2 (PDF, talk)
execution	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory (PDF, talk)
F
Formal Verification	Industrial-Strength Documentation for ACL2 (PDF, talk) Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis (PDF, talk)
ForMaRE	On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics (PDF, talk)
Functional instantiation	Polymorphic Types In ACL2 (PDF, talk)
G
Guards	ACL2(ml): Machine-Learning for ACL2 (PDF, talk)
H
hardware verification	Modeling Algorithms in SystemC and ACL2 (PDF, talk)
High Level Synthesis	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis (PDF, talk)
L
LLVM	Development of a Translator from LLVM to ACL2 (PDF, talk)
Loop Pipelining Transformation	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis (PDF, talk)
M
Machine-Learning	ACL2(ml): Machine-Learning for ACL2 (PDF, talk)
mechanized proof	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (PDF, talk)
multiprocessor	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory (PDF, talk)
N
new features	Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (PDF, talk)
non-standard analysis	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis (PDF, talk)
P
pedagogy	Data Definitions in ACL2 Sedan (PDF, talk)
polymorphism	Data Definitions in ACL2 Sedan (PDF, talk) Polymorphic Types In ACL2 (PDF, talk)
polynomial approximations	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent (PDF, talk)
R
real analysis	Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis (PDF, talk)
S
SSA Form	Development of a Translator from LLVM to ACL2 (PDF, talk)
SystemC	Modeling Algorithms in SystemC and ACL2 (PDF, talk)
T
taylor series	Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent (PDF, talk)
test data generation	Data Definitions in ACL2 Sedan (PDF, talk)
theorem proving	Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis (PDF, talk) Development of a Translator from LLVM to ACL2 (PDF, talk)
TPTP	Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (PDF, talk)
type framework	Data Definitions in ACL2 Sedan (PDF, talk)
type system	Polymorphic Types In ACL2 (PDF, talk)
V
Vickrey's theorem	On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics (PDF, talk)
W
weak memory	An ACL2 Mechanization of an Axiomatic Framework for Weak Memory (PDF, talk)
X
XML	Industrial-Strength Documentation for ACL2 (PDF, talk)