{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T04:02:19Z","timestamp":1748923339693,"version":"3.41.0"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,12,1]],"date-time":"2002-12-01T00:00:00Z","timestamp":1038700800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information Systems Frontiers"],"published-print":{"date-parts":[[2002,12]]},"DOI":"10.1023\/a:1020883625495","type":"journal-article","created":{"date-parts":[[2003,3,18]],"date-time":"2003-03-18T20:57:25Z","timestamp":1048021045000},"page":"363-377","source":"Crossref","is-referenced-by-count":4,"title":["Lightweight Reasoning about Program Correctness"],"prefix":"10.1007","volume":"4","author":[{"given":"Marsha","family":"Chechik","sequence":"first","affiliation":[]},{"given":"Wei","family":"Ding","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5100447_CR1","doi-asserted-by":"crossref","unstructured":"Bharadwaj R, Heitmeyer C. Model checking complete requirements specifications using abstraction. Journal of Automated Software Engineering 1999;6(1).","DOI":"10.1023\/A:1008697817793"},{"key":"5100447_CR2","first-page":"274","volume":"1633","author":"G Bruns","year":"1999","unstructured":"Bruns G, Godefroid P. Model checking partial state spaces with 3-valued temporal logics. In: Proceedings of CAV\u201999, vol. 1633 of LNCS, 1999:274-287.","journal-title":"Proceedings of CAV\u201999"},{"key":"5100447_CR3","first-page":"168","volume":"877","author":"G Bruns","year":"2000","unstructured":"Bruns G, Godefroid P. Generalized model checking: Reasoning about partial state spaces. In: Proceedings of CONCUR\u201900, vol. 877 of LNCS, 2000:168-182.","journal-title":"Proceedings of CONCUR\u201900"},{"key":"5100447_CR4","doi-asserted-by":"crossref","unstructured":"Bultan T, Gerber R, League C. Verifying systems with integer constraints and boolean predicates: A composite approach. In: Proceedings of International Symposium on Software Testing and Analysis (ISSTA\u201998), 1998:113-123.","DOI":"10.1145\/271771.271799"},{"issue":"1","key":"5100447_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/332740.332746","volume":"9","author":"T Bultan","year":"2000","unstructured":"Bultan T, Gerber R, League C. Composite model checking: Verification with type-specific symbolic representations. ACM Transactions on Software Engineering and Methodology 2000;9(1):3-50.","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"5100447_CR6","doi-asserted-by":"crossref","unstructured":"Bultan T, Gerber R, Pugh W. Model checking concurrent systems with unbounded integer variables: Symbolic representations, approximations and experimental results. ACM Transactions on Programming Languages and Systems, 1999.","DOI":"10.1145\/325478.325480"},{"key":"5100447_CR7","doi-asserted-by":"crossref","unstructured":"Chan W, Anderson RJ, Beame P, Jones DH, Notkin D, Warner WE. Decoupling synchronization from local control for efficient symbolic model checking of statecharts. In: Proceedings of the 1999 International Conference on Software Engineering (ICSE\u201999), 1999:142-151.","DOI":"10.1145\/302405.302460"},{"key":"5100447_CR8","first-page":"72","volume":"2021","author":"M Chechik","year":"2001","unstructured":"Chechik M, Easterbrook S, Petrovykh V. Model-checking over multi-valued logics. In: Proceedings of Formal Methods Europe (FME\u201901), vol. 2021 of LNCS, Springer, 2001:72-98.","journal-title":"Proceedings of Formal Methods Europe (FME\u201901)"},{"issue":"2","key":"5100447_CR9","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke E, Emerson E, Sistla A. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 1986;8(2):244-263.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5100447_CR10","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/BF01383968","volume":"6","author":"E Clarke","year":"1995","unstructured":"Clarke E, Grumberg O, Hiraishi H, Jha S, Long D, McMillan K, Ness L. Verification of the futurebus+ cache coherence protocol. In: Formal Methods in System Design 1995;6:217-232.","journal-title":"Formal Methods in System Design"},{"key":"5100447_CR11","unstructured":"Clarke EM, Grumberg O, Long DE. Model checking and abstraction. IEEE Transactions on Programming Languages and Systems 1994;19(2)."},{"key":"5100447_CR12","unstructured":"Colon M, Uribe T. Generating finite-state abstractions of reactive systems using decision procedures. In: Proceedings of the 10th Conference on Computer-Aided Verification, vol. 1427 of LNCS. Springer-Verlag, 1980."},{"key":"5100447_CR13","doi-asserted-by":"crossref","unstructured":"Corbett J, Dwyer M, Hatcliff J, Laubach S, Pasareanu C, Robby, Zheng H. Bandera: Extracting finite-state models from Java Source code. In: Proceedings of 22nd International Conference on Software Engineering, 2000.","DOI":"10.1145\/337180.337234"},{"key":"5100447_CR14","doi-asserted-by":"crossref","unstructured":"Courtois P-J, Parnas DL. Documentation for safety critical software. In: Proceedings of the 15th International Conference on Software Engineering, 1993:315-323.","DOI":"10.1109\/ICSE.1993.346033"},{"key":"5100447_CR15","unstructured":"Cousot P, Cousot R. Static determination of dynamic properties of programs. In: Proceedings of the \"Colloque sur la Programmation\", 1976."},{"key":"5100447_CR16","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th POPL, Los Angeles, California, 1977:238-252.","DOI":"10.1145\/512950.512973"},{"key":"5100447_CR17","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1023\/A:1008649901864","volume":"6","author":"P Cousot","year":"1999","unstructured":"Cousot P, Cousot R. Refining model checking by abstract interpretation. Authomated Software Engineering, special issue on Automated Software Analysis 1999;6:69-95.","journal-title":"Authomated Software Engineering, special issue on Automated Software Analysis"},{"issue":"19","key":"5100447_CR18","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","volume":"2","author":"D Dams","year":"1997","unstructured":"Dams D, Gerth R, Grumberg O. Abstract interpretation of reactive systems. ACMTransactions on Programming Languages and Systems 1997;2(19):253-291.","journal-title":"ACMTransactions on Programming Languages and Systems"},{"key":"5100447_CR19","unstructured":"Dams D, Grumberg O, Gerth R. Abstract interpretation of reactive system: Abstraction-preserving \u2200CTL*, \u2200CTL* andCTL*, North-Holland, 1994:573-592."},{"key":"5100447_CR20","doi-asserted-by":"crossref","unstructured":"Demartini C, Iosif R, Sisto R. dSPIN: A dynamic extension of SPIN. In: Proceedings of the 6th SPIN Workshop on Practical Aspects of Model-Checking, 1999.","DOI":"10.1007\/3-540-48234-2_20"},{"key":"5100447_CR21","first-page":"390","volume-title":"Computer-Aided Verification Computer","author":"D. Dill","year":"1996","unstructured":"Dill D. The Mur\u03c6 verification system. In: Alur R, Henzinger T, eds. Computer-Aided Verification Computer, vol. 1102 of Lecture Notes in Computer Science, New York, N.Y. Springer-Verlag,1996:390-393."},{"key":"5100447_CR22","unstructured":"Ding W. Analyzing infinite-state programs with abstract interpretation. Master\u2019s Thesis, University of Toronto, Department of Computer Science, 2000."},{"key":"5100447_CR23","volume-title":"Proceedings of Foundations of Software","author":"M Dwyer","year":"1997","unstructured":"Dwyer M, Carr V, Hines L. Model checking graphical user interfaces using abstractions. In: Proceedings of Foundations of Software Engineering, Zurich, Switzerland, 1997."},{"key":"5100447_CR24","doi-asserted-by":"crossref","unstructured":"Godefroid P.VeriSoft:Atool for the automatic analysis of concurrent reactive software. In: Proceedings of CAV\u201997, 1997:476-479.","DOI":"10.1007\/3-540-63166-6_52"},{"key":"5100447_CR25","doi-asserted-by":"crossref","unstructured":"Havelund K, Pressburger T. Model checking Java programs using Java pathfinder. International Journal on Software Tools for Technology Transfer, 1999.","DOI":"10.1007\/s100090050043"},{"issue":"5","key":"5100447_CR26","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann G. The model checker SPIN. IEEE Transactions on Software Engineering 1997;23(5):279-295.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"5100447_CR27","doi-asserted-by":"crossref","unstructured":"Holzmann G.Apractical method for verifying event-driven software. In: Proceedings of the 21st International Conference on Software Engineering (ICSE\u201999), 1999:597-607.","DOI":"10.1145\/302405.302710"},{"key":"5100447_CR28","first-page":"155","volume":"2028","author":"M Huth","year":"2001","unstructured":"Huth M, Jagadeesan R, Schmidt DA. Modal transition systems: A foundation for three-valued program analysis. In: Proceedings of 10th European Symposium on Programming (ESOP), vol. 2028 of LNCS, Springer, 2001:155-169.","journal-title":"Proceedings of 10th European Symposium on Programming (ESOP)"},{"key":"5100447_CR29","doi-asserted-by":"crossref","unstructured":"Jackson D. Abstract model checking of infinite specifications. In: Proceedings of FME\u201994: Industrial Benefit of Formal Methods, Second International Symposium of Formal Methods Europe, 1994:519-531.","DOI":"10.1007\/3-540-58555-9_113"},{"key":"5100447_CR30","unstructured":"Jackson D, Wing J. Lightweight formal methods. IEEE Computer, 1996."},{"key":"5100447_CR31","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/3-540-48234-2_7","volume":"1680","author":"W Janssen","year":"1999","unstructured":"Janssen W, Mateescu R, Mauw S, Fennema P, van der Stappen P. Model checking for managers. In: Theoretical and Practical Aspects of SPIN Model Checking, vol. 1680 of LNCS, Springer-Verlag, 1999:92-107.","journal-title":"Theoretical and Practical Aspects of SPIN Model Checking"},{"key":"5100447_CR32","unstructured":"Kamel M, Leue S. Validation of remote object invocation and objectmigration in CORBA GIOP using Promela\/Spin. In: Proceedings of the 4th International SPIN Workshop (SPIN\u20194), Paris, France, 1998."},{"key":"5100447_CR33","unstructured":"Kelb P, Dams D, Gerth R. Practical symbolic model checking of the full \u00b5-calculus using compositional abstractions. Technical Report 95-31, Department of Computer Science, Eindhoven University of Technology, 1995."},{"key":"5100447_CR34","unstructured":"Kelly W, Maslov V, Pugh W, Rosser E, Shpeisman T, Wonnacott D. The Omega calculator and library, version 1.1.0. Technical Report, University of Maryland, 1996."},{"key":"5100447_CR35","volume-title":"Introduction to metamathematics","author":"SC. Kleene","year":"1952","unstructured":"Kleene SC. Introduction to metamathematics. New York: Van Nostrand, 1952."},{"key":"5100447_CR36","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen D. Results on the propositional \u00b5-calculus. Theoretical Computer Science 1983;27:334-354.","journal-title":"Theoretical Computer Science"},{"key":"5100447_CR37","doi-asserted-by":"crossref","unstructured":"Larsen K, Thomsen B. A modal process logic. In: Third Annual Symposium on Logic in Computer Sciences, IEEE Computer Society Press, 1988:203-210.","DOI":"10.1109\/LICS.1988.5119"},{"key":"5100447_CR38","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K. McMillan","year":"1993","unstructured":"McMillan K. Symbolic model checking. Dordrecht: Kluwer Academic, 1993."},{"key":"5100447_CR39","unstructured":"Norrish M. An abstract dynamic semantics for C. Technical Report TR421-mn200, University of Cambridge Computer Laboratory, 1997."},{"issue":"3","key":"5100447_CR40","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"D. Oppen","year":"1978","unstructured":"Oppen D. A 22\n2\npn upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences 1978;16(3):323-332.","journal-title":"Journal of Computer and System Sciences"},{"key":"5100447_CR41","first-page":"12","volume":"1254","author":"A Pardo","year":"1997","unstructured":"Pardo A, Hachtel GD. Automatic abstraction techniques for propositional \u00b5-calculus model checking. In: Proceedings of 9th International Conference on Computer-Aided Verification (CAV\u201997), vol. 1254 of LNCS, Springer-Verlag, 1997:12- 23.","journal-title":"Proceedings of 9th International Conference on Computer-Aided Verification (CAV\u201997)"},{"key":"5100447_CR42","doi-asserted-by":"crossref","unstructured":"Pugh W. The Omega test: A fast and practical integer programming algorithm for dependence analysis. Comm. of the ACM, 1992.","DOI":"10.1145\/125826.125848"},{"key":"5100447_CR43","doi-asserted-by":"crossref","unstructured":"Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3-valued logic. In: Proceedings of 26th Annual ACM Symposium on Principles of Programming Languages, 1999.","DOI":"10.1145\/292540.292552"},{"key":"5100447_CR44","doi-asserted-by":"crossref","unstructured":"Saidi H. Modular and incremental analysis of concurrent software systems. In: Proceedings of the 14th IEEE International Conference on Automated Software Engineering, 1999:92-101.","DOI":"10.1109\/ASE.1999.802128"},{"key":"5100447_CR45","unstructured":"Somenzi F. Binary decision diagrams. In Broy M, Steinbr\u00fcggen R, eds. Calculational System Design, vol. 173 of NATO Science Series F: Computer and Systems Sciences, IOS Press, 1999:303-366."},{"key":"5100447_CR46","unstructured":"Sreemani T, Atlee JM. Feasibility of model checking software requirements: A case study. In: Proceedings of COMPASS\u201996, Gaithersburg, Maryland, 1996."},{"key":"5100447_CR47","doi-asserted-by":"crossref","unstructured":"Visser W, Park S, Penix J. Applying predicate abstraction to model check object-oriented programs.In: Proceedings of 4th International Workshop on Formal Methods in Software Practice, 2000.","DOI":"10.1145\/349360.351125"}],"container-title":["Information Systems Frontiers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020883625495.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1020883625495\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020883625495.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T09:22:36Z","timestamp":1748856156000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1020883625495"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,12]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2002,12]]}},"alternative-id":["5100447"],"URL":"https:\/\/doi.org\/10.1023\/a:1020883625495","relation":{},"ISSN":["1387-3326","1572-9419"],"issn-type":[{"type":"print","value":"1387-3326"},{"type":"electronic","value":"1572-9419"}],"subject":[],"published":{"date-parts":[[2002,12]]}}}