{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T19:58:07Z","timestamp":1672343887308},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,2,1]],"date-time":"2005-02-01T00:00:00Z","timestamp":1107216000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2005,2]]},"DOI":"10.1007\/s10270-003-0042-x","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T13:07:00Z","timestamp":1075381620000},"page":"14-31","source":"Crossref","is-referenced-by-count":8,"title":["Formal verification of software source code through semi-automatic modeling"],"prefix":"10.1007","volume":"4","author":[{"given":"Cindy","family":"Eisner","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,2,1]]},"reference":[{"key":"42_CRfemsys","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1023\/A:1011219209077","volume":"19","author":"Abarbanel-Vinov","year":"2001","unstructured":"Abarbanel-Vinov Y, Aizenbud-Reshef N, Beer I, Eisner C, Geist D, Heyman T, Reuveni I, Rippel E, Shitsevalov I, Wolfsthal Y, Yatzkar-Haham T (2001) On the effective deployment of functional formal verification. Formal Methods in System Design 19(1):35\u201344","journal-title":"Formal Methods in System Design"},{"key":"42_CRback","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"Back","year":"1981","unstructured":"Back R (1981) On correct refinement of programs. Journal of Computer and Systems Sciences 23(1):49\u201368, August","journal-title":"Journal of Computer and Systems Sciences"},{"key":"42_CRbebop","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2000) Bebop: A symbolic model checker for boolean programs. In: Proc. 7th International SPIN Workshop, LNCS, vol 1885. Springer-Verlag","DOI":"10.1007\/10722468_7"},{"key":"42_CRtamir","doi-asserted-by":"crossref","unstructured":"Baumgartner J, Heyman T, Singhal V, Aziz A (1999) Model checking the IBM Gigahertz Processor: An abstraction algorithm for high-performance netlists. In: Proc. 11th International Conference on Computer Aided Verification (CAV), LNCS, vol 1633. Springer-Verlag, pp 72\u201383","DOI":"10.1007\/3-540-48683-6_9"},{"key":"42_CRsugar","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Fisman D, Gringauze A, Rodeh Y (2001) The temporal logic Sugar. In: Berry G, Comon H, Finkel A (eds) Proc. 13th International Conference on Computer Aided Verification (CAV), LNCS, vol 2102. Springer-Verlag, pp 363\u2013367","DOI":"10.1007\/3-540-44585-4_33"},{"key":"42_CRrbcav97","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Geist D, Gluhovsky L, Heyman T, Landver A, Paanah P, Rodeh Y, Ronin G, Wolfsthal Y (1997) RuleBase: Model checking at IBM. In: Proc. 9th International Conference on Computer Aided Verification (CAV), LNCS, vol 1254. Springer-Verlag, pp 480\u2013483","DOI":"10.1007\/3-540-63166-6_53"},{"key":"42_CRdac96","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Landver A (1996) RuleBase: an industry-oriented formal verification tool. In: Proc. 33rd Design Automation Conference (DAC). Association for Computing Machinery, Inc., June, pp 655\u2013660","DOI":"10.1145\/240518.240642"},{"key":"42_CRfantechignesi","doi-asserted-by":"crossref","unstructured":"Bernardeschi C, Fantechi A, Gnesi S, LaRosa S, Mongardi G, Romano D (1998) A formal verification environment for railway signaling system design. Formal Methods in System Design 12(2), March","DOI":"10.1023\/A:1008645826258"},{"key":"42_CRprover","doi-asserted-by":"crossref","unstructured":"Bor\u00e4lv A, St\u00e5lmarck G (1999) Formal verification in railways. In: Hinchey M, Bowen J (eds) Industrial-Strength Formal Methods in Practice. Springer-Verlag, pp 329\u2013350","DOI":"10.1007\/978-1-4471-0523-7_15"},{"key":"42_CRChan-TSE98","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"Chan","year":"1998","unstructured":"Chan W, Anderson RJ, Beame P, Burns S, Modugno F, Notkin D, Reese JD (1998) Model checking large software specifications. IEEE Transactions on Software Engineering 24(7):498\u2013520, July","journal-title":"IEEE Transactions on Software Engineering"},{"key":"42_CRce81b","doi-asserted-by":"crossref","unstructured":"Clarke E, Emerson E (1981) Characterizing correctness properties of parallel programs as fixpoints. In: Seventh International Colloquium on Automata, Languages, and Programming, LNCS, vol 85. Springer-Verlag","DOI":"10.1007\/3-540-10003-2_69"},{"key":"42_CRfuturebus","unstructured":"Clarke E, Grumberg O, Hiraishi H, Jha S, Long D, McMillan K, Ness L (1993) Verfication of the Futurebus+ cache coherence protocol. In: Claesen L (ed) Proc. of the Eleventh International Symposium on Computer Hardware Description Languages and their Applications, April"},{"key":"42_CRornabook","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model Checking. MIT Press"},{"key":"42_CRbandera","doi-asserted-by":"crossref","unstructured":"Corbett JC, Dwyer MB, Hatcliff J, Laubach S, Pasareanu CS, Robby, Zheng H (2000) Bandera: Extracting finite-state models from Java source code. In: Proc. of the 22st International Conference on Software Engineering, June","DOI":"10.1145\/337180.337234"},{"key":"42_CRdemartini","unstructured":"Demartini C, Iosif R, Sisto R (1998) Modeling and validation of Java multithreading applications using SPIN. In: Proc. 4th International SPIN Workshop"},{"key":"42_CRslicingdh","unstructured":"Dwyer M, Hatcliff J (1999) Slicing software for model construction. In: Proc. 1999 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation"},{"key":"42_CRasgeir","doi-asserted-by":"crossref","unstructured":"Eir\u00edksson \u00c1 (1998) The formal design of 1M-gate ASICs. In: Second International Conference on Formal Methods in Computer-Aided Design (FMCAD), LNCS, vol 1522. Springer-Verlag, pp 49\u201363","DOI":"10.1007\/3-540-49519-3_5"},{"key":"42_CRcharme","doi-asserted-by":"crossref","unstructured":"Eisner C (1999) Using symbolic model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. In: Proceedings 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Bad Herrenalb, Germany, September 1999, LNCS, vol 1703. Springer-Verlag, pp 97\u2013109","DOI":"10.1007\/3-540-48153-2_9"},{"key":"42_CRmodelcheckingsmv","doi-asserted-by":"crossref","unstructured":"Eisner C (2001) Model checking the garbage collection mechanism of SMV. In: Stoller SD, Visser W (eds) Electronic Notes in Theoretical Computer Science, vol 55. Elsevier Science Publishers","DOI":"10.1016\/S1571-0661(04)00258-0"},{"key":"42_CRtrainssttt","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s100090100063","volume":"Transfer","author":"Eisner","year":"2002","unstructured":"Eisner C (2002) Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard. International Journal on Software Tools for Technology Transfer (STTT) 4(1):107\u2013124, October","journal-title":"International Journal on Software Tools for Technology"},{"key":"42_CRpecos","doi-asserted-by":"crossref","unstructured":"Eisner C, Hoover R, Nation W, Nelson K, Shitsevalov I, Valk K (2000) A methodology for formal design of hardware control with application to cache coherence protocols. In: Proc. 37th Design Automation Conference (DAC). Association for Computing Machinery, Inc., pp 724\u2013729, June","DOI":"10.1145\/337292.337757"},{"key":"42_CRspin2002","doi-asserted-by":"crossref","unstructured":"Eisner C, Peled D (2002) Comparing symbolic and explicit model checking of a software system. In: Proceedings, 9th International SPIN Workshop on Model Checking of Software, LNCS, vol 2318. Springer-Verlag","DOI":"10.1007\/3-540-46017-9_18"},{"key":"42_CRpushdown","doi-asserted-by":"crossref","unstructured":"Esparza J, Hansel D, Rossmanith P, Schwoon S (2000) Efficient algorithms for model checking pushdown systems. In: Proc. 12th International Conference on Computer Aided Verification (CAV), LNCS, vol 1855. Springer-Verlag, pp 232\u2013247","DOI":"10.1007\/10722167_20"},{"key":"42_CRrulebasemanual","unstructured":"RuleBase User\u2019s Manual, Version 1.4.3 (2003) Formal Methods Group, IBM Haifa Research Laboratory"},{"key":"42_CRinformalsugar","unstructured":"Guide to Sugar Formal Specification Language Version 1.3.1 (November 2000) Formal Methods Group, IBM Haifa Research Laboratory"},{"key":"42_CRverisoftpopl","doi-asserted-by":"crossref","unstructured":"Godefroid P (1997) Model checking for programming languages using VeriSoft. In: Proc. 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Association for Computing Machinery, Inc., January","DOI":"10.1145\/263699.263717"},{"key":"42_CRverisoftcav","doi-asserted-by":"crossref","unstructured":"Godefroid P (1997) VeriSoft: A tool for the automatic analysis of concurrent reactive software. In: Proc. 9th International Conference on Computer Aided Verification (CAV), LNCS, vol 1254. Springer-Verlag","DOI":"10.1007\/3-540-63166-6_52"},{"key":"42_CRamit","doi-asserted-by":"crossref","unstructured":"Goel A, Lee W (2000) Formal verification of an IBM Coreconnect Processor Local Bus arbiter core. In: Proc. 37th Design Automation Conference (DAC). Association for Computing Machinery, Inc., pp 196\u2013200, June","DOI":"10.1145\/337292.337384"},{"key":"42_CRgroote","unstructured":"Groote J, Koorn J, van Vlijmen S (1994) The safety guaranteeing system at station Hoorn-Kersenboogerd. Logic Group Preprint Series 121, Utrecht University"},{"key":"42_CRjavapathfindersttt","doi-asserted-by":"crossref","unstructured":"Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer (STTT) 2(4)","DOI":"10.1007\/s100090050043"},{"key":"42_CRholzmannansic","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (2000) Logic verification of ANSI-C code with SPIN. In: Proc. 7th International SPIN Workshop, LNCS, vol 1885. Springer-Verlag, pp 224 ff","DOI":"10.1007\/10722468_8"},{"key":"42_CRholzmannsw","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Smith MH (1999) Software model checking: Extracting verification models from source code. In: Proc. PSTV\/FORTE99. Kluwer, pp 481\u2013497","DOI":"10.1007\/978-0-387-35578-8_28"},{"key":"42_CRkesten","doi-asserted-by":"crossref","unstructured":"Kesten Y, Klein A, Pnueli A, Raanan G (1999) Bridging the e-business gap through formal verification. In: Hinchey M, Bowen J (eds) Industrial-Strength Formal Methods in Practice. Springer-Verlag, pp 117\u2013137","DOI":"10.1007\/978-1-4471-0523-7_6"},{"key":"42_CRleduc","doi-asserted-by":"crossref","unstructured":"Leduc G, Bonaventure O, L\u00e9onard L, Koerner E, Pecheur C (1999) Model-based verification of a security protocol for conditional access to services. Formal Methods in System Design 14(2), March","DOI":"10.1023\/A:1008683519655"},{"key":"42_CRmannapnueli","first-page":"Safety","volume":"Systems","author":"Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York","journal-title":"Temporal Verification of Reactive"},{"key":"42_CRsmv","doi-asserted-by":"crossref","unstructured":"McMillan K (1993) Symbolic Model Checking. Kluwer Academic Publishers","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"42_CRmertens","unstructured":"Mertens J (1996) Verifying the Safety Guaranteeing System at Railway Station Heerhugowaard. PhD thesis, Utrecht University"},{"key":"42_CRmilner","unstructured":"Milner R (1971) An algebraic definition of simulation between programs. In Proc. 2nd International Joint Conference on Artificial Intelligence, pp 481\u2013489"},{"key":"42_CRmorgan","unstructured":"Morgan C (1990) Programming from Specifications. Prentice-Hall"},{"key":"42_CRmorris","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"Morris","year":"1987","unstructured":"Morris J (1987) A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming 9(3):287\u2013306, December","journal-title":"Science of Computer Programming"},{"key":"42_CRpfa","unstructured":"Muchnick S, Jones N (1981) Program Flow Analysis. Prentice-Hall"},{"key":"42_CRzoran","unstructured":"Parash A (2000) Formal verification of an MPEG decoder chip: A case study in the industrial use of formal methods. In: Proceedings of the Workshop on Advances in Verification (WAVe), (a post CAV-2000 workshop), Chicago, July"},{"key":"42_CRqueillesifakis","doi-asserted-by":"crossref","unstructured":"Queille J, Sifakis J (1982) Specification and verification of concurrent systems in CESAR. In: Proc. International symposium in Programming, LNCS, vol 137. Springer-Verlag, pp 337\u2013351","DOI":"10.1007\/3-540-11494-7_22"},{"key":"42_CRhints","doi-asserted-by":"crossref","unstructured":"Ravi K, Somenzi F (1999) Hints to accelerate symbolic traversal. In: Proceedings 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), Bad Herrenalb, Germany, September, LNCS, vol 1703. Springer-Verlag","DOI":"10.1007\/3-540-48153-2_19"},{"key":"42_CRsheeran","doi-asserted-by":"crossref","unstructured":"Sheeran M, St\u00e5lmarck G (1998) A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. In: Second International Conference on Formal Methods in Computer-Aided Design (FMCAD), LNCS, vol 1522. Springer-Verlag, pp 82\u201399","DOI":"10.1007\/3-540-49519-3_7"},{"key":"42_CRstoller","doi-asserted-by":"crossref","unstructured":"Stoller SD (2000) Model-checking multi-threaded distributed Java programs. In: Proc. 7th International SPIN Workshop, LNCS, vol 1885. Springer-Verlag, pp 224 ff","DOI":"10.1007\/10722468_14"},{"key":"42_CRfranktip","first-page":"121","volume":"3","author":"Tip","year":"1995","unstructured":"Tip F (1995) A survey of program slicing techniques. Journal of Programming Languages 3(3):121\u2013189","journal-title":"Journal of Programming Languages"},{"key":"42_CRvisser","doi-asserted-by":"crossref","unstructured":"Visser W, Havelund K, Brat G, Park S (2000) Model checking programs. In: Proc. of the 15th International Conference on Automated Software Engineering, Grenoble, France, September","DOI":"10.1109\/ASE.2000.873645"},{"key":"42_CRgalileo","doi-asserted-by":"crossref","unstructured":"Yorav K, Katz S, Kiper R (2001) Reproducing synchronization bugs with model checking. In: Margaria T, Melham T (eds) Proceedings 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), LNCS, vol 2144. Springer-Verlag","DOI":"10.1007\/3-540-44798-9_8"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-003-0042-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-003-0042-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-003-0042-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,29]],"date-time":"2020-03-29T12:38:29Z","timestamp":1585485509000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-003-0042-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,2]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,2]]}},"alternative-id":["42"],"URL":"https:\/\/doi.org\/10.1007\/s10270-003-0042-x","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,2]]}}}