Bound Analysis of Imperative Programs with the Size-change Abstraction (extended version)

2012/03/23 by Florian Zuleger, Zuleger, Florian, Sumit Gulwani +5 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Testing and Debugging Techniques

paper · pdf · doi:10.48550/arxiv.1203.5303

openalex publication_date 2012/03/23 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28

Abstract

The size-change abstraction (SCA) is an important program abstraction for termination analysis, which has been successfully implemented in many tools for functional and logic programs. In this paper, we demonstrate that SCA is also a highly effective abstract domain for the bound analysis of imperative programs. We have implemented a bound analysis tool based on SCA for imperative programs. We abstract programs in a pathwise and context dependent manner, which enables our tool to analyze real-world programs effectively. Our work shows that SCA captures many of the essential ideas of previous termination and bound analysis and goes beyond in a conceptually simpler framework.

Citations

• Software Model Checking via Large-Block Encoding

Cited by

• On the Value and Limits of Multi-level Energy Consumption Static Analysis for Deeply Embedded Single and Multi-threaded Programs

Related

• Improving Size-Change Analysis in Offline Partial Evaluation
• Size-change termination with difference constraints
• Improving Automatic Complexity Analysis of Integer Programs
• Analysis of Equality Relationships for Imperative Programs
• Difference Constraints: An adequate Abstraction for Complexity Analysis\n of Imperative Programs