Article

Proof-guided underapproximation-widening for multi-process systems

Authors:

Ofer Strichman,

Michael TheobaldAuthors Info & Claims

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 122 - 131

https://doi.org/10.1145/1040305.1040316

Published: 12 January 2005 Publication History

Abstract

This paper presents a procedure for the verification of multi-process systems based on considering a series of underapproximated models. The procedure checks models with an increasing set of allowed interleavings of the given set of processes, starting from a single interleaving. The procedure relies on SAT solvers' ability to produce proofs of unsatisfiability: from these proofs it derives information that guides the process of adding interleavings on the one hand, and determines termination on the other. The presented approach is integrated in a SAT-based Bounded Model Checking (BMC) framework. Thus, a BMC formulation of a multi-process system is introduced, which allows controlling which interleavings are considered. Preliminary experimental results demonstrate the practical impact of the presented method.

References

[1]

R. Alur, R. Brayton, T. A. Henzinger, S. Quadeer, and S. Rajamani. Partial-order reduction in symbolic state space exploration. In O. Grumberg, editor, Proc. of the 9th conference on Computer-Aided Verification (CAV'97), volume 1254 of LNCS, pages 340--351, Haifa, June 1997.]]

Digital Library

[2]

N. Amla and K. McMillan. Automatic abstraction without counterexamples. In H. Garavel and J. Hatcliff, editors, 9th Intl. Conf. on Tools And Algorithms For The Construction And Analysis Of Systems (TACAS'03), volume 2619 of Lect. Notes in Comp. Sci., 2003.]]

Digital Library

[3]

F. Balarin and A. Sangiovanni-Vinventelli. An iterative approah to language containment. In C. Courcoubetis, editor, Proc. 5th Intl. Conference on Computer Aided Verification (CAV'94), volume 697 of Lect. Notes in Comp. Sci., pages 29--40. Springer-Verlag, 1993.]]

Digital Library

[4]

S. Barner, D. Geist, and A. Gringauze. Symbolic localization reduction with reconstruction layering and backtr acking. In Proc. of Conference on Computer-Aided Verification (CAV), Copenhagen, Denmark, July 2002.]]

Digital Library

[5]

S. Barner and O. Grumberg. Combining symmetry reduction and upper-approximation for symbolic model checking. In 14th International Conference on Computer Aided Verification (CAV'02), volume 2404 of LNCS, Copenhagen, Denmark, July 2002.]]

Digital Library

[6]

A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zue. Bounded Model Checking, volume~58 of Advances in computers. Academic Press, 2003.]]

[7]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Design Automation Conference (DAC'99), 1999.]]

Digital Library

[8]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Yhu. Symbolic model checking without BDDs. In Tools and Algorithms for Construction and Analysis of Systems, pages 193--207, 1999.]]

Digital Library

[9]

P. Chauhan, E. Clarke, J. Kukula, S. Sapra, H. Veith, and D. Wang. Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In A. O'Leary, editor, Fourth International Conference on Formal Methods in Computer-Aided Design (FMCAD'02), lncs, Portland, Oregon, Nov 2002.]]

Digital Library

[10]

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

Digital Library

[11]

E. Clarke, A. Gupta, J. Kukula, and O. Strichman. SAT based abstraction - refinement using ILP and machine learning techniques. In E. Brinksma and K. Larsen, editors, Proc. 14th Intl. Conference on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 265--279, Copenhagen, Denmark, July 2002. Springer-Verlag.]]

Digital Library

[12]

E. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. Completeness and complexity of bounded model checking. In Proc. 5th Intl. Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), volume 2937 of Lect. Notes in Comp. Sci., pages 85--96, Venice, Italy, Jan 2004.]]

[13]

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In E. A. Emerson and A. P. Sistla, editors, Proc. 12th Intl. Conference on Computer Aided Verification (CAV'00), volume 1855 of Lect. Notes in Comp. Sci. Springer-Verlag, 2000.]]

Digital Library

[14]

E. W. Dijkstra. A discipline of programming. Prentice Hall, 1976.]]

