Tests and Proofs

1. Front Matter

   PDF

2. Model-Based Mutation Testing of an Industrial Measurement Device

   • Bernhard K. Aichernig, Jakob Auer, Elisabeth Jöbstl, Robert Korošec, Willibald Krenn, Rupert Schlick et al.

   Pages 1-19

3. Computing with an SMT Solver

   • Nada Amin, K. Rustan M. Leino, Tiark Rompf

   Pages 20-35

4. An Abstraction Technique for Testing Decomposable Systems by Model Checking

   • Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene

   Pages 36-52

5. An All-in-One Toolkit for Automated White-Box Testing

   • Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov

   Pages 53-60

6. Behaviour Driven Development for Tests and Verification

   • Melanie Diepenbeck, Ulrich Kühne, Mathias Soeken, Rolf Drechsler

   Pages 61-77

7. Quality Assurance in MBE Back and Forth

   • Sebastian Gabmeyer

   Pages 78-81

8. Visualizing Unbounded Symbolic Execution

   • Martin Hentschel, Reiner Hähnle, Richard Bubel

   Pages 82-98

9. Filmstripping and Unrolling: A Comparison of Verification Approaches for UML and OCL Behavioral Models

   • Frank Hilken, Philipp Niemann, Martin Gogolla, Robert Wille

   Pages 99-116

10. Generating Classified Parallel Unit Tests

    • Ali Jannesari, Nico Koprowski, Jochen Schimmel, Felix Wolf

    Pages 117-133

11. JTACO: Test Execution for Faster Bounded Verification

    • Alexander Kampmann, Juan Pablo Galeotti, Andreas Zeller

    Pages 134-141

12. Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification

    • Johannes Kanig, Rod Chapman, Cyrille Comar, Jerôme Guitton, Yannick Moy, Emyr Rees

    Pages 142-157

13. A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing

    • Nikolai Kosmatov, Matthieu Lemerre, Céline Alec

    Pages 158-164

14. Runtime Assertion Checking and Its Combinations with Static and Dynamic Analyses

    • Nikolai Kosmatov, Julien Signoles

    Pages 165-168

15. Generating Test Data from a UML Activity Using the AMPL Interface for Constraint Solvers

    • Felix Kurth, Sibylle Schupp, Stephan Weißleder

    Pages 169-186

16. Lightweight State Capturing for Automated Testing of Multithreaded Programs

    • Kari Kähkönen, Keijo Heljanko

    Pages 187-203

17. How Test Generation Helps Software Specification and Deductive Verification in Frama-C

    • Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand

    Pages 204-211

18. Back Matter

    PDF

This book constitutes the refereed proceedings of the 8th International Conference on Tests and Proofs, TAP 2014, held in York, UK, in July 2014, as part of the STAF 2014 Federated Conferences. The 10 revised full papers and 4 short papers presented together with two tutorial descriptions were carefully reviewed and selected from 27 submissions. The papers cover topics in the following four research areas: test generation, bridging semantic gaps, integrated development processes and bounded verification.

• UML
• assertion checking
• formal methods
• program analysis
• program verification
• software testing and debugging
• specification languages
• static analysis

• Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria

  Martina Seidl

• One Microsoft Way, Microsoft Research, Redmond, USA

  Nikolai Tillmann

Policies and ethics