research-article

Quantitative abstraction refinement

Authors:

Thomas A. Henzinger,

Arjun RadhakrishnaAuthors Info & Claims

POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 115 - 128

https://doi.org/10.1145/2429069.2429085

Published: 23 January 2013 Publication History

Abstract

We propose a general framework for abstraction with respect to quantitative properties, such as worst-case execution time, or power consumption. Our framework provides a systematic way for counter-example guided abstraction refinement for quantitative properties. The salient aspect of the framework is that it allows anytime verification, that is, verification algorithms that can be stopped at any time (for example, due to exhaustion of memory), and report approximations that improve monotonically when the algorithms are given more time.

We instantiate the framework with a number of quantitative abstractions and refinement schemes, which differ in terms of how much quantitative information they keep from the original system. We introduce both state-based and trace-based quantitative abstractions, and we describe conditions that define classes of quantitative properties for which the abstractions provide over-approximations. We give algorithms for evaluating the quantitative properties on the abstract systems. We present algorithms for counter-example based refinements for quantitative properties for both state-based and segment-based abstractions. We perform a case study on worst-case execution time of executables to evaluate the anytime verification aspect and the quantitative abstractions we proposed.

Supplementary Material

JPG File (r2d1_talk3.jpg)

Download
18.18 KB

MP4 File (r2d1_talk3.mp4)

Download
194.56 MB

References

[1]

M. Boddy. Anytime problem solving using dynamic programming. In AAAI, pages 738--743, 1991.

Digital Library

[2]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50(5):752--794, 2003.

Digital Library

[3]

J. Cochet-Terrasson, G. Cohen, S. Gaubert, M. McGettrick, and J.-P. Quadrat. Numerical computation of spectral elements in max-plus algebra, 1998.

[4]

B. Cook, A. Podelski, and A. Rybalchenko. Abstraction refinement for termination. In SAS, pages 87--101, 2005.

Digital Library

[5]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252, 1977.

Digital Library

[6]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL, pages 269--282, 1979.

Digital Library

[7]

P. Cousot and R. Cousot. An abstract interpretation framework for termination. In POPL, pages 245--258, 2012.

Digital Library

[8]

L. de Alfaro and P. Roy. Magnifying-lens abstraction for Markov decision processes. In CAV, pages 325--338, 2007.

Digital Library

[9]

C. Ferdinand, F. Martin, R. Wilhelm, and M. Alt. Cache behavior prediction by abstract interpretation. Sci. Comput. Program., 35(2):163--189, 1999.

Digital Library

[10]

S. Gulwani and F. Zuleger. The reachability-bound problem. In PLDI, pages 292--304, 2010.

Digital Library

[11]

J. Gustafsson, A. Betts, A. Ermedahl, and B. Lisper. The m\"alardalen WCET benchmarks: Past, present and future. In WCET, pages 136--146, 2010.

[12]

H. Hermanns, B. Wachter, and L. Zhang. Probabilistic CEGAR. In CAV, pages 162--175, 2008.

Digital Library

[13]

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker. Abstraction refinement for probabilistic software. In VMCAI, pages 182--197, 2009.

Digital Library

[14]

A. Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. In POPL, pages 132--144, 2005.

Digital Library

[15]

A. Prantl, M. Schordan, and J. Knoop. TuBound - a conceptually new tool for worst-case execution time analysis. In WCET, 2008.

[16]

N. Shankar. A tool bus for anytime verification. Usable Verification, 2010.

[17]

V. Tiwari, S. Malik, and A. Wolfe. Power analysis of embedded software: a first step towards software power minimization. In ICCAD, pages 384--390, 1994.

Digital Library

[18]

R. Wilhelm, S. Altmeyer, C. Burguière, D. Grund, J. Herter, J. Reineke, B. Wachter, and S. Wilhelm. Static timing analysis for hard real-time systems. In VMCAI, pages 3--22, 2010.

Digital Library

[19]

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing, D. Whalley, G. Bernat, C. Ferdinand, R. Heckmann, T. Mitra, F. Mueller, I. Puaut, P. Puschner, J. Staschulat, and P. Stenström. The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst., 7(3), 2008.

Digital Library

Cited By

