More Web Proxy on the site http://driver.im/

Article

Programs with lists are counter automata

Authors:

Ahmed Bouajjani,

Peter Habermehl,

Tomáš VojnarAuthors Info & Claims

CAV'06: Proceedings of the 18th international conference on Computer Aided Verification

Pages 517 - 531

https://doi.org/10.1007/11817963_47

Published: 17 August 2006 Publication History

Abstract

We address the verification problem of programs manipulating one-selector linked data structures. We propose a new automated approach for checking safety and termination for these programs. Our approach is based on using counter automata as accurate abstract models: control states correspond to abstract heap graphs where list segments without sharing are collapsed, and counters are used to keep track of the number of elements in these segments. This allows to apply automatic analysis techniques and tools for counter automata in order to verify list programs. We show the effectiveness of our approach, in particular by verifying automatically termination of some sorting programs.

References

[1]

The LASH toolset. http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.

[2]

A. Bouajjani A. Annichini and M. Sighireanu. TReX: A Tool for Reachability Analysis of Complex Systems. In Proc. of CAV'01, volume 2102 of LNCS, 2001.

Digital Library

[3]

I. Balaban, A. Pnueli, and L. Zuck. Shape Analysis by Predicate Abstraction. In Proc. of VMCAI'05, volume 3385 of LNCS, 2005.

Digital Library

[4]

S. Bardin, A. Finkel, and D. Nowak. Toward Symbolic Verification of Programs Handling Pointers. In Proc. of AVIS'04, 2004.

[5]

S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: Fast Acceleration of Symbolic Transition systems. In Proc. of CAV'03, volume 2725 of LNCS, 2003.

[6]

J. Berdine, C. Calcagno, and P. O'Hearn. A Decidable Fragment of Separation Logic. In Proc. of FSTTCS'04, volume 3328 of LNCS, 2004.

Digital Library

[7]

A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with Lists are Counter Automata. Tech. Rep. TR-2006-3, Verimag, UJF/CNRS/INPG, Grenoble, 2006.

Digital Library

[8]

A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying Programs with Dynamic 1- Selector-Linked Structures in Regular Model Checking. In Proc. of TACAS'05, volume 3440 of LNCS, 2005.

Digital Library

[9]

A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract Regular Model Checking. In Proc. of CAV'04, volume 3114 of LNCS, 2004.

[10]

M. Bozga and R. Iosif. Quantitative Verification of Programs with Lists. VERIMAG TR- 2005-2, http://www-verimag.imag.fr, 2005.

[11]

A. Bradley, Z. Manna, and H. Sipma. Termination Analysis of Integer Linear Loops. In Proc. of CONCUR'05, volume 3653 of LNCS, 2005.

Digital Library

[12]

B. Cook, A. Podelski, and A. Rybalchenko. Abstraction Refinement for Termination. In Proc. of SAS'05, volume 3672 of LNCS, 2005.

Digital Library

[13]

P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of POPL'97, 1977.

Digital Library

[14]

N. Dor, M. Rodeh, and S. Sagiv. Checking Cleanness in Linked Lists. In Proc. of SAS'00, volume 1824 of LNCS, 2000.

Digital Library

[15]

A. Finkel, 2006. Personal communication.

[16]

R. Iosif. Symmetry Reductions forModel Checking of Concurrent Dynamic Software. STTT, pages 302-319, 2004.

[17]

S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In Proc. of POPL'01, 2001.

Digital Library

[18]

R. Manevich, E. Yahav, G. Ramalingam, and M. Sagiv. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In Proc. of VMCAI'05, volume 3385 of LNCS, 2005.

Digital Library

[19]

A. Møller and M.I. Schwartzbach. The Pointer Assertion Logic Engine. In Proc. of PLDI'01. ACM Press, 2001.

Digital Library

[20]

M. Presburger. Über die Vollstandigkeit eines Gewissen Systems der Arithmetik. Comptes Rendus du I Congrés des Pays Slaves, 1929.

[21]

S. Sagiv, T.W. Reps, and R. Wilhelm. Parametric Shape Analysis via 3-Valued Logic. TOPLAS, 2002.

Digital Library

[22]

E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm. Verifying Temporal Heap Properties Specified via Evolution Logic. In Proc. of ESOP'03, volume 2618 of LNCS, 2003.

