VERIFY-2010 Volume Information
Volume:Markus Aderhold, Serge Autexier and Heiko Mantel (editors)
VERIFY-2010. 6th International Verification Workshop

VERIFY-2010 Volume Information

Title:VERIFY-2010. 6th International Verification Workshop
Editors:Markus Aderhold, Serge Autexier and Heiko Mantel
Series:EPiC Series in Computing
Publication date:May 15, 2012


Veronique CortierVerification of Security Protocols1
Cliff JonesAbstractions Before Proofs2
André PlatzerReal Analysis for Complex Systems3
Bernhard Beckert, Daniel Bruns and Sarah GrebingMind the Gap: Formal Verification and the Common Criteria (Discussion Paper)4-12
Mark BickfordAutomated Proof of Authentication Protocols in a Logic of Events13-30
Angelo Brillout, Daniel Kroening, Philipp Rümmer and Thomas WahlProgram Verification via Craig Interpolation for Presburger Arithmetic with Arrays31-46
Alessandro Carioni, Silvio Ghilardi and Silvio RaniseMCMT in the Land of Parametrized Timed Automata47-64
Emanuele Di Rosa, Enrico Giunchiglia, Massimo Narizzano, Gabriele Palma and Alessandra PudduAutomatic generation of high quality test sets via CBMC65-78
Joe Leslie-HurdComposable Packages for Higher Order Logic Theories79-93
Andrei LapetsUser-friendly Support for Common Mathematical Concepts in a Lightweight Verifier94-109
Michael von TessinTowards High-Assurance Multiprocessor Virtualisation110-125
Shuling Wang and Xu WangProving Simpson's Four-Slot Algorithm Using Ownership Transfer126-140
Daniel Wasserrab and Denis LohnerProving Information Flow Noninterference by Reusing a Machine-Checked Correctness Proof for Slicing141-155


1authentication 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