Chatterjee KIbsen-Jensen RPavlogiannis A(2021)Faster algorithms for quantitative verification in bounded treewidth graphsFormal Methods in System Design10.1007/s10703-021-00373-5Online publication date: 29-Apr-2021
https://doi.org/10.1007/s10703-021-00373-5
Chatterjee KIbsen-Jensen RGoharshady APavlogiannis A(2018)Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth ComponentsACM Transactions on Programming Languages and Systems10.1145/321025740:3(1-43)Online publication date: 5-Jul-2018
https://dl.acm.org/doi/10.1145/3210257
Chatterjee KGoharshady AVelner Y(2018)Quantitative Analysis of Smart ContractsProgramming Languages and Systems10.1007/978-3-319-89884-1_26(739-767)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_26
Show More Cited By

Index Terms

Quantitative abstraction refinement

Recommendations

Quantitative abstraction refinement
POPL '13

We propose a general framework for abstraction with respect to quantitative properties, such as worst-case execution time, or power consumption. Our framework provides a systematic way for counter-example guided abstraction refinement for quantitative ...
A counterexample-guided abstraction-refinement framework for markov decision processes

The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of counterexample guided abstraction refinement (CEGAR), wherein one ...
Abstraction for model checking multi-agent systems

Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2013

586 pages

ISBN:9781450318327

DOI:10.1145/2429069

General Chair:
Roberto Giacobazzi
Università di Verona, Italy
,
Program Chair:
Radhia Cousot
École normale supérieure CNRS & INRIA, France

ACM SIGPLAN Notices Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '13

Sponsor:

SIGPLAN

POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 23 - 25, 2013

Rome, Italy

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
542
Total Downloads

Downloads (Last 12 months)15
Downloads (Last 6 weeks)2

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chatterjee KIbsen-Jensen RPavlogiannis A(2021)Faster algorithms for quantitative verification in bounded treewidth graphsFormal Methods in System Design10.1007/s10703-021-00373-5Online publication date: 29-Apr-2021
https://doi.org/10.1007/s10703-021-00373-5
Chatterjee KIbsen-Jensen RGoharshady APavlogiannis A(2018)Algorithms for Algebraic Path Properties in Concurrent Systems of Constant Treewidth ComponentsACM Transactions on Programming Languages and Systems10.1145/321025740:3(1-43)Online publication date: 5-Jul-2018
https://dl.acm.org/doi/10.1145/3210257
Chatterjee KGoharshady AVelner Y(2018)Quantitative Analysis of Smart ContractsProgramming Languages and Systems10.1007/978-3-319-89884-1_26(739-767)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_26
Nagar KSrikant Y(2017)Refining Cache Behavior Prediction Using Cache Miss PathsACM Transactions on Embedded Computing Systems10.1145/303554116:4(1-26)Online publication date: 11-May-2017
https://dl.acm.org/doi/10.1145/3035541
Knoop JKovács LZwirchmayr J(2017)Replacing conjectures by positive knowledgeJournal of Symbolic Computation10.1016/j.jsc.2016.07.02380:P1(101-124)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jsc.2016.07.023
Olaechea RFahrenberg UAtlee JLegay AMei H(2016)Long-term average cost in featured transition systemsProceedings of the 20th International Systems and Software Product Line Conference10.1145/2934466.2934473(109-118)Online publication date: 16-Sep-2016
https://dl.acm.org/doi/10.1145/2934466.2934473
Chatterjee KGoharshady AIbsen-Jensen RPavlogiannis A(2016)Algorithms for algebraic path properties in concurrent systems of constant treewidth componentsACM SIGPLAN Notices10.1145/2914770.283762451:1(733-747)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837624
Chatterjee KGoharshady AIbsen-Jensen RPavlogiannis ABodik RMajumdar R(2016)Algorithms for algebraic path properties in concurrent systems of constant treewidth componentsProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837624(733-747)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837624
Chatterjee KPavlogiannis AVelner Y(2015)Quantitative Interprocedural AnalysisACM SIGPLAN Notices10.1145/2775051.267696850:1(539-551)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2775051.2676968
Chatterjee KPavlogiannis AVelner YRajamani SWalker D(2015)Quantitative Interprocedural AnalysisProceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2676726.2676968(539-551)Online publication date: 14-Jan-2015
https://dl.acm.org/doi/10.1145/2676726.2676968
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents