VERIFY-2010:Keyword Index

KeywordPapers
A
Authentication protocolsAutomated Proof of Authentication Protocols in a Logic of Events
automated theorem provingUser-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
automatic test generationAutomatic generation of high quality test sets via CBMC
B
Bounded Model CheckingAutomatic generation of high quality test sets via CBMC
branch coverageAutomatic generation of high quality test sets via CBMC
C
certificationMind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
Common CriteriaMind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
concurrencyProving Simpson's Four-Slot Algorithm Using Ownership Transfer
Craig interpolationProgram Verification via Craig Interpolation for Presburger Arithmetic with Arrays
E
event logicAutomated Proof of Authentication Protocols in a Logic of Events
F
formal proofAutomated Proof of Authentication Protocols in a Logic of Events
formal verificationUser-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
H
higher-order logicComposable Packages for Higher Order Logic Theories
I
Infinite-state model checkingMCMT in the Land of Parametrized Timed Automata
information flow controlProving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
interactive theorem provingTowards High-Assurance Multiprocessor Virtualisation
Isabelle/HOLTowards High-Assurance Multiprocessor Virtualisation
isolationTowards High-Assurance Multiprocessor Virtualisation
L
logicProving Simpson's Four-Slot Algorithm Using Ownership Transfer
M
machine-checked verificationProving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
modularityProving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
O
ownership transferProving Simpson's Four-Slot Algorithm Using Ownership Transfer
P
package managementComposable Packages for Higher Order Logic Theories
Presburger arithmeticProgram Verification via Craig Interpolation for Presburger Arithmetic with Arrays
program verificationMind the Gap: Formal Verification and the Common Criteria (Discussion Paper)
proof reuseProving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
S
safety-critical systemsAutomatic generation of high quality test sets via CBMC
Satisfiability Modulo TheoriesMCMT in the Land of Parametrized Timed Automata
SecurityAutomated Proof of Authentication Protocols in a Logic of Events
seL4 microkernelTowards High-Assurance Multiprocessor Virtualisation
SlicingProving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing
software model checkingProgram Verification via Craig Interpolation for Presburger Arithmetic with Arrays
T
theory developmentComposable Packages for Higher Order Logic Theories
Theory of ArraysProgram Verification via Craig Interpolation for Presburger Arithmetic with Arrays
timed automataMCMT in the Land of Parametrized Timed Automata
tool supportUser-friendly Support for Common Mathematical Concepts in a Lightweight Verifier
V
verificationProving Simpson's Four-Slot Algorithm Using Ownership Transfer
VirtualisationTowards High-Assurance Multiprocessor Virtualisation