{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:18:39Z","timestamp":1725574719985},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676683"},{"type":"electronic","value":"9783540450993"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/978-3-540-45099-3_4","type":"book-chapter","created":{"date-parts":[[2011,1,14]],"date-time":"2011-01-14T09:05:17Z","timestamp":1294995917000},"page":"58-72","source":"Crossref","is-referenced-by-count":8,"title":["A Transformational Approach for Generating Non-linear Invariants"],"prefix":"10.1007","author":[{"given":"S.","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"M.","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"J. -C.","family":"Fernandez","sequence":"additional","affiliation":[]},{"given":"L.","family":"Ghirvu","sequence":"additional","affiliation":[]},{"given":"Y.","family":"Lakhnech","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Computer Aided Verification","author":"P. Abdulla","year":"1998","unstructured":"Abdulla, P., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy fifb channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 305\u2013318. Springer, Heidelberg (1998)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling Global Conditions in Parameterized System Verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 134\u2013145. Springer, Heidelberg (1999)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science\u00a0126 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1137\/0209050","volume":"9","author":"K.R. Apt","year":"1980","unstructured":"Apt, K.R., Meertens, L.G.L.T.: Completeness with finite systems of intermediate assertions for recursive program schemes. SIAM J. Comp.\u00a09, 665\u2013671 (1980)","journal-title":"SIAM J. Comp."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting wsis systems to verify parameterized networks. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 188. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-46419-0_14"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1996","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 1\u201312. Springer, Heidelberg (1996)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Bultan, Gerber, Pugh.: Symbolic model checking of infinite state systems using presburger arithmetic. In: CAV International Conference on Computer Aided Verification(1997)","DOI":"10.1007\/3-540-63166-6_39"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. 2nd Int. Symp. on Programming, pp. 106\u2013130 (1976)","DOI":"10.1145\/390018.808314"},{"key":"4_CR9","first-page":"238","volume-title":"4th ACM symp. of Prog. Lang.","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fix-points. In: 4th ACM symp. of Prog. Lang., pp. 238\u2013252. ACM Press, New York (1977)"},{"issue":"4","key":"4_CR10","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Logic and Comp.\u00a02(4), 511\u2013547 (1992)","journal-title":"Logic and Comp."},{"key":"4_CR11","first-page":"84","volume-title":"5th ACM symp. of Prog. Lang.","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: 5th ACM symp. of Prog. Lang., pp. 84\u201397. ACM Press, New York (1978)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Caspi, P., Halbwachs, N., Pilaud, D., Plaice, J.: LUSTRE, adclarative language for programming synchronous systems. In: 14th Symposium on Principles of Programming Langiages (1987)","DOI":"10.1145\/41625.41641"},{"issue":"3\/4","key":"4_CR13","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1023\/A:1009747629591","volume":"2","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Olsen, H.: A decompositional approach for computing least fized-points of datalog programs with z-counters. Constraints\u00a02(3\/4), 305\u2013335 (1997)","journal-title":"Constraints"},{"key":"4_CR14","unstructured":"Gorelick, G.A.: A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical report, Toronto (1975)"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1109\/LICS.1992.185551","volume-title":"Seventh Annual IEEE Symposium on Logic in Computer Science","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic modelchecking for real-time systems. In: Seventh Annual IEEE Symposium on Logic in Computer Science, pp. 394\u2013406. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"4_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Proceedings of the International Symposium on Static Analysis","author":"N. Halbwachs","year":"1994","unstructured":"Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Proceedings of the International Symposium on Static Analysis. LNCS, vol.\u00a0818, pp. 223\u2013237. Springer, Heidelberg (1994)"},{"key":"4_CR17","unstructured":"Ivanov, S., Griffioen, W.0.D.: Verification of a biphase mark protocol. Report CSI-R9915, Computing Science Institute, University of Nijmegen (August 1999)"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"4_CR19","volume-title":"Parallel Program Design","author":"K.M. Chandy","year":"1989","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design, May 1989. Addison-Wesley, Austin (1989)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","first-page":"424","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic Model Checking with Rich Assertional Languages. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 424\u2013435. Springer, Heidelberg (1997)"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Moore, J.S.: A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol. Formal Aspects of Computing\u00a03(1) (1993)","DOI":"10.1007\/BF01211081"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Vaandrager, F.: Analysis of a biphase mark protocol with uppaal. Presentation at the meeting of the VHS-ESPRIT Project","DOI":"10.1007\/s00165-006-0008-1"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45099-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T11:13:14Z","timestamp":1637147594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45099-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676683","9783540450993"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45099-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}