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 |