{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:02:33Z","timestamp":1776373353079,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540418658","type":"print"},{"value":"9783540453192","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_9","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T11:50:47Z","timestamp":1184586647000},"page":"113-127","source":"Crossref","is-referenced-by-count":34,"title":["A Technique for Invariant Generation"],"prefix":"10.1007","author":[{"given":"A.","family":"Tiwari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Sa\u00efdi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"9_CR1","unstructured":"S. Bensalem, V. Ganesh, Y. Lakhnech, C. Mu\u00f1oz, S. Owre, H. Rue\u00df, J. Rushby, V. Rusu, H. Sa\u00efdi, N. Shankar, E. Singerman, and A. Tiwari. An overview of SAL. In C. M. Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187\u2013196, 2000. Available at http:\/\/shemesh.larc.nasa.gov\/fm\/Lfm2000\/Proc\/ ."},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1023\/A:1008744030390","volume":"15","author":"S. Bensalem","year":"1999","unstructured":"S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Formal Methods in System Design, 15:75\u201392, 1999.","journal-title":"Formal Methods in System Design"},{"key":"9_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 9th Conference on Computer-Aided Verification, CAV\u201998","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In Proc. of the 9th Conference on Computer-Aided Verification, CAV\u201998, LNCS. Springer Verlag, June 1998."},{"key":"9_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-61474-5_80","volume-title":"Computer-Aided Verification, CAV\u2019 96","author":"S. Bensalem","year":"1996","unstructured":"S. Bensalem, Y. Lakhnech, and H. Sa\u00efdi. Powerful techniques for the automatic generation of invariants. In R. Alur and T. A. Henzinger, editors, Computer-Aided Verification, CAV\u2019 96, number 1102 in LNCS, pages 323\u2013335. Springer-Verlag, 1996."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"N. Bj\u00f8rner, A. Browne, and Z. Manna. Automatic Generation of Invariants and Intermediate Assertions. Theoretical Computer Science, 1997.","DOI":"10.1016\/S0304-3975(96)00191-0"},{"key":"9_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/BFb0039704","volume-title":"Proceedings of the Intl Conf on Formal Methods in Programming and their Applications","author":"F. Bourdoncle","year":"1993","unstructured":"F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In Proceedings of the Intl Conf on Formal Methods in Programming and their Applications, volume 735 of LNCS, pages 128\u2013141. Springer Verlag, 1993."},{"issue":"5","key":"9_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke","year":"1994","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512\u20131542, September 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR8","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 POPL, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Proc. of the 4th Intl. Symposium on Programming Language Implementation and Logic Programming (PLILP\u2019 92 )","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proc. of the 4th Intl. Symposium on Programming Language Implementation and Logic Programming (PLILP\u2019 92 ), volume 631 of LNCS, pages 269\u2013295, Berlin, 1992. Springer-Verlag."},{"issue":"1","key":"9_CR10","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"},{"key":"9_CR11","series-title":"Lect Notes Comput Sci","volume-title":"Conference on Computer Aided Verification CAV\u201996","author":"S. Graf","year":"1996","unstructured":"S. Graf and H. Sa\u00efdi. Verifying invariants using theorem proving. In Conference on Computer Aided Verification CAV\u201996, LNCS 1102, Springer Verlag, 1996."},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/360032.360048","volume":"194","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"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"L. Lamport. The \u2018Hoare logic\u2019 of concurrent programs. In Acta Informatica 14, pages 21\u201337, 1980.","DOI":"10.1007\/BF00289062"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), January 1995.","DOI":"10.1007\/BF01384313"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"H. Sa\u00efdi and N. Shankar. Abstract and model check while you prove. In Computer-Aided Verification, CAV\u2019 99, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48683-6_38"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45319-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:09:40Z","timestamp":1556665780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}