{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:04Z","timestamp":1751662864693},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602996"},{"type":"electronic","value":"9783540447887"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60299-2_37","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:15:07Z","timestamp":1330262107000},"page":"589-623","source":"Crossref","is-referenced-by-count":18,"title":["Automatic generation of invariants and intermediate assertions"],"prefix":"10.1007","author":[{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anca","family":"Browne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zohar","family":"Manna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symp. Princ. of Prog. Lang., pages 238\u2013252. ACM Press, 1977.","key":"37_CR1","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In 19th ACM Symp. Princ. of Prog. Lang., pages 343\u2013354, 1992.","key":"37_CR2","DOI":"10.1145\/143165.143235"},{"doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among the variables of a program. In 5th ACM Symp. Princ. of Prog. Lang., pages 84\u201397, Jan. 1978.","key":"37_CR3","DOI":"10.1145\/512760.512770"},{"unstructured":"D.R. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving \u2200CTL*, \u2203ECTL*, CTL*. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET 94), pages 573\u2013592, June 1994.","key":"37_CR4"},{"doi-asserted-by":"crossref","unstructured":"P. Granger. Static analysis of linear congruence equalities among variables of a program. In TAPSOFT 91, Vol. 1: Colloq. on Trees in Algebra and Programming (CAAP '91), LNCS, pages 169\u2013192. Springer-Verlag, April 1991.","key":"37_CR5","DOI":"10.1007\/3-540-53982-4_10"},{"issue":"1","key":"37_CR6","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/TSE.1975.6312821","volume":"1","author":"S. M. German","year":"1975","unstructured":"S. M. German and B. Wegbreit. A Synthesizer of Inductive Assertions. IEEE transactions on Software Engineering, 1(1):68\u201375, March 1975.","journal-title":"IEEE transactions on Software Engineering"},{"unstructured":"D. Harel. Statecharts: A visual approach to complex systems. Technical Report CS84-05, Dept. of Applied Mathematics, Weizmann Institute of Science, 1984.","key":"37_CR7"},{"unstructured":"N. Heintze. Set Based Program Analysis. PhD thesis, Carnegie Mellon University, 1992.","key":"37_CR8"},{"doi-asserted-by":"crossref","unstructured":"T.A. Henzinger and P.-H. Ho. Algorithmic analysis of nonlinear hybrid systems. In Proc. 7th Intl. Conference on Computer Aided Verification, LNCS, 1995.","key":"37_CR9","DOI":"10.1007\/3-540-60045-0_53"},{"unstructured":"N. Heintze and J. Jaffar. A decision procedure for a class of Herbrand set constraints. Technical Report CMU-CS-91-110, Carnegie Mellon University, Feb. 1991. Abstract appears in Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, 1990.","key":"37_CR10"},{"doi-asserted-by":"crossref","unstructured":"N. Halbwachs, P. Raymond, and Y.-E. Proy. Verification of linear hybrid systems by means of convex approximations. In 1st Intl. Static Analysis Symp., vol. 864 of LNCS, pages 223\u2013237. Springer-Verlag, Sept. 1994.","key":"37_CR11","DOI":"10.1007\/3-540-58485-4_43"},{"key":"37_CR12","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133\u2013151, 1976.","journal-title":"Acta Informatica"},{"issue":"4","key":"37_CR13","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S. Katz","year":"1976","unstructured":"S. Katz and Z. Manna. Logical analysis of programs. Communications of the ACM, 19(4):188\u2013206, April 1976.","journal-title":"Communications of the ACM"},{"unstructured":"K. Lautenbach. Exacte Bedingungen der Lebendigkeit f\u00fcr eine Klasse von Petri-Netzen. St. Augustin, GMD Bonn, 82, 1973.","key":"37_CR14"},{"doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, L. de Alfaro, H. Devarajan, H.B. Sipma, and T.E. Uribe. STeP: The Stan-ford temporal prover. Technical Report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.","key":"37_CR15","DOI":"10.21236\/ADA324036"},{"key":"37_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"37_CR17","volume-title":"vol. 4 of EATCS Monographs on Theoretical Computer Science","author":"W. Reisig","year":"1985","unstructured":"W. Reisig. Petri Nets: An Introduction, vol. 4 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1985."}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2014 CP '95"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60299-2_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:57:59Z","timestamp":1605628679000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60299-2_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602996","9783540447887"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-60299-2_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}