Digital Library

Cited By

Kanvar VKhedker U(2016)Heap Abstractions for Static AnalysisACM Computing Surveys10.1145/293109849:2(1-47)Online publication date: 30-Jun-2016
https://dl.acm.org/doi/10.1145/2931098
Leroux JRümmer PSubotić P(2016)Guiding Craig interpolation with domain-specific abstractionsActa Informatica10.1007/s00236-015-0236-z53:4(387-424)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1007/s00236-015-0236-z
Ganjei ZRezine AEles PPeng Z(2016)Lazy Constrained Monotonic AbstractionProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_7(147-165)Online publication date: 17-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-662-49122-5_7
Show More Cited By

Recommendations

Programs with lists are counter automata

We address the problem of verifying programs manipulating one-selector linked data structures. We propose and study in detail an application of counter automata as an accurate abstract model for this problem. We let control states of the counter ...
Quantum versus deterministic counter automata

This paper focuses on quantum analogues of various models of counter automata, and almost completely proves the relation between the classes of languages recognizable by bounded error quantum ones and classical deterministic ones in every model of ...
Flat Parametric Counter Automata
Machines, Computations and Universality, Part II

In this paper we study the reachability problem for parametric flat counter automata, in relation with the satisfiability problem of three fragments of integer arithmetic. The equivalence between non-parametric flat counter automata and Presburger ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV'06: Proceedings of the 18th international conference on Computer Aided Verification

August 2006

563 pages

ISBN:354037406X

Editors:
Thomas Ball
Microsoft Research, Redmond, WA,
,
Robert B. Jones
Intel Corporation, RA2-459, 2501 W. 229th Avenue, Hillsboro, OR,

Sponsors

INTEL: Intel Corporation
NEC
Cadence Design Systems
Microsoft Research: Microsoft Research
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 17 August 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

47
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kanvar VKhedker U(2016)Heap Abstractions for Static AnalysisACM Computing Surveys10.1145/293109849:2(1-47)Online publication date: 30-Jun-2016
https://dl.acm.org/doi/10.1145/2931098
Leroux JRümmer PSubotić P(2016)Guiding Craig interpolation with domain-specific abstractionsActa Informatica10.1007/s00236-015-0236-z53:4(387-424)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1007/s00236-015-0236-z
Ganjei ZRezine AEles PPeng Z(2016)Lazy Constrained Monotonic AbstractionProceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 958310.1007/978-3-662-49122-5_7(147-165)Online publication date: 17-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-662-49122-5_7
Cook BFuhs CNimkar KO'Hearn PJobstmann B(2014)Disproving termination with overapproximationProceedings of the 14th Conference on Formal Methods in Computer-Aided Design10.5555/2682923.2682941(67-74)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.5555/2682923.2682941
Bozga MIosif RKoneăźNý F(2014)Safety Problems Are NP-complete for Flat Integer Programs with Octagonal LoopsProceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 831810.1007/978-3-642-54013-4_14(242-261)Online publication date: 19-Jan-2014
https://dl.acm.org/doi/10.1007/978-3-642-54013-4_14
Cook BKoskinen E(2013)Reasoning about nondeterminism in programsACM SIGPLAN Notices10.1145/2499370.249196948:6(219-230)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2499370.2491969
Cook BKoskinen EBoehm HFlanagan C(2013)Reasoning about nondeterminism in programsProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2491956.2491969(219-230)Online publication date: 16-Jun-2013
https://dl.acm.org/doi/10.1145/2491956.2491969
Parízek PLhoták O(2012)Predicate abstraction of Java programs with collectionsACM SIGPLAN Notices10.1145/2398857.238462347:10(75-94)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384623
Parízek PLhoták OLeavens GDwyer M(2012)Predicate abstraction of Java programs with collectionsProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384623(75-94)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384623
Hojjat HIosif RKonečný FKuncak VRümmer P(2012)Accelerating interpolantsProceedings of the 10th international conference on Automated Technology for Verification and Analysis10.1007/978-3-642-33386-6_16(187-202)Online publication date: 3-Oct-2012
https://dl.acm.org/doi/10.1007/978-3-642-33386-6_16
Show More Cited By

View Options

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

Media

Figures

Other

Tables

View Table of Contents