© 2015

Validation of Evolving Software

  • Hana Chockler
  • Daniel Kroening
  • Leonardo Mariani
  • Natasha Sharygina

Table of contents

  1. Front Matter
    Pages i-viii
  2. Introduction

    1. Front Matter
      Pages 1-1
    2. Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
      Pages 3-5
    3. Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
      Pages 7-17
    4. Hana Chockler, Daniel Kroening, Leonardo Mariani, Natasha Sharygina
      Pages 19-21
  3. Static Analysis

    1. Front Matter
      Pages 23-23
    2. Hana Chockler, Sitvanit Ruah
      Pages 25-36
    3. Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
      Pages 37-53
    4. Ondrej Sery, Grigory Fedyukovich, Natasha Sharygina
      Pages 55-72
    5. Simone Fulvio Rollini, Leonardo Alt, Grigory Fedyukovich, Antti Eero Johannes Hyvärinen, Natasha Sharygina
      Pages 73-82
  4. Dynamic Analysis

    1. Front Matter
      Pages 83-83
    2. Fabrizio Pastore, Leonardo Mariani, Alberto Goffi, Manuel Oriol, Michael Wahler
      Pages 85-105
    3. Leonardo Mariani, Oliviero Riganelli, Mauro Santoro, Ali Muhammad
      Pages 107-121
  5. Common Preprocessing and Hybrid Analysis

    1. Front Matter
      Pages 123-123
    2. Ajitha Rajan, Daniel Kroening
      Pages 125-145
    3. Pietro Braione, Giovanni Denaro, Oliviero Riganelli, Mauro Baluda, Ali Muhammad
      Pages 147-184
    4. Fabrizio Pastore, Leonardo Mariani, Antti Eero Johannes Hyvärinen, Grigory Fedyukovich, Natasha Sharygina, Stephan Sehestedt et al.
      Pages 185-207
  6. Back Matter
    Pages 209-220

About this book


This book describes the methodology and accompanying technology for reducing the costs of validation of changes by introducing automatic techniques to analyze and test software increments. It builds a unified approach to efficient and reliable validation of changes and upgrades, and may be used as a research monograph and a reference book.


Efficient Validation Evolving Software Formal Methods Hybrid Techniques Incremental Validation Testing Validation

Editors and affiliations

  • Hana Chockler
    • 1
  • Daniel Kroening
    • 2
  • Leonardo Mariani
    • 3
  • Natasha Sharygina
    • 4
  1. 1.Dept. of InformaticsKing's CollegeLondonUnited Kingdom
  2. 2.Dept. of Computer ScienceUniversity of OxfordOxfordUnited Kingdom
  3. 3.DISCoUniversity of Milan BicoccaMilanoItaly
  4. 4.Dept. of InformaticsUniv. della Svizzera ItalianaLuganoSwitzerland

About the editors

Dr. Hana Chockler received her Ph.D. in Computer Science from the Hebrew University of Jerusalem in 2003. She is a member of the Software Modelling and Applied Logic Group in King's College, London, UK; she previously worked in the formal methods group at IBM Haifa Research Labs. She has particular expertise in coverage metrics and their extension to quality metrics; her broader research interests include formal verification, model-checking of hardware and software; coverage and vacuity in formal verification; causality, responsibility and its relation to formal methods; explanation of counterexamples and the cross-entropy method for testing.

Prof. Daniel Kroening received his Ph.D. in Computer Science from Saarland University in 2001. He was an assistant professor at ETH Zurich in 2004–2007, he is now a professor in the Dept. of Computer Science at the University of Oxford. His areas of interest include model checking, decision procedures and software analysis. A feature of his work is frequent interaction with industrial partners, such as Microsoft Research, Intel Research, Toyota Motors, Ford, and Airbus UK.

Dr. Leonardo Mariani received his Ph.D. in Computer Science at the University of Milano Bicocca in 2005, where he is currently a researcher, collaborating with the Laboratory of Test and Analysis. His research interests include the test and analysis of component-based systems, inference of behavioural models, dynamic analysis, test and analysis of service-based applications, design of self-healing solutions and the design and development of autonomous and adaptive systems.

Prof. Natasha Sharygina received her Ph.D. from the University of Texas at Austin. She is the head of the Formal Verification lab at the University of Lugano (USI) and an adjunct professor at Carnegie Mellon University. She is an expert in the field of formal verification, static analysis and system design. Her lab creates both theoretical frameworks and practical tools to enable sound, scalable verification of industrial-size systems and they collaborate with industrial partners such as IBM Haifa, Cadence, Intel and ABB.

Bibliographic information

  • Book Title Validation of Evolving Software
  • Editors Hana Chockler
    Daniel Kroening
    Leonardo Mariani
    Natasha Sharygina
  • DOI
  • Copyright Information Springer International Publishing Switzerland 2015
  • Publisher Name Springer, Cham
  • eBook Packages Computer Science Computer Science (R0)
  • Hardcover ISBN 978-3-319-10622-9
  • Softcover ISBN 978-3-319-38200-5
  • eBook ISBN 978-3-319-10623-6
  • Edition Number 1
  • Number of Pages VIII, 220
  • Number of Illustrations 32 b/w illustrations, 28 illustrations in colour
  • Topics Software Engineering
    Logics and Meanings of Programs
  • Buy this book on publisher's site
Industry Sectors
Chemical Manufacturing
IT & Software
Consumer Packaged Goods
Finance, Business & Banking
Energy, Utilities & Environment