VERIFY-2010: Keyword Index

Keyword	Papers
a
Authentication protocols	Automated Proof of Authentication Protocols in a Logic of Events
automated theorem proving	User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
automatic test generation	Automatic generation of high quality test sets via CBMC
b
Bounded Model Checking	Automatic generation of high quality test sets via CBMC
branch coverage	Automatic generation of high quality test sets via CBMC
c
certification	Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
Common Criteria	Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
concurrency	Proving Simpson's Four-Slot Algorithm Using Ownership Transfer
Craig interpolation	Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
e
event logic	Automated Proof of Authentication Protocols in a Logic of Events
f
formal proof	Automated Proof of Authentication Protocols in a Logic of Events
formal verification	User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
h
higher-order logic	Composable Packages for Higher Order Logic Theories
i
Infinite-state model checking	MCMT in the Land of Parametrized Timed Automata
information flow control	Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
interactive theorem proving	Towards High-Assurance Multiprocessor Virtualisation
Isabelle/HOL	Towards High-Assurance Multiprocessor Virtualisation
isolation	Towards High-Assurance Multiprocessor Virtualisation
l
logic	Proving Simpson's Four-Slot Algorithm Using Ownership Transfer
m
machine-checked verification	Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
modularity	Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
o
ownership transfer	Proving Simpson's Four-Slot Algorithm Using Ownership Transfer
p
package management	Composable Packages for Higher Order Logic Theories
Presburger arithmetic	Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
program verification	Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
proof reuse	Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
s
safety-critical systems	Automatic generation of high quality test sets via CBMC
Satisfiability Modulo Theories	MCMT in the Land of Parametrized Timed Automata
Security	Automated Proof of Authentication Protocols in a Logic of Events
seL4 microkernel	Towards High-Assurance Multiprocessor Virtualisation
Slicing	Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
software model checking	Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
t
theory development	Composable Packages for Higher Order Logic Theories
Theory of Arrays	Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays
timed automata	MCMT in the Land of Parametrized Timed Automata
tool support	User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
v
verification	Proving Simpson's Four-Slot Algorithm Using Ownership Transfer
Virtualisation	Towards High-Assurance Multiprocessor Virtualisation