Journal article icon

Journal article

Loop summarization using state and transition invariants.

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...

Expand abstract
Publication status:
Published

Actions


Access Document


Publisher copy:
10.1007/s10703-012-0176-y

Authors


Kroening, D More by this author
Sharygina, N More by this author
Tonetta, S More by this author
Tsitovich, A More by this author
Wintersteiger, CM More by this author
Journal:
Formal Methods in System Design
Volume:
42
Issue:
3
Pages:
221-261
Publication date:
2013
DOI:
EISSN:
1572-8102
ISSN:
0925-9856
URN:
uuid:523523ea-87d1-4124-983d-0be21d988195
Source identifiers:
406543
Local pid:
pubs:406543

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP