{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:17:23Z","timestamp":1755217043517,"version":"3.43.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1999,7]]},"DOI":"10.1023\/a:1008744030390","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"75-92","source":"Crossref","is-referenced-by-count":29,"title":["Automatic Generation of Invariants"],"prefix":"10.1007","volume":"15","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"Yassine","family":"Lakhnech","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"207109_CR1","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. Apt","year":"1981","unstructured":"K. Apt, \u201cTen years of Hoare's logic: A survey, Part I,\u201d ACM Trans. on Prog. Lang. and Sys., Vol. 3,No. 2, pp. 431\u2013483, 1981.","journal-title":"ACM Trans. on Prog. Lang. and Sys."},{"key":"207109_CR2","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre, \u201cInvest: A tool for the verification of invariants,\u201d In A.J. Hu and M.Y. Vardi, editors, Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, Springer-Verlag, pp. 505\u2013510, 1998.","DOI":"10.1007\/BFb0028771"},{"issue":"1","key":"207109_CR3","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0304-3975(96)00191-0","volume":"173","author":"N. Bj\u00f8rner","year":"1997","unstructured":"N. Bj\u00f8rner, A. Browne, and Z. Manna, \u201cAutomatic generation of invariants and intermediate assertions,\u201d Theoretical Computer Science, Vol. 173,No. 1, pp. 49\u201387, 1997.","journal-title":"Theoretical Computer Science"},{"key":"207109_CR4","doi-asserted-by":"crossref","unstructured":"M. Caplain, \u201cFinding invariant assertions for proving programs,\u201d in Proc. Int. Conf. on Reliable Software, Los Angeles, CA, 1975.","DOI":"10.1145\/800027.808436"},{"key":"207109_CR5","doi-asserted-by":"crossref","unstructured":"E. Clarke, E. Emerson, and E. Sistla, \u201cAutomatic verification of finite state concurrent systems using temporal logic specifications: A practical approach,\u201d in 10th ACM Symp. of Prog. Lang., ACM Press, 1983.","DOI":"10.1145\/567067.567080"},{"key":"207109_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot, \u201cAbstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints,\u201d in 4th ACM Symp. of Prog. Lang., ACM Press, pp. 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"issue":"8","key":"207109_CR7","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"E.W. Dijkstra, \u201cGuarded commands, nondeterminacy, and formal derivation,\u201d Comm. ACM, Vol. 18,No. 8, pp. 453\u2013457, 1975.","journal-title":"Comm. ACM"},{"key":"207109_CR8","series-title":"Research report","volume-title":"The semiautomatic generation of inductive assertions for proving program correctness","author":"B. Elspas","year":"1974","unstructured":"B. Elspas, \u201cThe semiautomatic generation of inductive assertions for proving program correctness,\u201d Research report, SRI, Menlo Park, CA, 1974."},{"key":"207109_CR9","doi-asserted-by":"crossref","unstructured":"R.W. Floyd, \u201cAssigning meanings to programs,\u201d in Int. Proc. Symp. on Appl. Math. 19, American Mathematical Society, pp. 19\u201332. 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"207109_CR10","doi-asserted-by":"crossref","unstructured":"S.M. German and B. Wegbreit, \u201cA synthesizer of inductive assertions,\u201d IEEE Trans. on Software Engineering, Vol. 1, pp. 68\u201375, March 1975.","DOI":"10.1109\/TSE.1975.6312821"},{"key":"207109_CR11","doi-asserted-by":"crossref","unstructured":"K. Havelund and N. Shankar, \u201cExperiments in theorem proving and model checking for protocol verification,\u201d in Formal Methods Europe, FME'96 Symposium, volume 1051 of Lecture Notes in Computer Science, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"207109_CR12","doi-asserted-by":"crossref","unstructured":"L. Helmink, M. Sellink, and F. Vaandrager, \u201cProof-checking a data link protocol,\u201d Technical Report CS-R9420, Centrum voor Wiskunde en Informatica (CWI), March 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"207109_CR13","unstructured":"S. Katz and Z. Manna, \u201cA heuristic approach to program verification,\u201d in Proc. 3rd Int. Joint Conf. on Artificial Intelligence, Stanford, CA, pp. 500\u2013512, 1973."},{"issue":"4","key":"207109_CR14","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S. Katz","year":"1976","unstructured":"S. Katz and Z. Manna, \u201cLogical analysis of programs,\u201d Comm. ACM, Vol. 19,No. 4, pp. 188\u2013206, 1976.","journal-title":"Comm. ACM"},{"issue":"8","key":"207109_CR15","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L. Lamport","year":"1974","unstructured":"L. Lamport, \u201cA new solution of Dijkstra's concurrent programming problem,\u201d Comm. ACM, Vol. 17,No. 8, pp. 453\u2013455, 1974.","journal-title":"Comm. ACM"},{"key":"207109_CR16","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specification,\u201d in POPL, pp. 97\u2013107, 1985.","DOI":"10.1145\/318593.318622"},{"key":"207109_CR17","series-title":"Technical report","doi-asserted-by":"crossref","DOI":"10.21236\/ADA324036","volume-title":"STeP: The Stanford Temporal Prover","author":"Z. Manna","year":"1994","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8ner, A. Browne, E. Chang, M. Colon, L. de Alfaro, H. Devarajan, H. Sipma, and T. Uribe, \u201cSTeP: The Stanford Temporal Prover,\u201d Technical report, Stanford Univ., Stanford, CA, 1994."},{"key":"207109_CR18","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":"207109_CR19","doi-asserted-by":"crossref","unstructured":"S. Mauw and G.V. Editors, Algebraic Specification of Communication Protocols, number 36 in Cambridge Tracts in Theoretical Computer Science, 1993.","DOI":"10.1017\/CBO9780511721625"},{"issue":"2","key":"207109_CR20","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries, \u201cAn axiomatic proof technique for parallel programs,\u201d Acta Informatica, Vol. 6,No. 2, pp. 319\u2013340, 1976.","journal-title":"Acta Informatica"},{"issue":"2","key":"207109_CR21","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke, \u201cFormal verification for fault-tolerant architectures: Prolegomena to the design of PVS,\u201d IEEE Trans. on Software Engineering, Vol. 21,No. 2, pp. 107\u2013125, 1995.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"207109_CR22","doi-asserted-by":"crossref","unstructured":"J.P. Queille and J. Sifakis, \u201cSpecification and verification of concurrent systems in CESAR,\u201d in Proc. 5th Int. Symp. on Programming, volume 137 of Lecture Notes in Computer Science, Springer-Verlag, pp. 337\u2013351, 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"207109_CR23","doi-asserted-by":"crossref","unstructured":"B.K. Szymanski, \u201cA simple solution to Lamport's concurrent programming problem verification,\u201d in Proc. Int. Conf. on Supercomputing Sys., pp. 621\u2013626, 1988.","DOI":"10.1145\/55364.55425"},{"key":"207109_CR24","unstructured":"B.K. Szymanski and J.M. Vidal, \u201cAutomatic verfication of a class of symmetric parallel programs,\u201d in Proc. 13th IFIP World Computer Congress, 1994."},{"key":"207109_CR25","unstructured":"M. Vardi and P. Wolper, \u201cAn automata-theoretic approach to automatic program verification,\u201d in 1st Symp. on Logic in Computer Science, IEEE, 1986."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008744030390.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008744030390\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008744030390.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:35:23Z","timestamp":1754368523000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008744030390"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,7]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,7]]}},"alternative-id":["207109"],"URL":"https:\/\/doi.org\/10.1023\/a:1008744030390","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1999,7]]}}}