{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:43:03Z","timestamp":1754484183582},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"license":[{"start":{"date-parts":[[1998,1,1]],"date-time":"1998-01-01T00:00:00Z","timestamp":883612800000},"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":[[1998]]},"DOI":"10.1007\/bfb0028771","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"505-510","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["InVeSt : A tool for the verification of invariants"],"prefix":"10.1007","author":[{"given":"S.","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"Y.","family":"Lakhnech","sequence":"additional","affiliation":[]},{"given":"S.","family":"Owre","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,18]]},"reference":[{"key":"46_CR1","unstructured":"S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Accepted in Formal Methods in System Design. To appear."},{"key":"46_CR2","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems automatically and compositionally. Accepted in CAV'98, 1998.","DOI":"10.1007\/BFb0028755"},{"key":"46_CR3","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful techniques for the automatic generation of invariants. In CAV'96, volume 1102 of LNCS. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_80"},{"key":"46_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 10th ACM symp. of Prog. Lang. ACM Press, 1983.","DOI":"10.1145\/567067.567080"},{"key":"46_CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5), 1994.","DOI":"10.1145\/186025.186051"},{"key":"46_CR6","unstructured":"D. Dams.Abstract interpretation and partition refinement for model checking. PhD thesis, Technical University of Eindhoven, 1996."},{"key":"46_CR7","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL, ECTL and CTL. In PROCOMET. IFIP Transactions, North-Holland\/Elsevier, 1994."},{"key":"46_CR8","volume-title":"Mathematical Theory of Program Cortrectness","author":"J.W. Bakker de","year":"1980","unstructured":"J.W. de Bakker. Mathematical Theory of Program Cortrectness. Prentice-Hall, NJ., 1980."},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In FME'96, volume 1051 of LNCS. Springer-verlag, 1996.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"J. Hooman. Verifying part of the access.bus protocol using PVS. In Proc. 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1026 of LNCS. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60692-0_43"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer-Aided Verification of Coordinating Processes, the automata theoretic approach. Princeton Series in Computer Science. 1994.","DOI":"10.1515\/9781400864041"},{"key":"46_CR12","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), 1995.","DOI":"10.1007\/BF01384313"},{"key":"46_CR13","unstructured":"D. E. Long. Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon, 1993."},{"key":"46_CR14","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. STeP: The Stanford Temporal Prover. Technical report, Stanford Univ., Stanford, CA, 1994."},{"issue":"1","key":"46_CR15","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83(1):97\u2013130, 1991.","journal-title":"Theoretical Computer Science"},{"key":"46_CR16","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":"46_CR17","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan. Symbolic model checking. Kluwer Academic Publishers, Boston, 1993."},{"key":"46_CR18","doi-asserted-by":"crossref","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. volume 1102 of LNCS, pages 411\u2013414. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_91"},{"issue":"2","key":"46_CR19","doi-asserted-by":"publisher","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. Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, Feb. 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"46_CR20","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"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028771","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:00:30Z","timestamp":1558270830000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028771"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0028771","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]},"assertion":[{"value":"18 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}