{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:52:29Z","timestamp":1762458749738},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2009,9,12]],"date-time":"2009-09-12T00:00:00Z","timestamp":1252713600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10703-009-0081-1","type":"journal-article","created":{"date-parts":[[2009,9,11]],"date-time":"2009-09-11T09:58:53Z","timestamp":1252663133000},"page":"325-367","source":"Crossref","is-referenced-by-count":8,"title":["Action Language verifier: an infinite-state model checker for reactive software specifications"],"prefix":"10.1007","volume":"35","author":[{"given":"Tuba","family":"Yavuz-Kahveci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,9,12]]},"reference":[{"key":"81_CR1","doi-asserted-by":"crossref","unstructured":"Bardin S, Finkel A, Leroux J (2004) Faster acceleration of counter automata in practice. In: TACAS, pp 576\u2013590","DOI":"10.1007\/978-3-540-24730-2_42"},{"issue":"4","key":"81_CR2","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1142\/S0129054103001911","volume":"14","author":"C Bartzis","year":"2003","unstructured":"Bartzis C, Bultan T (2003) Efficient symbolic representations for arithmetic constraints in verification. Int J Found Comput Sci 14(4):605\u2013624","journal-title":"Int J Found Comput Sci"},{"key":"81_CR3","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/978-3-540-27813-9_25","volume-title":"Proceedings of the 16th international conference on computer aided verification (CAV 2004)","author":"C Bartzis","year":"2004","unstructured":"Bartzis C, Bultan T (2004) Widening arithmetic automata. In: Alur R, Peled D (eds) Proceedings of the 16th international conference on computer aided verification (CAV 2004). Lecture notes in computer science, vol 3114. Springer, Berlin, pp 321\u2013333"},{"key":"81_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann G, Bengtsson J, David A, Larsen KG, Pettersson P, Yi W (2002) Uppaal implementation secrets. In: Proceedings of the 7th international symposium on formal techniques in real-time and fault-tolerant systems (FTRTFT 2002), pp 3\u201322","DOI":"10.1007\/3-540-45739-9_1"},{"key":"81_CR5","doi-asserted-by":"crossref","unstructured":"Betin-Can A, Bultan T (2004) Verifiable concurrent programming using concurrency controllers. In: Proceedings of the 19th IEEE international conference on automated software engineering (ASE 2004), September 2004, pp 248\u2013257","DOI":"10.1109\/ASE.2004.1342742"},{"issue":"2","key":"81_CR6","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/s10515-007-0008-2","volume":"14","author":"A Betin-Can","year":"2007","unstructured":"Betin-Can A, Bultan T, Lindvall M, Lux B, Topp S (2007) Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers. Autom Softw Eng 14(2):129\u2013178","journal-title":"Autom Softw Eng"},{"key":"81_CR7","doi-asserted-by":"crossref","unstructured":"Bultan T (2000) Action Language: a specification language for model checking reactive systems. In: Proceedings of the 22nd international conference on software engineering (ICSE 2000), June 2000, pp 335\u2013344","DOI":"10.1145\/337180.337219"},{"issue":"1\u20132","key":"81_CR8","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10617-008-9014-2","volume":"12","author":"T Bultan","year":"2008","unstructured":"Bultan T, Heitmeyer C (2008) Applying infinite state model checking and other analysis techniques to tabular requirements specifications of safety-critical systems. Des Autom Embed Syst 12(1\u20132):97\u2013137","journal-title":"Des Autom Embed Syst"},{"key":"81_CR9","doi-asserted-by":"crossref","unstructured":"Bultan T, Yavuz-Kahveci T (2001) Action Language verifier. In: Proceedings of the 16th IEEE international conference on automated software engineering","DOI":"10.1109\/ASE.2001.989834"},{"issue":"4","key":"81_CR10","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1145\/325478.325480","volume":"21","author":"T Bultan","year":"1999","unstructured":"Bultan T, Gerber R, Pugh W (1999) Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results. ACM Trans Program Lang Syst 21(4):747\u2013789","journal-title":"ACM Trans Program Lang Syst"},{"issue":"1","key":"81_CR11","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 (2000) Composite model checking: verification with type-specific symbolic representations. ACM Trans Softw Eng Methodol 9(1):3\u201350","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"81_CR12","series-title":"LNCS","volume-title":"Proc. international conference on computer-aided verification (CAV 2002)","author":"A Cimatti","year":"2002","unstructured":"Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV version 2: an opensource tool for symbolic model checking. In: Proc. international conference on computer-aided verification (CAV 2002), Copenhagen, Denmark, July 2002. LNCS, vol 2404. Springer, Berlin"},{"key":"81_CR13","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke E, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge"},{"key":"81_CR14","doi-asserted-by":"crossref","unstructured":"Clarke EM, Jha S, Lu Y, Veith H (2002) Tree-like counterexamples in model checking. In: Proceedings of the 17th IEEE symposium on logic in computer science (LICS 2002), pp 19\u201329","DOI":"10.1109\/LICS.2002.1029814"},{"key":"81_CR15","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th annual ACM symposium on principles of programming languages, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"81_CR16","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th annual ACM symposium on principles of programming, pp 84\u201397","DOI":"10.1145\/512760.512770"},{"key":"81_CR17","unstructured":"CUDD: CU decision diagram package. http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"81_CR18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/10722167_8","volume-title":"Proceedings of the 12th international conference on computer aided verification","author":"G Delzanno","year":"2000","unstructured":"Delzanno G (2000) Automatic verification of parameterized cache coherence protocols. In: Proceedings of the 12th international conference on computer aided verification. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 53\u201368"},{"key":"81_CR19","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno G (2003) Constraint-based verification of parameterized cache-coherence protocols. Formal Methods Syst Des 23:257\u2013301","journal-title":"Formal Methods Syst Des"},{"key":"81_CR20","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/3-540-45578-7_20","volume-title":"Proceedings of the 7th international conference on principles and practice of constraint programming (CP 2001)","author":"G Delzanno","year":"2001","unstructured":"Delzanno G, Bultan T (2001) Constraint-based verification of client-server protocols. In: Walsh T (ed) Proceedings of the 7th international conference on principles and practice of constraint programming (CP 2001). Lecture notes in computer science, vol 2239. Springer, Berlin, pp 286\u2013301"},{"key":"81_CR21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-45319-9_11","volume-title":"Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2001)","author":"X Fu","year":"2001","unstructured":"Fu X, Bultan T, Hull R, Su J (2001) Verification of Vortex workflows. In: Margaria T, Yi W (eds) Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2001). Lecture notes in computer science, vol 2031. Springer, Berlin, pp 143\u2013157"},{"key":"81_CR22","doi-asserted-by":"crossref","unstructured":"Henriksen JG, Jensen J, Jorgensen M, Klarlund N, Paige R, Rauhe T, Sandholm A (1995) Mona: monadic second-order logic in practice. In: Proc. TACAS (1995)","DOI":"10.1007\/3-540-60630-0_5"},{"key":"81_CR23","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger TA, Ho P, Wong-Toi H (1997) Hytech: a model checker for hybrid systems. Softw Tools Technol Transf 1:110\u2013122","journal-title":"Softw Tools Technol Transf"},{"issue":"5","key":"81_CR24","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ 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":"81_CR25","doi-asserted-by":"crossref","unstructured":"Lowry M (2002) Software construction and software analysis tools for future space missions. In: Proceedings of the eighth international conference on tools and algorithms for the construction and analysis of systems (TACAS 2002)","DOI":"10.1007\/3-540-46002-0_1"},{"key":"81_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer Academic, Norwell"},{"issue":"1","key":"81_CR27","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/s10703-006-0019-9","volume":"30","author":"T Sch\u00fcle","year":"2007","unstructured":"Sch\u00fcle T, Schneider K (2007) Bounded model checking of infinite state systems. Formal Methods Syst Des 30(1):51\u201381","journal-title":"Formal Methods Syst Des"},{"key":"81_CR28","unstructured":"The Omega project. http:\/\/www.cs.umd.edu\/projects\/omega\/"},{"key":"81_CR29","doi-asserted-by":"crossref","unstructured":"Vardhan A, Viswanathan M (2006) Lever: a tool for learning based verification. In: Proceedings of the 18th international conference on computer aided verification (CAV 2006), pp 471\u2013474","DOI":"10.1007\/11817963_43"},{"issue":"1","key":"81_CR30","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10703-006-0026-x","volume":"31","author":"A Vardhan","year":"2007","unstructured":"Vardhan A, Viswanathan M (2007) Learning to verify branching time properties. Formal Methods Syst Des 31(1):35\u201361","journal-title":"Formal Methods Syst Des"},{"key":"81_CR31","unstructured":"Yang Z, Wang C, Gupta A, Ivancic F (2006) Mixed symbolic representations for model checking software programs. In: MEMOCODE, pp 17\u201326"},{"key":"81_CR32","doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci T, Bultan T (2002) Specification, verification, and synthesis of concurrency control components. In: Proc. of international symposium on software testing and analysis","DOI":"10.1145\/566172.566199"},{"issue":"1","key":"81_CR33","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/s10009-002-0091-4","volume":"5","author":"T Yavuz-Kahveci","year":"2003","unstructured":"Yavuz-Kahveci T, Bultan T (2003) A symbolic manipulator for automated verification of reactive systems with heterogeneous data types. Int J Softw Tools Technol Transf (STTT) 5(1):15\u201333","journal-title":"Int J Softw Tools Technol Transf (STTT)"},{"key":"81_CR34","doi-asserted-by":"crossref","unstructured":"Yavuz-Kahveci T, Bultan T (2005) Verification of parameterized hierarchical state machines using action language verifier. In: Proceedings of the 3rd ACM-IEEE international conference on formal methods and models for codesign (MEMOCODE 2005), July 2005","DOI":"10.1109\/MEMCOD.2005.1487897"},{"key":"81_CR35","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/11513988_40","volume-title":"Proceedings of the 17th international conference on computer aided verification (CAV 2005)","author":"T Yavuz-Kahveci","year":"2005","unstructured":"Yavuz-Kahveci T, Bartzis C, Bultan T (2005) Action language verifier, extended. In: Etessami K, Rajamani SK (eds) Proceedings of the 17th international conference on computer aided verification (CAV 2005). Lecture notes in computer science, vol 3576. Springer, Berlin, pp 413\u2013417"},{"key":"81_CR36","unstructured":"Zhong C (1997) Modeling of airport operations using an object-oriented approach. PhD thesis, Virginia Polytechnic Institute and State University"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0081-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-009-0081-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-009-0081-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:05:51Z","timestamp":1559239551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-009-0081-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9,12]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["81"],"URL":"https:\/\/doi.org\/10.1007\/s10703-009-0081-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9,12]]}}}