Digital Library

[15]

E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.]]

Digital Library

[16]

M. Glusman and S. Katz. A mechanized proof environment for the convenient computations proof method. Formal Methods in System Design, 23(2):115--142, 2003.]]

Digital Library

[17]

P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Workshop on Computer-Aided Verification (CAV'91), volume 575 of LNCS, pages 332--342, 1991.]]

Digital Library

[18]

S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6(2):107--120, September 1992.]]

Digital Library

[19]

D. Kroening and O. Strichman. Efficient computation of recurrence diameters. In Proc. 4th Intl. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'03), volume 2575 of Lecture Notes in Computer Science, pages 298--309, NYU, New-York, January 2003. Springer Verlag.]]

Digital Library

[20]

R. Kurshan. Computer aided verification of coordinating processes. Princeton University Press, 1994.]]

Digital Library

[21]

R. Kurshan, V. Levin, M. Minea, and D. P. H. Yenigün. Combining software and hardware verification techniques. Formal Methos in System Design, 21(3):251--280, 2002.]]

Digital Library

[22]

J. Lind-Nielsen and H. Andersan. Stepwise CTL model checking of state/event systems. In N. Halbwachs and D. Peled, editors, Proc. 11th Intl. Conference on Computer Aided Verification (CAV'99), volume 1633 of Lect. Notes in Comp. Sci., pages 316--327. Springer-Verlag, 1999.]]

Digital Library

[23]

K. L. McMillan. Interpolation and sat-based model checking. In J. Warren A. Hunt and F. Somenzi, editors, cav03, Lect. Notes in Comp. Sci., Jul 2003.]]

[24]

D. Peled. Combining partial order reductions with on-the-fly model-checking. Journal of Formal Methods in Systems Design, 8 (1):39--64, 1996. also appeared in 6th International Conference on Computer Aided Verification 1994, Stanford CA, USA, LNCS 818, Springer-Verlag, 377--390.]]

Digital Library

[25]

K. Ravi and F. Somenzi. High-density reachability analysis. In Proc. Intl. Conf. on Computer-Aided Design, pages 154--158, November 1995.]]

Digital Library

[26]

K. Ravi and F. Somenzi. Hints to accelerate symbolic traversal. In CHARME'99, LNCS 1703, pages 250--264. Springer-Verlag, 1999.]]

Digital Library

[27]

M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties using induction and a sat-solver. In Hunt and Johnson, editors, Proc. Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD 2000), 2000.]]

Digital Library

[28]

A. Valmari. A stubborn attack on state explosion. In Workshop on Computer-Aided Verification (CAV'90), volume 531 of LNCS, New Brunswick, 1990.]]

Digital Library

Cited By

Verma SRoy S(2022)Debug-localize-repair: a symbiotic construction for heap manipulationsFormal Methods in System Design10.1007/s10703-021-00387-z58:3(399-439)Online publication date: 8-Feb-2022
https://doi.org/10.1007/s10703-021-00387-z
Chatterjee PMeda JLal ARoy S(2022)Proof-Guided Underapproximation Widening for Bounded Model CheckingComputer Aided Verification10.1007/978-3-031-13185-1_15(304-324)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_15
Golia PSlivovsky FRoy SMeel K(2021)Engineering an Efficient Boolean Functional Synthesis Engine2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)10.1109/ICCAD51958.2021.9643583(1-9)Online publication date: 1-Nov-2021
https://doi.org/10.1109/ICCAD51958.2021.9643583
Show More Cited By

Index Terms

Proof-guided underapproximation-widening for multi-process systems
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Proof-guided underapproximation-widening for multi-process systems
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

