{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T17:10:27Z","timestamp":1739034627029,"version":"3.37.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2009,3,24]],"date-time":"2009-03-24T00:00:00Z","timestamp":1237852800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2009,11]]},"DOI":"10.1007\/s10009-009-0112-7","type":"journal-article","created":{"date-parts":[[2009,3,23]],"date-time":"2009-03-23T06:59:43Z","timestamp":1237791583000},"page":"359-374","source":"Crossref","is-referenced-by-count":9,"title":["Checking the reliability of socket based communication software"],"prefix":"10.1007","volume":"11","author":[{"given":"Pedro","family":"de la C\u00e1mara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mar\u00eda","family":"del Mar Gallardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pedro","family":"Merino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,3,24]]},"reference":[{"key":"112_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: IFM, Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"112_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Mjumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of the SIGPLAN \u201901 Conference on Programming Language Design and Implementation (2001)","DOI":"10.1145\/378795.378846"},{"key":"112_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking C programs. In: TACAS 01: Tools and Algorithms for Construction and Analysis of Systems. LNCS, vol. 2031, pp. 268\u2013283. Springer, Heidelberg (2001)","DOI":"10.1007\/3-540-45319-9_19"},{"key":"112_CR4","unstructured":"Bosnacki, D.: Enhancing state space reduction techniques for model checking. Ph.D. Thesis, Eindhoven University of Technology (2001)"},{"key":"112_CR5","doi-asserted-by":"crossref","unstructured":"Camara, P., Gallardo, M.M., Merino, P., Sanan, D.: Model checking software with well-defined APIs: the socket case. In: FMICS 05: Tenth International Workshop on Formal Methods for Industrial Critical Systems, pp. 17\u201326. ACM Press, London (2005)","DOI":"10.1145\/1081180.1081184"},{"key":"112_CR6","unstructured":"Camara, P., Gallardo, M.M., Merino, P.: Abstract matching for software model checking. In: SPIN 06: 13th International SPIN Workshop on Model Checking of Software. LNCS, vol. 3925. Springer, Heidelberg (2006)"},{"key":"112_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"112_CR8","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1007\/s00165-004-0040-y","volume":"16","author":"M.M. Gallardo","year":"2004","unstructured":"Gallardo M.M., Merino P., Pimentel E.: A generalized semantics of promela for abstract model checking. Formal Asp. Comput. 16, 166\u2013193 (2004)","journal-title":"Formal Asp. Comput."},{"issue":"2\u20133","key":"112_CR9","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/s10009-003-0122-9","volume":"5","author":"M.M. Gallardo","year":"2004","unstructured":"Gallardo M.M., Martinez J., Merino P., Pimentel E.: \u03b1SPIN: a tool for abstract model checking. Int. J. Softw. Tools Technol. Trans. 5(2\u20133), 165\u2013184 (2004)","journal-title":"Int. J. Softw. Tools Technol. Trans."},{"key":"112_CR10","doi-asserted-by":"crossref","unstructured":"Garavel, H.: OPEN\/CAESAR: an open software architecture for verification, simulation, and testing. In: Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201998. LNCS, vol. 1384, pp 68\u201384 (1998)","DOI":"10.1007\/BFb0054165"},{"key":"112_CR11","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (1997)","DOI":"10.1145\/263699.263717"},{"key":"112_CR12","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. SE 23(5) (1997)","DOI":"10.1109\/32.588521"},{"key":"112_CR13","volume-title":"SPIN Model Checker, The: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann G.J.: SPIN Model Checker, The: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"112_CR14","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: SPIN, pp. 76\u201391 (2004)","DOI":"10.1007\/978-3-540-24732-6_6"},{"key":"112_CR15","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Smith, M.: Software model checking. Extracting verification models from source code. In: Invited Paper. Proc. PSTV\/FORTE99 Pulb. Kluwer, Dordrecht (1999)","DOI":"10.1007\/978-0-387-35578-8_28"},{"key":"112_CR16","doi-asserted-by":"crossref","unstructured":"Havelund, K.: Thomas Pressburger. Model checking Java programs using Java PathFinder. In: International Journal on Software tools for Technology Transfer (STTT) (1999)","DOI":"10.1007\/s100090050043"},{"key":"112_CR17","unstructured":"Java Compiler Compiler: The Java Parser Generator. Online documentation for Version 0.7.1. Sun Microsystems. Available at http:\/\/www.sun.com\/suntest\/JavaCC"},{"key":"112_CR18","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., Zheng, H.: Bandera: extracting finitestate models from java source code. In: Proc. of the 22nd Int. Conf. on Software Engineering. ACM Press, London (2000)","DOI":"10.1145\/337180.337234"},{"key":"112_CR19","unstructured":"Mikac, J., Caspi, P.: Flush: a system development tool based on Scade\/Lustre. Int. J. Softw. Tools Technol. Transf. (STTT) (2009)"},{"key":"112_CR20","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: a pragmatic approach to checking real code. In: Procosc. of the Fifth Symposium on Operating Systems Design and Implementation (2002)","DOI":"10.1145\/1060289.1060297"},{"key":"112_CR21","unstructured":"Raffelt, H., Steffen, B., Berg, T.: LearnLib: a library for automata learning and experimentation. Int. J. Softw. Tools Technol. Transf. (STTT) (2009)"},{"key":"112_CR22","unstructured":"Stoller, S.D.: Model-checking multi-threaded distributed java programs. In: Proc. 11th International Conference on Automated Deduction. LNAI, vol. 607, pp. 748\u2013752 (1992)"},{"key":"112_CR23","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. of the 15th Int. Conf. on Automated Software Engineering, pp. 3\u201312. IEEE Comp. Society (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"112_CR24","doi-asserted-by":"crossref","unstructured":"Wijs, A., van de Pol, J., Bortnik, E.: Solving scheduling problems by untimed model checking: the clinical chemical analyser case study. Int. J. Softw. Tools Technol. Transf. (STTT) (2009)","DOI":"10.1007\/s10009-009-0110-9"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0112-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-009-0112-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-009-0112-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T16:38:11Z","timestamp":1739032691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-009-0112-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,24]]},"references-count":24,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2009,11]]}},"alternative-id":["112"],"URL":"https:\/\/doi.org\/10.1007\/s10009-009-0112-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2009,3,24]]}}}