Article

Symbolic compositional verification by learning assumptions

Authors:

Wonhong NamAuthors Info & Claims

CAV'05: Proceedings of the 17th international conference on Computer Aided Verification

Pages 548 - 562

https://doi.org/10.1007/11513988_52

Published: 06 July 2005 Publication History

Abstract

The verification problem for a system consisting of components can be decomposed into simpler subproblems for the components using assume-guarantee reasoning. However, such compositional reasoning requires user guidance to identify appropriate assumptions for components. In this paper, we propose an automated solution for discovering assumptions based on the L^* algorithm for active learning of regular languages. We present a symbolic implementation of the learning algorithm, and incorporate it in the model checker NuSMV. Our experiments demonstrate significant savings in the computational requirements of symbolic model checking.

References

[1]

M. Abadi and L. Lamport. Conjoining specifications. ACM TOPLAS, 17:507-534, 1995.

Digital Library

[2]

R. Alur, P. Cerny, P. Madhusudan, and W. Nam. Synthesis of interface specifications for Java classes. In Proc. 32nd ACM POPL, pages 98-109, 2005.

Digital Library

[3]

R. Alur, L. de Alfaro, T.A. Henzinger, and F. Mang. Automating modular verification. In CONCUR'99: Concurrency Theory, LNCS 1664, pages 82-97, 1999.

Digital Library

[4]

R. Alur and T.A. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7-48, 1999. A preliminary version appears in Proc. 11th LICS, 1996.

Digital Library

[5]

R. Alur, T.A. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In 10th CAV, pages 516-520, 1998.

Digital Library

[6]

D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75:87-106, 1987.

Digital Library

[7]

H. Barringer, C.S. Pasareanu, and D. Giannakopolou. Proof rules for automated compositional verification through learning. In Proc. 2nd SVCBS, 2003.

[8]

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. 5th TACAS, pages 193-207, 1999.

Digital Library

[9]

R.E. Bryant. Graph-based algorithms for boolean-function manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986.

Digital Library

[10]

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In Proc. CAV 2002, LNCS 2404, pages 359-364, 2002.

Digital Library

[11]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154-169, 2000.

[12]

J.M. Cobleigh, D. Giannakopoulou, and C.S. Pasareanu. Learning assumptions for compositional verification. In Proc. 9th TACAS, LNCS 2619, pages 331-346, 2003.

Digital Library

[13]

O. Grümberg and D.E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843-871, 1994.

Digital Library

[14]

T.A. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: Methodology and case studies. In Proc. CAV 98, LNCS 1427, pages 521-525, 1998.

Digital Library

[15]

R.P. Kurshan. Computer-aided Verification of Coordinating Processes: the automata-theoretic approach. Princeton University Press, 1994.

Digital Library

[16]

K.L. McMillan. Symbolic model checking. Kluwer Academic Publishers, 1993.

Digital Library

[17]

K.L. McMillan. A compositional rule for hardware design refinement. In CAV 97: Computer-Aided Verification, LNCS 1254, pages 24-35, 1997.

Digital Library

[18]

K.L. McMillan. Applying SAT methods in unbounded symbolic model checking. In Proc. 14th Computer Aided Verification, LNCS 2404, pages 250-264, 2002.

Digital Library

[19]

K.S. Namjoshi and R.J. Trefler. On the completeness of compositional reasoning. In CAV 2000: Computer-Aided Verification, LNCS 1855, pages 139-153, 2000.

Digital Library

[20]

D. Peled, M.Y. Vardi and M. Yannakakis. Black box checking. Journal of Automata, Languages and Combinatorics, 7(2): 225-246, 2002.

Digital Library

[21]

R.L. Rivest and R.E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299-347, 1993.

Digital Library

[22]

E.W. Stark. A proof technique for rely-guarantee properties. In FST & TCS 85, LNCS 206, pages 369-391, 1985.

Digital Library

[23]

A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Actively learning to verify safety properties for FIFO automata. In Proc. 24th FSTTCS, pages 494-505, 2004.

Digital Library

Cited By

