乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T15:52:10Z","timestamp":1732031530365},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2004,8,1]],"date-time":"2004-08-01T00:00:00Z","timestamp":1091318400000},"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":[[2004,8]]},"DOI":"10.1007\/s10009-003-0130-9","type":"journal-article","created":{"date-parts":[[2004,10,28]],"date-time":"2004-10-28T19:07:10Z","timestamp":1098990430000},"page":"260-276","source":"Crossref","is-referenced-by-count":67,"title":["Heuristics for model checking Java programs"],"prefix":"10.1007","volume":"6","author":[{"given":"Alex","family":"Groce","sequence":"first","affiliation":[]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,10,29]]},"reference":[{"key":"130_CR1","unstructured":"Ammann P, Black P (2000) Test generation and recognition with formal methods. In: Proceedings of the 1st international workshop on automated program analysis, testing, and verication, Limerick, Ireland, June 2000, pp 64\u201367"},{"key":"130_CR2","doi-asserted-by":"crossref","unstructured":"Ammann P, Black P, Majurski W (1998) Using model checking to generate tests from specifications. In: Proceedings of the 2nd IEEE international conference on formal engineering methods, Brisbane, Australia, December 1998, pp 46\u201354","DOI":"10.1109\/ICFEM.1998.730569"},{"key":"130_CR3","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2001) Automatically Validating Temporal Safety Properties of Interfaces. In: Proceedings of the 8th international SPIN workshop on model checking of software, Toronto, May 2001, pp 103\u2013122","DOI":"10.1007\/3-540-45139-0_7"},{"key":"130_CR4","unstructured":"Beizer B (1990) Software testing techniques, 2nd edn. Van Nostrand Reinhold, New York"},{"key":"130_CR5","doi-asserted-by":"crossref","unstructured":"Bloem R, Ravi K, Somenzi F (2000) Symbolic guided search for CTL model checking. In: Proceedings of the conference on design automation (DAC), Los Angeles, June 2000, pp 29\u201334","DOI":"10.1145\/337292.337306"},{"key":"130_CR6","doi-asserted-by":"crossref","unstructured":"Chaki S, Clarke E, Groce A, Jha S, Veith H (2003) Modular Verification of Software Components in C. In: Proceedings of the 25th international conference on software engineering, Portland, OR, May 2003, pp 385\u2013395","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"130_CR7","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th conference on computer aided verification, Chicago, July 2000, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"130_CR8","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"Clarke","year":"1994","unstructured":"Clarke EM, Grumberg O, Long DE (1994) Model checking and abstraction. ACM Trans Programm Lang Sys 16(5):1512\u20131542","journal-title":"ACM Trans Programm Lang Sys"},{"key":"130_CR9","unstructured":"Clarke EM, Grumberg O, Peled D (2000) Model checking. MIT Press, Cambridge, MA"},{"key":"130_CR10","doi-asserted-by":"crossref","unstructured":"Cobleigh JM, Clarke LA, Osterweil LJ (2001) The right algorithm at the right time: comparing data flow analysis algorithms for finite state verification. In: Proceedings of the 23rd international conference on software engineering, Toronto, May 2001, pp 37\u201346","DOI":"10.1109\/ICSE.2001.919079"},{"key":"130_CR11","doi-asserted-by":"crossref","unstructured":"Corbett JC, Dwyer M, Hatcliff J, P\u0103s\u0103reanu C, Robby, Laubach S, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of the 22nd international conference on software engineering, Limerick, Ireland, June 2000, pp 439\u2013448","DOI":"10.1145\/337180.337234"},{"key":"130_CR12","doi-asserted-by":"crossref","unstructured":"Dwyer M, Hatcliff J, Joehanes R, Laubach S, P\u0103s\u0103reanu CS, Robby, Visser W, Zheng H (2001) Tool-supported Program Abstraction for Finite-state Verification. In: Proceedings of the 23rd international conference on software engineering, Toronto, May 2001, pp 177\u2013187","DOI":"10.1109\/ICSE.2001.919092"},{"key":"130_CR13","unstructured":"Edelkamp S, Mehler T (2003) Byte code distance heuristics and trail direction for model checking Java programs. In: Proceedings of the workshop on model checking and artificial intelligence (MoChArt), Acapulco, Mexico, August 2003"},{"key":"130_CR14","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Reffel F (1998) OBDDs in heuristic search. In: Proceedings of the 22nd annual German conference on advances in artificial intelligence (KI-98), Berlin, Germany, September 1998, pp 81\u201392","DOI":"10.1007\/BFb0095430"},{"key":"130_CR15","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Lafuente AL, Leue S (2001a) Directed explicit model checking with HSF-Spin. In: Proceedings of the 8th international SPIN workshop on model checking of software, Toronto, May 2001, pp 57\u201379","DOI":"10.1007\/3-540-45139-0_5"},{"key":"130_CR16","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Lafuente AL, Leue S (2001b) Trail-directed model checking. In: Proceedings of the workshop on software model checking, Electronic notes in theoretical computer science. Elsevier, Amsterdam, 5(3)","DOI":"10.1016\/S1571-0661(04)00261-0"},{"key":"130_CR17","unstructured":"Edelkamp S, Lafuente AL, Leue S (2002a) Directed explicit-state model checking in the validation of communication protocols. Int J Softw Tools Technol Transfer http:\/\/www.springerlink.com\/app\/home\/issue.asp?wasp=6ea5d385hl2uyg5c6q9x&referrer=parent&backto=journal,1,15;linkingpublicationresults,id:101563,1"},{"key":"130_CR18","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Lafuente AL, Leue S (2002b) Partial order reduction in directed model checking. In: Proceedings of the 9th international SPIN workshop on model checking of software, Grenoble, France, April 2002, pp 112\u2013127","DOI":"10.1007\/3-540-46017-9_10"},{"key":"130_CR19","doi-asserted-by":"crossref","unstructured":"Engels A, Feijs L, Mauw S (1997) Test generation for intelligent networks using model checking. In: Proceedings of the conference on tools and algorithms for construction and analysis of systems, Enschede, The Netherlands, April 1997, pp 384\u2013398","DOI":"10.1007\/BFb0035401"},{"key":"130_CR20","doi-asserted-by":"crossref","unstructured":"Fernandez JC, Jard C, Jeron T, Viho G (1996) Using on-the-fly verification techniques for the generation of test suites. In: Proceedings of the 8th conference on computer aided verification, New Brunswick, NJ, July 1996, pp 348\u2013359","DOI":"10.1007\/3-540-61474-5_82"},{"key":"130_CR21","doi-asserted-by":"crossref","unstructured":"Friedman G, Hartman A, Nagin K, Shiran T (2002) Projected state machine coverage for software testing. In: Proceedings of the international symposium on software testing and analysis (ISSTA 2002), Rome, July 2002, pp 134\u2013143","DOI":"10.1145\/566172.566192"},{"key":"130_CR22","unstructured":"Ganai AK, Aziz A (1998) Efficient coverage directed state space search. In: Proceedings of the international workshop on logic synthesis, Lake Tahoe, CA, May 1998, pp 267\u2013275"},{"key":"130_CR23","doi-asserted-by":"crossref","unstructured":"Garagantini A, Heitmeyer C (1999) Using model checking to generate tests from requirements specifications. In: Proceedings of the joint 7th European software engineering conference and 7th ACM SIGSOFT international symposium on foundations of software engineering, Toulouse, France, September 1999, pp 146\u2013162","DOI":"10.1007\/3-540-48166-4_10"},{"key":"130_CR24","doi-asserted-by":"crossref","unstructured":"Godefroid P (1997) VeriSoft: a tool for the automatic analysis of concurrent reactive software. In: Proceedings of the 9th conference on computer aided verification, Haifa, Israel, June 1997, pp 172\u2013186","DOI":"10.1007\/3-540-63166-6_52"},{"key":"130_CR25","doi-asserted-by":"crossref","unstructured":"Godefroid P, Khurshid S (2002) Exploring very large state spaces using genetic algorithms. In: Proceedings of the conference on tools and algorithms for construction and analysis of systems, Grenoble, France, April 2002, pp 266\u2013280","DOI":"10.1007\/3-540-46002-0_19"},{"key":"130_CR26","doi-asserted-by":"crossref","unstructured":"Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Proceedings of the 9th conference on computer aided verification, Haifa, Israel, June 1997, pp 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"130_CR27","doi-asserted-by":"crossref","unstructured":"Groce A, Visser W (2002a) Heuristic model checking for Java programs. In: Proceedings of the 9th international SPIN workshop on model checking of software, Grenoble, France, April 2002, pp 242\u2013245","DOI":"10.1007\/3-540-46017-9_21"},{"key":"130_CR28","doi-asserted-by":"crossref","unstructured":"Groce A, Visser W (2002b) Model checking Java programs using structural heuristics. In: Proceedings of the international symposium on software testing and analysis (ISSTA 2002), Rome, July 2002, pp 12\u201321","DOI":"10.1145\/566172.566175"},{"key":"130_CR29","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"Hart","year":"1968","unstructured":"Hart PE, Nilsson NJ, Raphael B (1968) A formal basis for heuristic determination of minimum path cost. IEEE Trans Sys Sci Cybern 4(2):100\u2013107","journal-title":"IEEE Trans Sys Sci Cybern"},{"key":"130_CR30","unstructured":"Havelund K, Lowry M, Park S, Pecheur C, Penix J, Visser W, White J (2000) Formal analysis of the remote agent before and after flight. In: Proceedings of the 5th NASA Langley formal methods workshop, Hampton, VA, June 2000"},{"key":"130_CR31","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of the ACM SIGPLAN-SIGACT conference on principles of programming languages, Portland, OR, January 2002, pp 58\u201370","DOI":"10.1145\/565816.503279"},{"key":"130_CR32","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1990) Algorithms for automated protocol verification. AT&T Tech J 69(2):32\u201344. Special Issue on Protocol Testing, Specification, and Verification","DOI":"10.1002\/j.1538-7305.1990.tb00101.x"},{"key":"130_CR33","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Peled D (1996) The state of SPIN. In: Proceedings of the 8th conference on computer aided verification, New Brunswick, NJ, July 1996, pp 385\u2013389","DOI":"10.1007\/3-540-61474-5_85"},{"key":"130_CR34","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Smith MH (2000) Automating software feature verification. In: Bell Labs Tech J 5(2):72\u201387","DOI":"10.1002\/bltj.2223"},{"key":"130_CR35","unstructured":"Iosif R, Sisto R (1999) dSPIN: a dynamic extension of SPIN. In: Proceedings of the 6th international SPIN workshop on model checking of software, Toulouse, France, September 1999, pp 261\u2013276"},{"key":"130_CR36","unstructured":"Jensen RM, Bryant RE, Veloso MM (2002a) An efficient BDD-based A* algorithm. In: Proceedings of the AIPS-02 workshop on planning via model checking, Toulouse, France, April 2002, pp 72\u201380"},{"key":"130_CR37","unstructured":"Jensen RM, Bryant RE, Veloso MM (2002b) SetA*: an efficient BDD-based heuristic search algorithm. In: Proceedings of the 18th national conference on artificial intelligence (AAAI-02), Edmonton, Alberta, Canada, July 2002, pp 668\u2013673"},{"key":"130_CR38","doi-asserted-by":"crossref","unstructured":"Khurshid S, P\u0103s\u0103reanu CS, Visser W (2003) Generalized symbolic execution for model checking and testing. In: Proceedings of the conference on tools and algorithms for construction and analysis of systems, Warsaw, Poland, April 2003, pp 553\u2013568","DOI":"10.1007\/3-540-36577-X_40"},{"key":"130_CR39","doi-asserted-by":"crossref","first-page":"870","DOI":"10.1109\/32.57624","volume":"16","author":"Korel","year":"1990","unstructured":"Korel B (1990) Automated software test data generation. IEEE Trans Softw Eng 16(8):870\u2013879","journal-title":"IEEE Trans Softw Eng"},{"key":"130_CR40","first-page":"the","volume":"analysis","author":"Lin","year":"1987","unstructured":"Lin FJ, Chu PM, Liu MT (1987) Protocol verification using reachability analysis: the state space explosion problem and relief strategies. ACM SIGCOMM Comput Commun Rev 17(5)","journal-title":"Protocol verification using reachability"},{"key":"130_CR41","doi-asserted-by":"crossref","unstructured":"Musuvathi M, Park D, Chou A, Engler D, Dill D (2002) CMC: a pragmatic approach to model checking real code. In: Proceedings of the 5th symposium on operating system design and implementation, Boston, December 2002","DOI":"10.1145\/1060289.1060297"},{"key":"130_CR42","unstructured":"Pageot JM, Jard C (1988) Experience in guiding simulation. In: Proceedings of the 8th workshop of protocol specification, testing, and verification, Atlantic City, NJ"},{"key":"130_CR43","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/s10009-002-0088-z","volume":"5","author":"P","year":"2003","unstructured":"P\u0103s\u0103reanu CS, Dwyer MB, Visser W (2003) Finding feasible counter-examples when model checking abstracted Java programs. Int J Softw Tools Technol Transfer 5(1):34\u201348","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"130_CR44","doi-asserted-by":"crossref","unstructured":"Penix J, Visser W, Engstrom E, Larson A, Weininger N (2000) Verification of time partitioning in the DEOS scheduler kernel. In: Proceedings of the 22nd international conference on software engineering, Limerick, Ireland, June 2000, pp 488\u2013497","DOI":"10.1145\/337180.337364"},{"key":"130_CR45","unstructured":"Pretschner A (2001) Classical search strategies for test case generation with Constraint Logic Programming. In: Proceedings of the workshop on formal approaches to testing of software, Aalborg, Denmark, August 2001, pp 47\u201360"},{"key":"130_CR46","doi-asserted-by":"crossref","unstructured":"Rayadurgam S, Heimdahl MP (2001) Coverage based test-case generation using model checkers. In: Proceedings of the 8th annual IEEE international conference and workshop on the engineering of computer based systems, Washington, DC, April 2001, pp 83\u201393","DOI":"10.1109\/ECBS.2001.922409"},{"key":"130_CR47","unstructured":"RTCA Special Committee 167 (1992) Software considerations in airborne systems and equipment certification. Technical Report DO-178B, RTCA Inc, Washington, DC, December 1992"},{"key":"130_CR48","doi-asserted-by":"crossref","unstructured":"Saidi H (1999) Modular and incremental analysis of concurrent software systems. In: Proceedings of the 14th IEEE international conference on automated software engineering (ASE), Cocoa Beach, FL, October 1999, pp 92\u2013101","DOI":"10.1109\/ASE.1999.802128"},{"key":"130_CR49","doi-asserted-by":"crossref","unstructured":"Savage S, Burrows M, Nelson G, Sobalvarro P (1997) Eraser: a dynamic data race detector for multithreaded programs. In: ACM Trans Comput Sys 15(4):391\u2013411","DOI":"10.1145\/265924.265927"},{"key":"130_CR50","unstructured":"Sun R, Sessions C (2001) Learning plans without a priori knowledge. Adapt Behav 8(3\/4):225\u2013254"},{"key":"130_CR51","doi-asserted-by":"crossref","unstructured":"Tracey N, Clark J, Mander K, McDermid J (1998) An automated framework for structural test-data generation. In: Proceedings of the 13th IEEE international conference on automated software engineering (ASE), Honolulu, October 1998, pp 285\u2013288","DOI":"10.1109\/ASE.1998.732680"},{"key":"130_CR52","doi-asserted-by":"crossref","unstructured":"Visser W, Havelund K, Brat G, Park S (2000a) Model checking programs. In: Proceedings of the 15th IEEE international conference on automated software engineering (ASE), Grenoble, France, September 2000, pp 3\u201311","DOI":"10.1109\/ASE.2000.873645"},{"key":"130_CR53","doi-asserted-by":"crossref","unstructured":"Visser W, Park S, Penix J (2000b) Using predicate abstraction to reduce object-oriented programs for model checking. In: Proceedings of the 3rd ACM SIGSOFT workshop on formal methods in software practice, Portland, OR, August 2000, pp 3\u201312","DOI":"10.1145\/349360.351125"},{"key":"130_CR54","doi-asserted-by":"crossref","unstructured":"Yang HC, Dill DL (1998) Validation with guided search of the state space. In: Proceedings of the conference on design automation (DAC), San Francisco, June 1998, pp 599\u2013604","DOI":"10.1145\/277044.277201"}],"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-003-0130-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0130-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0130-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T14:23:53Z","timestamp":1585923833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0130-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,8]]},"references-count":54,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["130"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0130-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,8]]}}}