{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:26Z","timestamp":1763467766807},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T00:00:00Z","timestamp":1167350400000},"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":[[2007,6,14]]},"DOI":"10.1007\/s10703-006-0026-x","type":"journal-article","created":{"date-parts":[[2006,12,28]],"date-time":"2006-12-28T15:58:05Z","timestamp":1167321485000},"page":"35-61","source":"Crossref","is-referenced-by-count":6,"title":["Learning to verify branching time properties"],"prefix":"10.1007","volume":"31","author":[{"given":"Abhay","family":"Vardhan","sequence":"first","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,12,29]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"1. Abdulla PA, Jonsson B, Nilsson M, d'Orso J (2003) Algorithmic improvements in regular model checking. In: Computer-Aided verification (CAV\u203203), LNCS, vol 2725, Springer, pp 236\u2013248","DOI":"10.1007\/978-3-540-45069-6_25"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"2. Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: 2nd ACM SIGPLAN-SIGACT symposium on principles of program languages","DOI":"10.1145\/1040305.1040314"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"3. Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proceedings of the 17th international conference on computer aided verification","DOI":"10.1007\/11513988_52"},{"key":"26_CR4","unstructured":"4. ALV (2004) Action language verifier. http:\/\/www.cs.ucsb.edu\/~bultan\/composite\/"},{"issue":"1","key":"26_CR5","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/565816.503275","volume":"37","author":"G Ammons","year":"2002","unstructured":"5. Ammons G, Bod\u00edk R, Larus JR (2002) Mining specifications. ACM SIGPLAN Notices 37(1):4\u201316","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"26_CR6","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"6. Angluin D (1987) Learning regular sets from queries and counterexamples. Inform Comput 75(2):87\u2013106","journal-title":"Inform Comput"},{"key":"26_CR7","volume-title":"Proceedings of the international conference on computer aided verification (CAV\u203201), lecture notes in computer science, vol 1855","author":"A Annichini","year":"2001","unstructured":"7. Annichini A, Bouajjani A, Sighireanu M (2001) TReX: a tool for reachability analysis of complex systems. In: Berry G, Comon H, Finkel A (eds) Proceedings of the international conference on computer aided verification (CAV\u203201), lecture notes in computer science, vol 1855, Springer, Paris, France"},{"key":"26_CR8","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1007\/978-3-540-24730-2_42","volume-title":"Proceedings of the 10th international conference on tools and algorithms for construction and analysis of systems (TACAS\u203204), lecture notes in computer science, vol 2988","author":"S Bardin","year":"2004","unstructured":"8. Bardin S, Finkel A, Leroux J (2004) FASTer acceleration of counter automata in practice. In: Jensen K, Podelski A (eds) Proceedings of the 10th international conference on tools and algorithms for construction and analysis of systems (TACAS\u203204), lecture notes in computer science, vol 2988. Springer, Barcelona, Spain, pp 576\u2013590"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"9. Bartzis C, Bultan T (2004) Widening arithmetic automata. In: Computer aided verification, 2004","DOI":"10.1007\/978-3-540-27813-9_25"},{"key":"26_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-663-09367-1","volume-title":"Transductions and context-free-languages","author":"J Berstel","year":"1979","unstructured":"10. Berstel J (1979) Transductions and context-free-languages. B.G. Teubner, Stuttgart"},{"key":"26_CR11","unstructured":"11. Boigelot B (1999) Symbolic methods for exploring infinite state spaces. PhD thesis, Collection des Publications de la Facult\u00e9 des Sciences Appliqu\u00e9es de l'Universit\u00e9 de Li\u00e9ge"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"12. Boigelot B, Legay A, Wolper P (2003) Iterating transducers in the large (extended abstract). In: CAV: International conference on computer aided verification","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"13. Bouajjani A, Jonsson B, Nilsson M, Touili T (2000) Regular model checking. In: Emerson EA, Sistla AP (eds) Proceedings of the 12th International Conference on Computer-Aided Verification (CAV\u203200), LNCS, vol 1855, Springer, pp 403\u2013418","DOI":"10.1007\/10722167_31"},{"key":"26_CR14","unstructured":"14. Bultan T (1998) Automated symbolic analysis of reactive systems. PhD thesis, Department of Computer Science, University of Maryland, College Park, MD"},{"key":"26_CR15","unstructured":"15. Bultan T, Gerber R, Pugh W (1997) Symbolic model checking of infinite state programs using presburger arithmetic. In: Proceedings of the 9th international conference on computer aided verification (CAV 1997). pp 400\u2013411"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"16. Bultan T, Yavuz-Kahveci T (2001) Action language verifier. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, pp 382\u2013386","DOI":"10.1109\/ASE.2001.989834"},{"key":"26_CR17","unstructured":"17. Clarke E, Chaki S, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: Proceedings of the 17th International Conference on Computer Aided Verification"},{"key":"26_CR18","unstructured":"18. Clarke EM, Grumberg O, Peled DA (2000) Model checking. Number ISBN:0262032708. The MIT Press"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"19. Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp 331\u2013346","DOI":"10.1007\/3-540-36577-X_24"},{"key":"26_CR20","first-page":"223","volume":"1579","author":"G Delzanno","year":"1999","unstructured":"20. Delzanno G, Podelski A (1999) Model checking in CLP, LNCS 1579:223\u2013239","journal-title":"LNCS"},{"key":"26_CR21","unstructured":"21. FAST (2004) Fast acceleration of symbolic transition systems. http:\/\/www.lsv.ens-cachan.fr\/fast\/"},{"issue":"1\u20132","key":"26_CR22","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"22. Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere! Theor Comput Sci 256(1\u20132):63\u201392","journal-title":"Theor Comput Sci"},{"key":"26_CR23","unstructured":"23. Habermehl P, Vojnar T (2004) Regular model checking using inference of regular languages. In: Proceedings of infinity\u203204, London, UK"},{"key":"26_CR24","unstructured":"24. Hopcroft JE, Motwani R, Rotwani, Ullman JD (2000) Introduction to automata theory, languages and computability. Addison-Wesley Longman Publishing Co Inc"},{"key":"26_CR25","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An introduction to computational learning theory","author":"MJ Kearns","year":"1994","unstructured":"25. Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. The MIT Press, Cambridge, Massachusetts"},{"key":"26_CR26","unstructured":"26. Klarlund N, M\u00f8ller A (2004) Mona. http:\/\/www.brics.dk\/mona\/"},{"key":"26_CR27","volume-title":"Introduction to metamathematics","author":"S Kleene","year":"1952","unstructured":"27. Kleene S (1952) Introduction to metamathematics. D. van Nostrand, Princeton"},{"key":"26_CR28","unstructured":"28. LASH (2004) The liege automata-based symbolic handler. http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/ research\/lash\/"},{"key":"26_CR29","unstructured":"29. LEVER (2004) Learning to verify tool. http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/ research\/lash\/ http:\/\/osl.cs.uiuc.edu\/ vardhan\/lever.html"},{"issue":"2","key":"26_CR30","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"RL Rivest","year":"1993","unstructured":"30. Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inform Comput 103(2):299\u2013347","journal-title":"Inform Comput"},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"31. Rybina T, Voronkov A (2002) Brain: backward reachability analysis with integers. In: AMAST, pp 489\u2013494","DOI":"10.1007\/3-540-45719-4_33"},{"issue":"2","key":"26_CR32","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"32. Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2):285\u2013309","journal-title":"Pac J Math"},{"key":"26_CR33","doi-asserted-by":"crossref","unstructured":"33. Touili T (2001) Regular model checking using widening techniques. In: ENTCS, vol 50. Elsevier","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"26_CR34","unstructured":"34. Vardhan A (2006) Learning to verify systems. PhD thesis, Department of Computer Science, University of Illinois at Urbana Champaign"},{"key":"26_CR35","doi-asserted-by":"crossref","unstructured":"35. Vardhan A, Sen K, Viswanathan M, Agha G (2004) Actively learning to verify safety for FIFO automata. In: LNCS 3328, Proceedings of FSTTCS\u203204, Chennai, India, pp 494\u2013505","DOI":"10.1007\/978-3-540-30538-5_41"},{"key":"26_CR36","doi-asserted-by":"crossref","unstructured":"36. Vardhan A, Sen K, Viswanathan M, Agha G (2004) Learning to verify safety properties. In: LNCS 3308, Proceedings of ICFEM\u203204, Seattle, USA, pp 274\u2013288","DOI":"10.1007\/978-3-540-30482-1_26"},{"key":"26_CR37","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/978-3-540-31980-1_4","volume-title":"Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u203205), vol 3440","author":"A Vardhan","year":"2005","unstructured":"37. Vardhan A, Sen K, Viswanathan M, Agha G (2005) Using language inference to verify omega-regular properties. In: Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u203205), vol 3440, Springer, Edinburgh, UK, pp 45\u201360"},{"key":"26_CR38","doi-asserted-by":"crossref","unstructured":"38. Vardhan A, Viswanathan M (2005) Learning to verify branching time properties. In: Proceedings of the twentieth IEEE\/ACM International Conference on Automated Software Engineering. Long Beach, California, USA","DOI":"10.1145\/1101908.1101961"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0026-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0026-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0026-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:01:02Z","timestamp":1559239262000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0026-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12,29]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,6,14]]}},"alternative-id":["26"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0026-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12,29]]}}}