Volume •Abstracts •Preface •Authors •Keywords •BibTex Entries

VERIFY-2010: Volume Information

VERIFY-2010. 6th International Verification Workshop

Editors: Markus Aderhold, Serge Autexier and Heiko Mantel

EPiC Series in Computing•Volume 3

13 articles•155 pages•Published: May 15, 2012

Papers

Verification of Security Protocols

Vèronique Cortier

1

Abstractions Before Proofs

2

Real Analysis for Complex Systems

3

Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper)

Bernhard Beckert, Daniel Bruns and Sarah Grebing

4-12

Automated Proof of Authentication Protocols in a Logic of Events

13-30

Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays

Angelo Brillout, Daniel Kroening, Philipp Rümmer and Thomas Wahl

31-46

MCMT in the Land of Parametrized Timed Automata

Alessandro Carioni, Silvio Ghilardi and Silvio Ranise

47-64

Automatic generation of high quality test sets via CBMC

Emanuele Di Rosa, Enrico Giunchiglia, Massimo Narizzano, Gabriele Palma and Alessandra Puddu

65-78

Composable Packages for Higher Order Logic Theories

79-93

User-friendly Support for Common Mathematical Concepts in a Lightweight Verifier

94-109

Towards High-Assurance Multiprocessor Virtualisation

Michael von Tessin

110-125

Proving Simpson's Four-Slot Algorithm Using Ownership Transfer

Shuling Wang and Xu Wang

126-140

Proving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing

Daniel Wasserrab and Denis Lohner

141-155

Keyphrases

Authentication protocols, automated theorem proving, automatic test generation, Bounded Model Checking, branch coverage, certification, Common Criteria, concurrency, Craig interpolation, event logic, formal proof, formal verification, higher-order logic, Infinite-state model checking, information flow control, interactive theorem proving, Isabelle/HOL, isolation, logic, machine-checked verification, modularity, ownership transfer, package management, Presburger arithmetic, program verification, proof reuse, safety-critical systems, Satisfiability Modulo Theories, Security, seL4 microkernel, Slicing, software model checking, theory development, Theory of Arrays, timed automata, tool support, verification, Virtualisation.