{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T02:28:47Z","timestamp":1747880927747,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642356674"},{"type":"electronic","value":"9783642356681"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35668-1_27","type":"book-chapter","created":{"date-parts":[[2013,1,4]],"date-time":"2013-01-04T10:07:03Z","timestamp":1357294023000},"page":"393-407","source":"Crossref","is-referenced-by-count":1,"title":["SMT-Based Model Checking for Stabilizing Programs,"],"prefix":"10.1007","author":[{"given":"Jingshu","family":"Chen","sequence":"first","affiliation":[]},{"given":"Sandeep","family":"Kulkarni","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Arora, A., Gouda, M.: Closure and convergence: A foundation of fault-tolerant computing. IEEE Transactions on Software Engineering\u00a019(11) (1993)","DOI":"10.1109\/32.256850"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bdds. In: Proc. of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (1999)","DOI":"10.21236\/ADA360973"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a035(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-17653-1_11","volume-title":"Principles of Distributed Systems","author":"J. Chen","year":"2010","unstructured":"Chen, J., Abujarad, F., Kulkarni, S.: Effect of Fairness in Model Checking of Self-stabilizing Programs. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol.\u00a06490, pp. 135\u2013138. Springer, Heidelberg (2010)"},{"key":"27_CR5","unstructured":"Chen, J., Kulkarni, S.: Smt-based model checking for stabilizing programs. Technical Report MSU-CSE-12-13, Computer Science and Engineering, Michigan State University, East Lansing, Michigan (October 2012)"},{"key":"27_CR6","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Journal of Form. Methods Syst. Des. (2001)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F. Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of Bounded Model Checking at an Industrial Setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 436\u2013453. Springer, Heidelberg (2001)"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Self stabilizing systems in spite of distributed control. Communications of the ACM\u00a017(11) (1974)","DOI":"10.1145\/361179.361202"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Dolev, S.: Self-stabilizing routing and related protocols. Journal of Parallel and Distributed Computing\u00a042(2) (1997)","DOI":"10.1006\/jpdc.1997.1317"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Dolev, S.: Self-Stabilization. MIT Press (2000)","DOI":"10.7551\/mitpress\/6156.001.0001"},{"key":"27_CR12","unstructured":"Dutertre, B., De Moura, L.: The yices smt solver. Technical report, Computer Science Laboratory, SRI International (2006)"},{"key":"27_CR13","unstructured":"Grumberg, O., Clarke, E.M., Peled, D.A.: Model Checking. The MIT Press (2000)"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Ghosh, S.: Binary self-stabilization in distributed systems. Information Processing Letter\u00a040(3) (1991)","DOI":"10.1016\/0020-0190(91)90172-E"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Ghosh, S.: Distributed Systems: An Algorithmic Approach. CRC Press (2006)","DOI":"10.1201\/9781420010848"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Ghosh, S., Gupta, A.: An exercise in fault-containment: Self-stabilizing leader election. Information Processing Letters (1996)","DOI":"10.1016\/0020-0190(96)00121-4"},{"key":"27_CR18","unstructured":"Goldberg, E., Novikov, Y.: Berkmin: A fast and robust sat-solver. In: Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2002 (2002)"},{"issue":"4","key":"27_CR19","doi-asserted-by":"publisher","first-page":"448","DOI":"10.1109\/12.88464","volume":"40","author":"M.G. Gouda","year":"1991","unstructured":"Gouda, M.G., Multari, N.: Stabilizing communication protocols. IEEE Trans. Comput.\u00a040(4), 448\u2013458 (1991)","journal-title":"IEEE Trans. Comput."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Kulkarni, S.S., Bolen, C., Oleszkiewicz, J., Robinson, A.: Alternator in read\/write model. Information Processing Letters (2005)","DOI":"10.1016\/j.ipl.2004.11.009"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Kulkarni, S.S., Rushby, J.M., Natarajan, S.: A case-study in component-based mechanical verification of fault-tolerant programs. In: Workshop on Self-stabilizing System, pp. 33\u201340 (1999)","DOI":"10.1109\/SLFSTB.1999.777484"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"27_CR23","unstructured":"McMillan, K.L.: The smv system for smv version 2.5.4. Technical report, Carnegie Mellon University (2000)"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Prasetya, I.S.W.B.: Mechanically verified self-stabilizing hierarchical algorithms. In: Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pp. 399\u2013415 (1997)","DOI":"10.1007\/BFb0035402"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Shankar, N.: Verifying a self-stabilizing mutual exclusion algorithm. In: IFIP International Conference on Programming Concepts and Methods, PROCOMET 1998 (1998)","DOI":"10.1007\/978-0-387-35358-6_27"},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11513988_9","volume-title":"Computer Aided Verification","author":"I. Rabinovitz","year":"2005","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded Model Checking of Concurrent Programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 82\u201397. Springer, Heidelberg (2005)"},{"key":"27_CR28","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/58564.59295","volume":"7","author":"K. Raymond","year":"1989","unstructured":"Raymond, K.: A tree-based algorithm for distributed mutual exclusion. ACM Transactions on Computer Systems (TOCS)\u00a07, 61\u201377 (1989)","journal-title":"ACM Transactions on Computer Systems (TOCS)"},{"key":"27_CR29","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/71.899941","volume":"12","author":"T. Tsuchiya","year":"2001","unstructured":"Tsuchiya, T., Nagano, S., Paidi, R.B., Kikuno, T.: Symbolic model checking for self-stabilizing algorithms. IEEE Trans. Parallel Distrib. Syst.\u00a012, 81\u201395 (2001)","journal-title":"IEEE Trans. Parallel Distrib. Syst."}],"container-title":["Lecture Notes in Computer Science","Distributed Computing and Networking"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35668-1_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T16:00:13Z","timestamp":1745942413000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35668-1_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642356674","9783642356681"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35668-1_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}