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

research-article

C-SHORe: a collapsible approach to higher-order verification

Authors:

Christopher Broadbent,

Arnaud Carayol,

Olivier SerreAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 9

Pages 13 - 24

https://doi.org/10.1145/2544174.2500589

Published: 25 September 2013 Publication History

Abstract

Higher-order recursion schemes (HORS) have recently received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. This paper contributes to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. We introduce the first practical model-checking algorithm that acts on a generalisation of pushdown automata equi-expressive with HORS called collapsible pushdown systems (CPDS). At its core is a substantial modification of a recently studied saturation algorithm for CPDS. In particular it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, we introduce an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We compare our tool with the state-of-the-art verification tools for HORS and obtain encouraging results. In contrast to some of the main competition tackling the same problem, our algorithm is fixed-parameter tractable, and we also offer significantly improved performance over the only previously published tool of which we are aware that also enjoys this property. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.

References

[1]

M. F. Atig. Global model checking of ordered multi-pushdown systems. In FSTTCS, 2010.

[2]

T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In POPL, 2002.

Digital Library

[3]

M. Benois. Parties rationnelles du groupe libre. Comptes-Rendus de l'Acamdemie des Sciences de Paris, Série A, 269:1188--1190, 1969.

[4]

A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, 1997.

Digital Library

[5]

A. Bouajjani and A. Meyer. Symbolic Reachability Analysis of Higher-Order Context-Free Processes. In FSTTCS, 2004.

Digital Library

[6]

C. H. Broadbent, A. Carayol, C.-H. L. Ong, and O. Serre. Recursion schemes and logical reflection. In LICS, 2010.

Digital Library

[7]

C. H. Broadbent, A. Carayol, M. Hague, and O. Serre. A saturation method for collapsible pushdown systems. In ICALP, 2012.

Digital Library

[8]

T. Cachat. Games on Pushdown Graphs and Extensions. PhD thesis, RWTH Aachen, 2003.

[9]

T. Cachat. Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In ICALP, 2003.

Digital Library

[10]

A. Carayol and O. Serre. Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection. In LICS, 2012.

Digital Library

[11]

A. Carayol, M. Hague, A. Meyer, C.-H. L. Ong, and O. Serre. Winning Regions of Higher-Order Pushdown Games. In LICS, 2008.

Digital Library

[12]

J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In CAV, 2000.

Digital Library

[13]

A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In INFINITY, 1997.

[14]

M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis for higher-order pushdown systems. Logical Methods in Computer Science, 4(4), 2008.

[15]

M. Hague and C.-H. L. Ong. Analysing mu-calculus properties of pushdown systems. In SPIN, 2010.

Digital Library

[16]

M. Hague, A. S. Murawski, C.-H. L. Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In LICS, 2008.

Digital Library

[17]

D. Hopkins and C.-H. L. Ong. Homer: A higher-order observational equivalence model checker. In CAV, 2009.

Digital Library

[18]

D. Hopkins, A. S. Murawski, and C.-H. L. Ong. Hector: An equivalence checker for a higher-order fragment of ml. In CAV, 2012.

Digital Library

[19]

R. Jhala, R. Majumdar, and A. Rybalchenko. Hmc: Verifying functional programs using abstract interpreters. In CAV, 2011.

Digital Library

[20]

N. D. Jones and S. S. Muchnick. Even simple programs are hard to analyze. J. ACM, 24:338--350, April 1977.

Digital Library

[21]

T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. In ICALP, 2005.

Digital Library

[22]

N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, 2009.

Digital Library

[23]

N. Kobayashi. Model-checking higher-order functions. In PPDP, 2009.

Digital Library

[24]

N. Kobayashi. Higher-order model checking: From theory to practice. In LICS, 2011.

Digital Library

[25]

N. Kobayashi. A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In FOSSACS, 2011.

Digital Library

[26]

N. Kobayashi. GTRECS2: A model checker for recursion schemes based on games and types. A tool available at http://www-kb.is.s.u-tokyo.ac.jp/~koba/gtrecs2/, 2012.

[27]

N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and cegar for higher-order model checking. In PLDI, 2011.

Digital Library

[28]

R. P. Neatherway, S. J. Ramsay, and C.-H. L. Ong. A traversal-based algorithm for higher-order model checking. In ICFP, 2012.

Digital Library

[29]

C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, 2006.

Digital Library

[30]

C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In POPL, 2011.

Digital Library

[31]

T. W. Reps, S. Schwoon, S. Jha, and D. Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program., 58(1-2):206--263, 2005.

Digital Library

[32]

S. Salvati and I. Walukiewicz. Recursive schemes, krivine machines, and collapsible pushdown automata. In RP, 2012.

Digital Library

[33]

S. Schwoon. Model-checking Pushdown Systems. PhD thesis, Technical University of Munich, 2002.

[34]

M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis, chapter 7, pages 189--234. Prentice-Hall, 1981.

[35]

O. Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie-Mellon University, 1991.

Digital Library

[36]

D. Suwimonteerabuth, S. Schwoon, and J. Esparza. Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In ATVA, 2006.

Digital Library

[37]

D. Suwimonteerabuth, J. Esparza, and S. Schwoon. Symbolic contextbounded analysis of multithreaded java programs. In SPIN, 2008.

Digital Library

[38]

H. Unno, N. Tabuchi, and N. Kobayashi. Verification of treeprocessing programs via higher-order model checking. In APLAS, 2010.

Digital Library

[39]

D. Vardoulakis. CFA2: Pushdown-Flow Analysis for Higher-Order Languages. PhD thesis, Northeastern University, Boston, 2012.

Digital Library

[40]

D. Vardoulakis and O. Shivers. Pushdown flow analysis of first-class control. In ICFP, 2011.

Digital Library

Cited By

Broadbent CCarayol AHague MMurawski AOng CSerre O(2021)Collapsible Pushdown Parity GamesACM Transactions on Computational Logic10.1145/345721422:3(1-51)Online publication date: 28-Jun-2021
https://dl.acm.org/doi/10.1145/3457214
Salvati SWalukiewicz I(2015)Typing Weak MSOL PropertiesFoundations of Software Science and Computation Structures10.1007/978-3-662-46678-0_22(343-357)Online publication date: 2015
https://doi.org/10.1007/978-3-662-46678-0_22
Terao TKobayashi N(2014)A ZDD-Based Efficient Higher-Order Model Checking AlgorithmProgramming Languages and Systems10.1007/978-3-319-12736-1_19(354-371)Online publication date: 2014
https://doi.org/10.1007/978-3-319-12736-1_19
Show More Cited By

Index Terms

C-SHORe: a collapsible approach to higher-order verification
1. Theory of computation
  1. Formal languages and automata theory

Recommendations

C-SHORe: a collapsible approach to higher-order verification
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Higher-order recursion schemes (HORS) have recently received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. This paper ...
Efficient on-the-fly model-checking for regular alternation-free mu-calculus
Special issure on formal methods for industrial critical systems (FMICS 2000)

Model-checking is a successful technique for automatically verifying concurrent finite-state systems. When designing a model-checker, a good compromise must be made between the expressive power of the property description formalism, the complexity of ...
Formal Analysis and Verification of a Multimedia Messaging Service Protocol
CSO '11: Proceedings of the 2011 Fourth International Joint Conference on Computational Sciences and Optimization

this paper reports about the formal analysis and verification of a Multimedia Messaging Service Protocol (MMS) used by NOKIA in its products. We started with the Timed Automata models of the MMS protocol, and then we performed verifications by model-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 48, Issue 9

ICFP '13

September 2013

457 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2544174

Editor:
Mark W. Bailey
Hamilton College, Clinton, NY

Issue’s Table of Contents

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming
September 2013
484 pages
ISBN:9781450323260
DOI:10.1145/2500365
General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Tarmo Uustalu
Institute of Cybernetics at TUT, Estonia

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 the author(s) 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].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2013

Published in SIGPLAN Volume 48, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
139
Total Downloads

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

Reflects downloads up to 23 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Broadbent CCarayol AHague MMurawski AOng CSerre O(2021)Collapsible Pushdown Parity GamesACM Transactions on Computational Logic10.1145/345721422:3(1-51)Online publication date: 28-Jun-2021
https://dl.acm.org/doi/10.1145/3457214
Salvati SWalukiewicz I(2015)Typing Weak MSOL PropertiesFoundations of Software Science and Computation Structures10.1007/978-3-662-46678-0_22(343-357)Online publication date: 2015
https://doi.org/10.1007/978-3-662-46678-0_22
Terao TKobayashi N(2014)A ZDD-Based Efficient Higher-Order Model Checking AlgorithmProgramming Languages and Systems10.1007/978-3-319-12736-1_19(354-371)Online publication date: 2014
https://doi.org/10.1007/978-3-319-12736-1_19
Bruse F(2025)Space-Efficient Model-Checking of Higher-Order Recursion SchemesVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-82700-6_2(29-51)Online publication date: 24-Jan-2025
https://doi.org/10.1007/978-3-031-82700-6_2
Kobayashi NKomendantskaya E(2019)10 Years of the Higher-Order Model Checking Project (Extended Abstract)Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354167(1-2)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1145/3354166.3354167
Terao TSabel DThiemann P(2018)Lazy Abstraction for Higher-Order Program VerificationProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236969(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236969
Genet THaudebourg TJensen T(2018)Verifying Higher-Order Functions with Tree AutomataFoundations of Software Science and Computation Structures10.1007/978-3-319-89366-2_31(565-582)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89366-2_31
Hague MPenelle V(2018)Constrained Dynamic Tree NetworksReachability Problems10.1007/978-3-030-00250-3_4(45-58)Online publication date: 30-Aug-2018
https://doi.org/10.1007/978-3-030-00250-3_4
Clairambault PGrellois CMurawski A(2017)Linearity in higher-order recursion schemesProceedings of the ACM on Programming Languages10.1145/31581272:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158127
Cathcart Burn TOng CRamsay S(2017)Higher-order constrained horn clauses for verificationProceedings of the ACM on Programming Languages10.1145/31580992:POPL(1-28)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158099
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 Issue’s Table of Contents