{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:11Z","timestamp":1761611171784},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646082"},{"type":"electronic","value":"9783540693390"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0028755","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:48:09Z","timestamp":1133419689000},"page":"319-331","source":"Crossref","is-referenced-by-count":80,"title":["Computing abstractions of infinite state systems compositionally and automatically"],"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":"30_CR1","unstructured":"S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Accepted in Formal Methods in System Design. To appear."},{"key":"30_CR2","doi-asserted-by":"crossref","unstructured":"N. Bj\u00f8rner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1), 1997.","DOI":"10.1016\/S0304-3975(96)00191-0"},{"key":"30_CR3","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":"30_CR4","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"},{"key":"30_CR5","unstructured":"D. Dams. Abstract interpretation and partition refinement for model checking. PhD thesis, Technical University of Eindhoven, 1996."},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, G. D\u00f6hmen, R. Herrmann, P. Kelb, and H. Pargmann. Model checking using adaptive state and data abstraction. In CAV'94, volume 818 of LNCS. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_75"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Generation of reduced models for checking fragments of CTL. In CAV'93, volume 697 of LNCS. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_39"},{"key":"30_CR8","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL, ECTL and CTL In ROCOMET'94. IFIP Transactions, North-Holland\/Elsevier, 1994."},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Transactions in Programming Languages and Systems, 19(2), 1997.","DOI":"10.1145\/244795.244800"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"J. Dingel and Th. Filkorn. Model checking for infinite state systems using data abstraction. In CAV'95, volume 939 of LNCS, pages 54\u201369. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60045-0_40"},{"key":"30_CR11","unstructured":"S. Graf. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Accepted to Distributed Computing, 1995."},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In CAV'93, volume 697 of LNCS. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_7"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In CAV'97, volume 1254 of LNCS, 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"30_CR14","unstructured":"F.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large packets. In A case study in computer checked verification, Logic Group Preprint Series 100. Utrecht University, 1993."},{"key":"30_CR15","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":"30_CR16","doi-asserted-by":"crossref","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. Technical Report CS-119420, CWI, March 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"30_CR17","unstructured":"P. Kelb. Abstraktionstechniken f\u00fcr Automatische Verifikationsmethoden. PhD thesis, University of Oldenburg, 1995."},{"key":"30_CR18","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":"30_CR19","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":"30_CR20","unstructured":"D. E. Long. Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon, 1993."},{"issue":"1","key":"30_CR21","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":"30_CR22","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":"30_CR23","doi-asserted-by":"crossref","unstructured":"S. Mauw and G.J. Veltink editors. Algebraic Specification of Communication Protocols. Number 36 in Cambridge Tracts in Theoretical Computer Science. 1993.","DOI":"10.1017\/CBO9780511721625"},{"key":"30_CR24","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 Publ., Boston, 1993."},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"O. M\u00fcller and T. Nipkow.Combining model checking and deduction for I\/O-utomata. In TACAS'95, volume 1019 of LNCS, 1995.","DOI":"10.1007\/3-540-60630-0_1"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 1995.","DOI":"10.1109\/32.345827"},{"key":"30_CR27","doi-asserted-by":"crossref","unstructured":"J. X. Su, D. L. Dill, and C. Barrett. Automatic generation of invariants in processor verification. In FMCAD '96, volume 1166 of LNCS, 1996.","DOI":"10.1007\/BFb0031822"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0028755","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T08:24:12Z","timestamp":1586593452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028755"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646082","9783540693390"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/bfb0028755","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}