This paper presents a procedure for the verification of multi-process systems based on considering a series of underapproximated models. The procedure checks models with an increasing set of allowed interleavings of the given set of processes, starting ...
Proof-Guided Underapproximation Widening for Bounded Model Checking
Computer Aided Verification
Abstract
Bounded Model Checking (BMC) is a popularly used strategy for program verification and it has been explored extensively over the past decade. Despite such a long history, BMC still faces scalability challenges as programs continue to grow larger ... $^{}$ $^{}$ $^{}$
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2005

402 pages

ISBN:158113830X

DOI:10.1145/1040305

General Chair:
Jens Palsberg
University of California, Los Angeles, CA
,
Program Chair:
Martín Abadi
University of California, Santa Cruz, CA

ACM SIGPLAN Notices Volume 40, Issue 1
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2005
391 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1047659
Issue’s Table of Contents

Copyright © 2005 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 January 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

POPL05

Sponsor:

POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005

January 12 - 14, 2005

California, Long Beach, USA

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

52
Total Citations
View Citations
611
Total Downloads

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

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Verma SRoy S(2022)Debug-localize-repair: a symbiotic construction for heap manipulationsFormal Methods in System Design10.1007/s10703-021-00387-z58:3(399-439)Online publication date: 8-Feb-2022
https://doi.org/10.1007/s10703-021-00387-z
Chatterjee PMeda JLal ARoy S(2022)Proof-Guided Underapproximation Widening for Bounded Model CheckingComputer Aided Verification10.1007/978-3-031-13185-1_15(304-324)Online publication date: 7-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-13185-1_15
Golia PSlivovsky FRoy SMeel K(2021)Engineering an Efficient Boolean Functional Synthesis Engine2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD)10.1109/ICCAD51958.2021.9643583(1-9)Online publication date: 1-Nov-2021
https://doi.org/10.1109/ICCAD51958.2021.9643583
Verma AKalita PPandey ARoy SMars JTang LXue JWu P(2020)Interactive debugging of concurrent programs under relaxed memory modelsProceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3368826.3377910(68-80)Online publication date: 22-Feb-2020
https://dl.acm.org/doi/10.1145/3368826.3377910
Golia PRoy SMeel K(2020)Manthan: A Data-Driven Approach for Boolean Function SynthesisComputer Aided Verification10.1007/978-3-030-53291-8_31(611-633)Online publication date: 14-Jul-2020
https://doi.org/10.1007/978-3-030-53291-8_31
Laarman A(2018)Stubborn Transaction ReductionNASA Formal Methods10.1007/978-3-319-77935-5_20(280-298)Online publication date: 11-Mar-2018
https://doi.org/10.1007/978-3-319-77935-5_20
Verma SRoy SBodden ESchäfer WDeursen AZisman A(2017)Synergistic debug-repair of heap manipulationsProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering10.1145/3106237.3106263(163-173)Online publication date: 21-Aug-2017
https://dl.acm.org/doi/10.1145/3106237.3106263
Prabhu SSchrammel PSrivas MTautschnig MYeolekar A(2017)Concurrent Program Verification with Invariant-Guided UnderapproximationAutomated Technology for Verification and Analysis10.1007/978-3-319-68167-2_17(241-248)Online publication date: 27-Sep-2017
https://doi.org/10.1007/978-3-319-68167-2_17
Guthmann OStrichman OTrostanetski APiskac RTalupur M(2016)Minimal unsatisfiable core extraction for SMTProceedings of the 16th Conference on Formal Methods in Computer-Aided Design10.5555/3077629.3077644(57-64)Online publication date: 3-Oct-2016
https://dl.acm.org/doi/10.5555/3077629.3077644
Cordeiro Lde Lima Filho E(2016)SMT-Based Context-Bounded Model Checking for Embedded SystemsACM SIGSOFT Software Engineering Notes10.1145/2934240.293424741:3(1-6)Online publication date: 24-Jun-2016
https://dl.acm.org/doi/10.1145/2934240.2934247
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