Talk Keyword Index

TALK KEYWORD INDEX

This page contains an index consisting of author-provided keywords.

Shortcuts: A B C D F G H I L M N O P R S T

A
ACL2	Second-Order Functions and Theorems in ACL2 A Brief Introduction to Oracle’s Use of ACL2 Reasoning about LLVM code using Codewalker Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
ACL2(r)	Fourier Series Formalization in ACL2(r)
automatic functional instantiation	Second-Order Functions and Theorems in ACL2
B
byte-addressed memory	Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
C
clause processors	Extending ACL2 with SMT Solvers
Codewalker	Reasoning about LLVM code using Codewalker
compiler transformation	Proving Skipping Refinement with ACL2s
Connecting ACL2 with other systems: SMT solvers	Extending ACL2 with SMT Solvers
convergence	Perfect Numbers in ACL2
D
decision procedures: real arithmetic	Extending ACL2 with SMT Solvers
Decompilation into logic	Reasoning about LLVM code using Codewalker
F
fixing functions	Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
formal methods	A Brief Introduction to Oracle’s Use of ACL2
Fourier series formalization	Fourier Series Formalization in ACL2(r)
function variables	Second-Order Functions and Theorems in ACL2
G
guards	Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
H
hardware verification	A Brief Introduction to Oracle’s Use of ACL2
Hardware verification: analog/mixed-signal	Extending ACL2 with SMT Solvers
I
Infinite series	Fourier Series Formalization in ACL2(r)
L
LLVM	Reasoning about LLVM code using Codewalker
M
memoization	Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
memory controller	Proving Skipping Refinement with ACL2s
N
Non-standard analysis	Fourier Series Formalization in ACL2(r)
O
operational semantics	Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
Overspill principle	Fourier Series Formalization in ACL2(r)
P
perfect numbers	Perfect Numbers in ACL2
program refinement	Second-Order Functions and Theorems in ACL2
R
reactive systems	Proving Skipping Refinement with ACL2s
Real analysis	Fourier Series Formalization in ACL2(r)
refinement	Proving Skipping Refinement with ACL2s
S
second-order logic	Second-Order Functions and Theorems in ACL2
series	Perfect Numbers in ACL2
Software verification	Reasoning about LLVM code using Codewalker
symbolic execution	Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
T
theorem proving	A Brief Introduction to Oracle’s Use of ACL2
type reasoning	Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
type safety	Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning