{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:56Z","timestamp":1725489356040},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540740605"},{"type":"electronic","value":"9783540740612"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-74061-2_4","type":"book-chapter","created":{"date-parts":[[2007,8,21]],"date-time":"2007-08-21T11:39:13Z","timestamp":1187696353000},"page":"52-68","source":"Crossref","is-referenced-by-count":8,"title":["Lattice Automata: A Representation for Languages on Infinite Alphabets, and Some Applications to Verification"],"prefix":"10.1007","author":[{"given":"Tristan","family":"Le Gall","sequence":"first","affiliation":[]},{"given":"Bertrand","family":"Jeannet","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11784180_17","volume-title":"Algebraic Methodology and Software Technology","author":"T. Gall Le","year":"2006","unstructured":"Le Gall, T., Jeannet, B., J\u00e9ron, T.: Verification of communication protocols using abstract interpretation of FIFO queues. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol.\u00a04019, Springer, Heidelberg (2006)"},{"key":"4_CR2","unstructured":"Le Gall, T., Jeannet, B.: Analysis of communicating infinite state machines using lattice automata. Technical Report PI 1839, IRISA (2007)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. of ACM 30(2) (1983)","DOI":"10.1145\/322374.322380"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032741","volume-title":"Static Analysis","author":"B. Boigelot","year":"1997","unstructured":"Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs (extended abstract). In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302, Springer, Heidelberg (1997)"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theoretical Computer Science\u00a0221(1-2) (1999)","DOI":"10.1016\/S0304-3975(99)00033-X"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Finkel, A., Iyer, S.P., Sutre, G.: Well-abstracted transition systems: application to FIFO automata. Information and Computation 181(1) (2003)","DOI":"10.1016\/S0890-5401(02)00027-5"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Peng, W., Puroshothaman, S.: Data flow analysis of communicating finite state machines. ACM Trans. Program. Lang. Syst. 13(3) (1991)","DOI":"10.1145\/117009.117015"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Algebraic Methodology and Software Technology","author":"B. Jeannet","year":"2004","unstructured":"Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, Springer, Heidelberg (2004)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"L. Mauborgne","year":"2000","unstructured":"Mauborgne, L.: Tree schemata and fair termination. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, Springer, Heidelberg (2000)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-69738-1_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"O. Kupferman","year":"2007","unstructured":"Kupferman, O., Lustig, Y.: Lattice automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 199\u2013213. Springer, Heidelberg (2007)"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","first-page":"332","volume-title":"Algebraic Methodology and Software Technology","author":"F. Logozzo","year":"2004","unstructured":"Logozzo, F.: Separate compositional analysis of class-based object-oriented languages. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 332\u2013346. Springer, Heidelberg (2004)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44683-4_49","volume-title":"Mathematical Foundations of Computer Science 2001","author":"F. Neven","year":"2001","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol.\u00a02136, Springer, Heidelberg (2001)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theoretical Computer Science 134(2) (1994)","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Milo, T., Suciu, D., Vianu, V.: Typechecking for XML transformers. In: Symp. on Principles of Database Systems (2000)","DOI":"10.1145\/335168.335171"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS 2006. Symp. on Logic in Computer Science (2006)","DOI":"10.1109\/LICS.2006.51"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL 1999. Symp. on Principles of Programming Languages (1999)","DOI":"10.1145\/292540.292552"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45789-5_8","volume-title":"Static Analysis","author":"T. Yavuz-Kahveci","year":"2002","unstructured":"Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, Springer, Heidelberg (2002)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, Springer, Heidelberg (2006)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Technology for Verification and Analysis","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract tree regular model checking of complex dynamic data structures. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, Springer, Heidelberg (2006)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Gopan","year":"2004","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, Springer, Heidelberg (2004)"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis","author":"J. Feret","year":"2001","unstructured":"Feret, J.: Abstract interpretation-based static analysis of mobile ambients. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, Springer, Heidelberg (2001)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica 6 (1976)","DOI":"10.1007\/BF00268497"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978. Symp. on Principles of programming languages (1978)","DOI":"10.1145\/512760.512770"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Jeannet, B.: Dynamic partitioning in linear relation analysis. application to the verification of reactive systems. Formal Methods in System Design 23(1) (2003)","DOI":"10.1023\/A:1024480913162"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages and Systems","author":"L. Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, Springer, Heidelberg (2005)"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"M. Higuchi","year":"1993","unstructured":"Higuchi, M., Shirakawa, O., Seki, H., Fujii, M., Kasami, T.: A verification procedure via invariant for extended communicating finite-state machines. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, Springer, Heidelberg (1993)"},{"key":"4_CR27","unstructured":"Lee, D., Ramakrishnan, K.K., Moh, W.M., Shankar, U.: Protocol specification using parameterized communicating extended finite state machines. In: ICNP 1996. Int. Conf. on Network Protocols (1996)"},{"key":"4_CR28","unstructured":"Jeannet, B., Min\u00e9, A.: The APRON Numerical Abstract Domain Library. http:\/\/apron.cri.ensmp.fr\/library\/"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Besson, F., Jensen, T., M\u00e9tayer, D.L., Thorn, T.: Model checking security properties of control flow graphs. J. of Computer Security 9 (2001)","DOI":"10.3233\/JCS-2001-9303"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Constant, C., Jeannet, B., J\u00e9ron, T.: Automatic test generation from interprocedural specifications. Technical Report PI 1835, IRISA Submitted to TESTCOM\/FATES conference (2007)","DOI":"10.1007\/978-3-540-73066-8_4"},{"key":"4_CR32","unstructured":"Sharir, M., Pnueli, A.: Semantic foundations of program analysis. In: Program Flow Analysis: Theory and Applications (1981)"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: POPL 1982. Symp. on Principles of Programming Languages (1982)","DOI":"10.1145\/582153.582161"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Caucal, D.: On the regular structure of prefix rewriting. Theoretical Computer Science 106 (1992)","DOI":"10.1016\/0304-3975(92)90278-N"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) ETAPS 1999 and FOSSACS 1999. LNCS, vol.\u00a01578, Springer, Heidelberg (1999)"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, Springer, Heidelberg (1997)"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electronic Notes on Theoretical Computer Science 9 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"4_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45306-7_10","volume-title":"Compiler Construction","author":"N. Rinetzky","year":"2001","unstructured":"Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001 and ETAPS 2001. LNCS, vol.\u00a02027, Springer, Heidelberg (2001)"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L., Jard, C., J\u00e9ron, T., Kerbrat, A., Morel, P., Mounier, L.: Verification and test generation for the SSCOP protocol. Scientific Computer Programming 36(1) (2000)","DOI":"10.1016\/S0167-6423(99)00017-9"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Rusu, V.: Combining formal verification and conformance testing for validating reactive systems. J. of Software Testing, Verification, and Reliability 13(3) (2003)","DOI":"10.1002\/stvr.274"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74061-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T05:59:52Z","timestamp":1556776792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74061-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540740605","9783540740612"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74061-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}