{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T21:17:48Z","timestamp":1673385468655},"reference-count":58,"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-004-0151-z","type":"journal-article","created":{"date-parts":[[2004,11,2]],"date-time":"2004-11-02T15:00:58Z","timestamp":1099407658000},"page":"277-301","source":"Crossref","is-referenced-by-count":14,"title":["Partial-order reduction and trail improvement in directed model checking"],"prefix":"10.1007","volume":"6","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Lluch-Lafuente","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,11,3]]},"reference":[{"key":"151_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Brayton R, Henzinger T, Qaderer S, Rajamani S (1997) Partial-order reduction in symbolic state space exploration. In: 9th conference on computer-aided verification (CAV). Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 340\u2013351","DOI":"10.1007\/3-540-63166-6_34"},{"key":"151_CR2","doi-asserted-by":"crossref","unstructured":"Ball T, Naik M, Rajamani S (2003) From sympton to cause: Localizing errors in counterexample traces. In: 30th annual ACM symposium on principles of programming languages (POPL)","DOI":"10.1145\/604131.604140"},{"key":"151_CR3","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2001) Automatically validating temporal safety properties of interfaces. In: 7th international SPIN workshop on software model checking. Lecture notes in computer science, vol 2057. Springer, Berlin Heidelberg New York, pp 103\u2013122","DOI":"10.1007\/3-540-45139-0_7"},{"key":"151_CR4","unstructured":"Behrmann G, Fehnker A, Hune T, Larsen KG, Petterson P, Romijn J (2001) Guiding and cost-imality in UPPAAL. In: AAAI spring symposium on model-based validation of intelligence, pp 66\u201374"},{"key":"151_CR5","doi-asserted-by":"crossref","unstructured":"Behrmann G, Fehnker A, Hune T, Larsen KG, Petterson P, Romijn J, Vaandrager FW (2001) Efficient guiding towards cost-imality in uppaal. In: Conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45319-9_13"},{"key":"151_CR6","first-page":"model","volume":"verification","author":"B","year":"2001","unstructured":"B\u00e9rard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P (2001) Systems and software verification: model-checking techniques and tools. Springer, Berlin Heidelberg New York","journal-title":"Systems and software"},{"key":"151_CR7","doi-asserted-by":"crossref","unstructured":"Bloem R, Ravi K, Somenzi F (2000) Symbolic guided search for CTL model checking. In: ACM\/IEEE Design Automation Conference (DAC), pp 29\u201334","DOI":"10.1145\/337292.337306"},{"key":"151_CR8","doi-asserted-by":"crossref","unstructured":"Bonet B, Geffner H (2001) Planning as heuristic search. Artif Intell 129(1\u20132):5\u201333","DOI":"10.1016\/S0004-3702(01)00108-4"},{"key":"151_CR9","unstructured":"Bosnacki D, Dams D, Holenderski L (2000) Symmetric SPIN. In: 7th SPIN workshop on software model checking. Lecture notes in computer science, vol 1885. Springer, Berlin Heidelberg New York, pp 1\u201319"},{"key":"151_CR10","doi-asserted-by":"crossref","unstructured":"Chou C-T, Peled D (1996) Formal verification of a partial-order reduction technique for model checking. In: 2nd conference on tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1055. Springer, Berlin Heidelberg New York, pp 241\u2013257","DOI":"10.1007\/3-540-61042-1_48"},{"key":"151_CR11","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA"},{"key":"151_CR12","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: 23rd IEEE international conference on software engineering (ICSE), pp 37\u201346","DOI":"10.1109\/ICSE.2001.919079"},{"key":"151_CR13","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1145\/256163.256168","volume":"15","author":"Cohen","year":"1997","unstructured":"Cohen JD (1997) Recursive hashing functions for n-grams. ACM Trans Inf Sys 15(3):291\u2013320","journal-title":"ACM Trans Inf Sys"},{"key":"151_CR14","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: 22nd IEEE international conference on software engineering (ICSE)","DOI":"10.1145\/337180.337234"},{"key":"151_CR15","unstructured":"Cormen TH, Leiserson CE, Rivest RL (1990) Introduction to algorithms. MIT Press, Cambridge, MA"},{"key":"151_CR16","first-page":"111","volume":"19","author":"Dams","year":"1997","unstructured":"Dams D, Gerth R, Grumberg O (1997) Abstract interpretation of reactive systems. ACM Trans Programm Lang Sys 19(2):111\u2013149","journal-title":"ACM Trans Programm Lang Sys"},{"key":"151_CR17","doi-asserted-by":"crossref","unstructured":"Dechter R, Pearl J (1985) Generalized best-first strategies and the optimality of A*. J ACM 32","DOI":"10.1145\/3828.3830"},{"key":"151_CR18","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0196-6774(82)90023-2","volume":"3","author":"Dolev","year":"1982","unstructured":"Dolev D, Klawe M, Rodeh M (1982) An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. J Algorithms 3:245\u2013260","journal-title":"J Algorithms"},{"key":"151_CR19","unstructured":"Edelkamp S (1999) Data structures and learning algorithms in state space search. PhD thesis, University of Freiburg, Infix"},{"key":"151_CR20","doi-asserted-by":"crossref","unstructured":"Edelkamp S (2003) Promela planning. In: 10th SPIN workshop on model checking software. Lecture notes in computer science, vol 2648. Springer, Berlin Heidelberg New York, pp 197\u2013212","DOI":"10.1007\/3-540-44829-2_13"},{"key":"151_CR21","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Leue S, Lluch-Lafuente A (2004) Directed explicit-state model checking in the validation of communication protocols. Int J Softw Tools Technol Transfer 5(2\u20133):247\u2013267. http:\/\/www.di.unipi.it\/%7Elafuente\/papers\/index.html#phd","DOI":"10.1007\/s10009-002-0104-3"},{"key":"151_CR22","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Lluch-Lafuente A, Leue S (2001) Trail-directed model checking. In: Stoller SD, Visser W (eds) Electronic Notes in Theoretical Computer Science, vol 55. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)00261-0"},{"key":"151_CR23","unstructured":"Edelkamp S, Mehler T (2003) Byte code distance heuristics and trail direction for model checking Java programs. In: 2nd workshop on model checking and artificial intelligence, pp 69\u201376"},{"key":"151_CR24","unstructured":"Emerson EA, Jha S, Peled D (1997) Comibing partial order and symmetry reduction. In: 3rd conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1217. Springer, Berlin Heidelberg New York, pp 19\u201334"},{"key":"151_CR25","doi-asserted-by":"crossref","unstructured":"Emerson EA, Sistla AP (1993) Symmetry and model checking. In: 5th international conference on computer-aided verification (CAV). Lecture notes in computer science, vol 697. Springer, Berlin Heidelberg New York, pp 463\u2013378","DOI":"10.1007\/3-540-56922-7_38"},{"key":"151_CR26","doi-asserted-by":"crossref","unstructured":"Godefroid P (1991) Using partial orders to improve automatic verification methods. In: 2nd conference on computer-aided verification (CAV). Lecture notes in computer science, vol 531. Springer, Berlin Heidelberg New York, pp 176\u2013185","DOI":"10.1007\/BFb0023731"},{"key":"151_CR27","doi-asserted-by":"crossref","unstructured":"Godefroid P, Khurshid S (2002) Exploring very large state spaces using genetic algorithms. In: 8th conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 266\u2013280","DOI":"10.1007\/3-540-46002-0_19"},{"key":"151_CR28","doi-asserted-by":"crossref","unstructured":"Graf S, Saidi H (1997) Construction of abstract state graphs of infinite systems with PVS. In: 9th conference on computer-aided verification (CAV). Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-63166-6_10"},{"key":"151_CR29","doi-asserted-by":"crossref","unstructured":"Groce A, Visser W (2002) Heuristic model checking for java programs. In: 9th SPIN workshop on model checking software. Lecture notes in computer science, vol 2318. Springer, Berlin Heidelberg New York, pp 242\u2013245","DOI":"10.1007\/3-540-46017-9_21"},{"key":"151_CR30","doi-asserted-by":"crossref","unstructured":"Groce A, Visser W (2002) Model checking java programs using structural heuristics. In: International symposium on software testing and analysis (ISSTA). ACM Press, New York","DOI":"10.1145\/566172.566175"},{"key":"151_CR31","doi-asserted-by":"crossref","unstructured":"Groce A, Visser W (2003) What went wrong: Explaining counterexamples. In: Workshop on software model checking (SPIN). Lecture notes in computer science, vol 2648. Springer, Berlin Heidelberg New York, pp 121\u2013135","DOI":"10.1007\/3-540-44829-2_8"},{"key":"151_CR32","unstructured":"Object Management Group (1997) The common object request broker architecture and specification. Revised version 2.1"},{"key":"151_CR33","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:100\u2013107","journal-title":"IEEE Trans Sys Sci Cybern"},{"key":"151_CR34","unstructured":"Holzmann GJ (1990) Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs, NJ"},{"key":"151_CR35","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Holzmann","year":"1997","unstructured":"Holzmann GJ (1997) The model checker Spin. IEEE Trans Softw Eng 23(5):279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"151_CR36","unstructured":"Holzmann GJ (2003) The Spin model checker, primer and reference manual. Addison-Wesley, Reading, MA"},{"key":"151_CR37","doi-asserted-by":"crossref","unstructured":"Holzmann GJ, Godefroid P, Pirottin D (1992) Coverage preserving reduction strategies for reachability analysis. In: 12th international conference on protocol specification, testing, and verification (PSTV)","DOI":"10.1016\/B978-0-444-89874-6.50028-3"},{"key":"151_CR38","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1109\/TSE.2002.995426","volume":"28","author":"Holzmann","year":"2002","unstructured":"Holzmann GJ, Smith MH (2002) An automated verification method for distributed systems software based on model extraction. IEEE Trans Softw Eng 28(4):364\u2013377","journal-title":"IEEE Trans Softw Eng"},{"key":"151_CR39","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"Ip","year":"1996","unstructured":"Ip CN, Dill DL (1996) Better verification through symmetry. Formal Methods Sys Des 9:41\u201375","journal-title":"Formal Methods Sys Des"},{"key":"151_CR40","unstructured":"Jin H, Ravi K, Somenzi F (2002) Fate and free will in error traces. In: 8th conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 445\u2013459"},{"key":"151_CR41","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/s100090050045","volume":"2","author":"Kamel","year":"2000","unstructured":"Kamel M, Leue S (2000) Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN. Int J Softw Tools Technol Transfer 2(4):394\u2013409","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"151_CR42","doi-asserted-by":"crossref","unstructured":"Kamel M, Leue S (2000) VIP: A visual editor and compiler for v-Promela. In: 6th conference on tools and algorithms for the construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 471\u2013486","DOI":"10.1007\/3-540-46419-0_32"},{"key":"151_CR43","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"Korf","year":"1985","unstructured":"Korf RE (1985) Depth-first iterative-deepening: An optimal admissible tree search. Artif Intell 27(1):97\u2013109","journal-title":"Artif Intell"},{"key":"151_CR44","doi-asserted-by":"crossref","unstructured":"Kurshan RP, Levin V, Minea M, Peled D, Yenigun H (1998) Static partial order reduction. In: 4th conference on tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 345\u2013357","DOI":"10.1007\/BFb0054182"},{"key":"151_CR45","doi-asserted-by":"crossref","unstructured":"Lerda F, Sinha N, Theobald M (2003) Symbolic model checking of software. In: Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(05)80008-8"},{"key":"151_CR46","unstructured":"Lluch-Lafuente A (2003) Symmetry reduction and heuristic search for error detection in model checking. In: 2nd workshop on model checking and artificial intelligence (MoChArt), pp 77\u201386"},{"key":"151_CR47","doi-asserted-by":"crossref","unstructured":"Lluch-Lafuente A, Leue S, Edelkamp S (2002) Partial order reduction in directed model checking. In: SPIN workshop on model checking software. Lecture notes in computer science, vol 2318. Springer, Berlin Heidelberg New York, pp 112\u2013127","DOI":"10.1007\/3-540-46017-9_10"},{"key":"151_CR48","first-page":"specification","volume":"systems","author":"Manna","year":"1992","unstructured":"Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, Berlin Heidelberg New York","journal-title":"The temporal logic of reactive and concurrent"},{"key":"151_CR49","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1145\/362619.362631","volume":"14","author":"McVitie","year":"1971","unstructured":"McVitie DG, Wilson LB (1971) The stable marriage problem. Commun ACM 14(7):486\u2013492","journal-title":"Commun ACM"},{"key":"151_CR50","doi-asserted-by":"crossref","unstructured":"Nalumasu R, Gopalakrishnan G (1997) A new partial order reduction algorithm for concurrent system verification. In: Hardware description languages and their applications (CHDL). Chapman & Hall, London","DOI":"10.1007\/978-0-387-35064-6_25"},{"key":"151_CR51","unstructured":"Nilsson NJ (1980) Principles of artificial intelligence. Tioga, Palo Alto, CA"},{"key":"151_CR52","unstructured":"Pearl J (1985) Heuristics. Addison-Wesley, Reading, MA"},{"key":"151_CR53","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00121262","volume":"8","author":"Peled","year":"1996","unstructured":"Peled DA (1996) Combining partial order reductions with on-the-fly model-checking. Formal Methods Sys Des 8:39\u201364","journal-title":"Formal Methods Sys Des"},{"key":"151_CR54","doi-asserted-by":"crossref","unstructured":"Peled DA (1998) Ten years of partial order reduction. In: 10th conference on computer-aided verification (CAV). Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 17\u201328","DOI":"10.1007\/BFb0028727"},{"key":"151_CR55","doi-asserted-by":"crossref","unstructured":"Sharygina N, Peled D (2001) A combined testing and verification approach for software reliability. In: Formal methods of increasing software productivity, internatioanl symposioum of Formal Methods Europe, pp 611\u2013628","DOI":"10.1007\/3-540-45251-6_35"},{"key":"151_CR56","doi-asserted-by":"crossref","unstructured":"Valmari A (1991) A stubborn attack on state explosion. Lecture notes in computer science, vol 531. Springer, Berlin Heidelberg New York, pp 156\u2013165","DOI":"10.1007\/BFb0023729"},{"key":"151_CR57","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1142\/S0218213094000285","volume":"3","author":"Wah","year":"1995","unstructured":"Wah BW, Shang Y (1995) Study of ida*-style searches. J Tools Artif Intell 3(4):493\u2013523","journal-title":"J Tools Artif Intell"},{"key":"151_CR58","doi-asserted-by":"crossref","unstructured":"Yang CH, Dill DL (1998) Validation with guided search of the state space. In: Conference on design automation (DAC), 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-004-0151-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0151-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0151-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T18:00:24Z","timestamp":1585936824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0151-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,8]]},"references-count":58,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["151"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0151-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,8]]}}}