Formal Methods in System Design

, Volume 42, Issue 3, pp 221–261

Loop summarization using state and transition invariants

  • Daniel Kroening
  • Natasha Sharygina
  • Stefano Tonetta
  • Aliaksei Tsitovich
  • Christoph M. Wintersteiger
Article

DOI: 10.1007/s10703-012-0176-y

Cite this article as:
Kroening, D., Sharygina, N., Tonetta, S. et al. Form Methods Syst Des (2013) 42: 221. doi:10.1007/s10703-012-0176-y

Abstract

This paper presents algorithms for program abstraction based on the principle of loop summarization, which, unlike traditional program approximation approaches (e.g., abstract interpretation), does not employ iterative fixpoint computation, but instead computes symbolic abstract transformers with respect to a set of abstract domains. This allows for an effective exploitation of problem-specific abstract domains for summarization and, as a consequence, the precision of an abstract model may be tailored to specific verification needs. Furthermore, we extend the concept of loop summarization to incorporate relational abstract domains to enable the discovery of transition invariants, which are subsequently used to prove termination of programs. Well-foundedness of the discovered transition invariants is ensured either by a separate decision procedure call or by using abstract domains that are well-founded by construction.

We experimentally evaluate several abstract domains related to memory operations to detect buffer overflow problems. Also, our light-weight termination analysis is demonstrated to be effective on a wide range of benchmarks, including OS device drivers.

Keywords

Program abstraction Loop summarization Loop invariants Transition invariants Termination 

Copyright information

© Springer Science+Business Media New York 2012

Authors and Affiliations

  • Daniel Kroening
    • 1
  • Natasha Sharygina
    • 2
  • Stefano Tonetta
    • 3
  • Aliaksei Tsitovich
    • 2
    • 4
  • Christoph M. Wintersteiger
    • 5
  1. 1.University of OxfordOxfordUK
  2. 2.University of LuganoLuganoSwitzerland
  3. 3.Fondazione Bruno KesslerTrentoItaly
  4. 4.Phonak AGStäfaSwitzerland
  5. 5.Microsoft ResearchCambridgeUK

Personalised recommendations