{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T04:26:54Z","timestamp":1778300814357,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614746","type":"print"},{"value":"9783540685999","type":"electronic"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_80","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:41:20Z","timestamp":1330274480000},"page":"323-335","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":54,"title":["Powerful techniques for the automatic generation of invariants"],"prefix":"10.1007","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hassen","family":"Saidi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"issue":"2","key":"28_CR1","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K.R. Apt","year":"1981","unstructured":"K.R. Apt. Ten years of Hoare's logic: a survey, part I. ACM Trans. on Prog. Lang. and Sys., 3(2):431\u2013483, 1981.","journal-title":"ACM Trans. on Prog. Lang. and Sys."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"N. Bj\u00f8ner, A. Browne; and Z. Manna. Automatic generation of invariants and intermediate assertions. In U. Montanari, editor, 1st Int. Conf. on Principles and Practice of Constraint Programming, 1995.","DOI":"10.1007\/3-540-60299-2_37"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"M. Caplain. Finding invariant assertions for proving programs. In Proc. Int. Conf. on Reliable Software, Los Angeles, CA, 1975.","DOI":"10.1145\/800027.808436"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and E. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In POPL'83. ACM, 1983.","DOI":"10.1145\/567067.567080"},{"key":"28_CR5","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. of Prog. Lang., pages 238\u2013252. ACM Press, 1977.","DOI":"10.1145\/512950.512973"},{"issue":"8","key":"28_CR6","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. W. Dijkstra","year":"1975","unstructured":"E. W. Dijkstra. Guarded commands, nondeterminacy, and formal derivation. Comm. ACM, 18(8):453\u2013457, 1975.","journal-title":"Comm. ACM"},{"key":"28_CR7","volume-title":"Research report","author":"B. Elspas","year":"1974","unstructured":"B. Elspas. The semiautomatic generation of inductive assertions for proving program correctness. Research report, SRI, Menlo Park, CA, 1974."},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"R. W. Floyd. Assigning meanings to programs. In In. Proc. Symp. on Appl. Math. 19, pages 19\u201332. American Mathematical Society, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"28_CR9","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 Trans. On Software Engineering, 1:68\u201375, March 1975.","journal-title":"IEEE Trans. On Software Engineering"},{"key":"28_CR10","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. Verifying invariants using theorem proving. In In this volume, 1996.","DOI":"10.1007\/3-540-61474-5_69"},{"key":"28_CR11","unstructured":"S. Katz and Z. Manna. A heuristic approach to program verification. In Proc. 3rd Int. Joint Conf. on Artificial Intelligence, Stanford, CA, 1976."},{"issue":"8","key":"28_CR12","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"L. Lamport. A new solution of Dijkstra's concurrent programming problem. Comm. ACM, 17(8):453\u2013455, 1974.","journal-title":"Comm. ACM"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In POPL, pages 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"28_CR14","volume-title":"Technical report","author":"Z. Manna","year":"1995","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8ner, A. Browne, E. Chang, M. Colon, L. De Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Technical report, Stanford Univ., Stanford, CA, 1995."},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 1995.","DOI":"10.1109\/32.345827"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int. Sym. on Programming, volume 137 of Lecture Notes in Computer Science, pages 337\u2013351. Springer-Verlag, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"B. K. Szymanski. A simple solution to Lamport's concurrent programming problem verification. In Proc. Intern. Conf. on Supercomputing Sys., pages 621\u2013626, 1988.","DOI":"10.1145\/55364.55425"},{"key":"28_CR19","unstructured":"B. K. Szymanski and J. M. Vidal. Automatic verfication of a class of symmetric parallel programs. In Proc. 13th IFIP World Computer Congress, 1994."},{"key":"28_CR20","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS'86. IEEE, 1986."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_80","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:41:04Z","timestamp":1558255264000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_80"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_80","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}