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 |