Teng YZhang MAn J(2024)Learning Deterministic Multi-Clock Timed AutomataProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650124(1-11)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650124
Chen HSu YZhang MLiu ZMi J(2023)Learning Assumptions for Compositional Verification of Timed AutomataComputer Aided Verification10.1007/978-3-031-37706-8_3(40-61)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_3
An JZhan BZhan NZhang M(2021)Learning Nondeterministic Real-Time AutomataACM Transactions on Embedded Computing Systems10.1145/347703020:5s(1-26)Online publication date: 22-Sep-2021
https://dl.acm.org/doi/10.1145/3477030
Show More Cited By

Symbolic compositional verification by learning assumptions
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation

Recommendations

Automatic symbolic compositional verification by learning assumptions

Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on assume-guarantee reasoning principles, and requires user guidance to identify ...
Learning assumptions for compositional verification
TACAS'03: Proceedings of the 9th international conference on Tools and algorithms for the construction and analysis of systems

Compositional verification is a promising approach to addressing the state explosion problem associated with model checking. One compositional technique advocates proving properties of a system by checking properties of its components in an assume-...
Learning Assumptions for Compositional Verification of Timed Automata
Computer Aided Verification
Abstract
Compositional verification, such as the technique of assume-guarantee reasoning (AGR), is to verify a property of a system from the properties of its components. It is essential to address the state explosion problem associated with model ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV'05: Proceedings of the 17th international conference on Computer Aided Verification

July 2005

564 pages

ISBN:3540272313

Editors:
Kousha Etessami
LFCS, School of Informatics, University of Edinburgh
,
Sriram K. Rajamani
LFCS, School of Informatics, Microsoft Research India

Sponsors

Jasper Design Automation: Jasper Design Automation
Weizmann Institute: Weizmann Institute
Microsoft: Microsoft
Intel: Intel
IBM: IBM

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 06 July 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

45
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Teng YZhang MAn J(2024)Learning Deterministic Multi-Clock Timed AutomataProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650124(1-11)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650124
Chen HSu YZhang MLiu ZMi J(2023)Learning Assumptions for Compositional Verification of Timed AutomataComputer Aided Verification10.1007/978-3-031-37706-8_3(40-61)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_3
An JZhan BZhan NZhang M(2021)Learning Nondeterministic Real-Time AutomataACM Transactions on Embedded Computing Systems10.1145/347703020:5s(1-26)Online publication date: 22-Sep-2021
https://dl.acm.org/doi/10.1145/3477030
Li YChen YZhang LLiu D(2021)A novel learning algorithm for Büchi automata based on family of DFAs and classification treesInformation and Computation10.1016/j.ic.2020.104678281:COnline publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1016/j.ic.2020.104678
Zhang Zde Amorim AJia LPăsăreanu C(2021)Learning Assumptions for Verifying Cryptographic Protocols CompositionallyFormal Aspects of Component Software10.1007/978-3-030-90636-8_1(3-23)Online publication date: 28-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-90636-8_1
Mayr FVisca RYovine S(2020)On-the-fly Black-Box Probably Approximately Correct Checking of Recurrent Neural NetworksMachine Learning and Knowledge Extraction10.1007/978-3-030-57321-8_19(343-363)Online publication date: 25-Aug-2020
https://dl.acm.org/doi/10.1007/978-3-030-57321-8_19
Abbasi RGhassemi FKhosravi R(2019)Verification of asynchronous systems with an unspecified componentActa Informatica10.1007/s00236-018-0317-x56:2(161-203)Online publication date: 1-Mar-2019
https://dl.acm.org/doi/10.1007/s00236-018-0317-x
Íncer Romeo ÍSangiovanni-Vincentelli ALin CKang EHu KZhan N(2018)Quotient for assume-guarantee contractsProceedings of the 16th ACM-IEEE International Conference on Formal Methods and Models for System Design10.5555/3343872.3343881(67-77)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.5555/3343872.3343881
Abd Elkader KGrumberg OPăsăreanu CShoham S(2018)Automated circular assume-guarantee reasoningFormal Aspects of Computing10.1007/s00165-017-0436-030:5(571-595)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s00165-017-0436-0
Garg PNeider DMadhusudan PRoth D(2016)Learning invariants using decision trees and implication counterexamplesACM SIGPLAN Notices10.1145/2914770.283766451:1(499-512)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837664
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents