{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:16Z","timestamp":1725487216207},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418658"},{"type":"electronic","value":"9783540453192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_8","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T11:50:47Z","timestamp":1184586647000},"page":"98-112","source":"Crossref","is-referenced-by-count":36,"title":["Incremental Verification by Abstraction"],"prefix":"10.1007","author":[{"given":"Y.","family":"Lakhnech","sequence":"first","affiliation":[]},{"given":"S.","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"S.","family":"Berezin","sequence":"additional","affiliation":[]},{"given":"S.","family":"Owre","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-56922-7_4","volume-title":"Computer Aided Verification: 5th International Conference","author":"F. Balarin","year":"1993","unstructured":"F. Balarin and A.L. Sangiovanni-Vincentelli. Am iterative approach to language containment. In Costas Courcoubetis, editor, Computer Aided Verification: 5th International Conference, volume 697 of Lecture Notes in Computer Science, pages 29\u201340. Springer-Verlag, 1993."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"K.A. Barlett, R.A. Scantlebury, and P.T. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5), 1969.","DOI":"10.1145\/362946.362970"},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201900","author":"K. Baukus","year":"2000","unstructured":"K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. Abstracting WS1S Systems to Verify Parameterized Networks. In S. Graf and M. Schwartzbach, editors, TACAS\u201900, volume 1785 of Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"8_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/3-540-45352-0_24","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"K. Baukus","year":"2000","unstructured":"K. Baukus, Y. Lakhnech, and K. Stahl. Verifying universal properties of parameterized networks. In M. Joseph, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1926 of Lecture Notes in Computer Science, pages 291\u2013304. Springer-Verlag, 2000."},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"S. Bensalem and Y. Lakhnech. Automatic generation of invariants. Formal Methods in System Design, 1999. To appear.","DOI":"10.1023\/A:1008744030390"},{"key":"8_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems automatically and compositionally. In Alan J. Hu and Moshe Y. vardi, editors, Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 319\u2013331. Springer-Verlag, 1998."},{"key":"8_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/BFb0028771","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. Invest: A tool for the verification of invariants. In Alan J. Hu and Moshe Y. vardi, editors, Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 505\u2013510. Springer-Verlag, 1998."},{"key":"8_CR8","unstructured":"A. Bouajjani, J. Cl. Fernandez, and N. Halbwachs. Minimal model generation. In Workshop on Computer-aided Verification. Rutgers-American Mathematical Society, Association for Computing Machinery, June 1990."},{"key":"8_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/3-540-61648-9_48","volume-title":"4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT\u201996","author":"A. Bouajjani","year":"1996","unstructured":"Ahmed Bouajjani, Yassine Lakhnech, and Sergio Yovine. Model checking for extended timed temporal logics. In B. Jonsson and J. Parrow, editors, 4th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems FTRTFT\u201996, volume 1135 of Lecture Notes in Computer Science, pages 306\u2013326. Springer-Verlag, 1996."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Bettina Buth, Karl-Heinz Buth, Martin Fr\u00e4anzle, Burghard v. Karger, Yassine Lakhnech, Hans Langmaack, and Markus M\u00fculler-Olm. Provably correct compiler development and implementation. Compiler Construction, 1992.","DOI":"10.1007\/3-540-55984-1_14"},{"key":"8_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, Lecture Notes in Computer Science, pages 154\u2013169. Springer-Verlag, 2000."},{"key":"8_CR12","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":"8_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/3-540-60360-3_32","volume-title":"Static Analysis","author":"R. Cleaveland","year":"1995","unstructured":"R. Cleaveland, P. Iyer, and D. Yankelevitch. Optimality in abstractions of model checking. In A Mycroft, editor, Static Analysis, volume 983 of Lecture Notes in Computer Science, pages 51\u201363, 1995."},{"key":"8_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Generating finite-state abstractions of reactive systems using decision procedures","author":"M. A. Colon","year":"1998","unstructured":"M. A. Colon and T. E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. Lecture Notes in Computer Science, 1427:293\u2013304, 1998."},{"key":"8_CR15","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":"8_CR16","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6th ACM POPL, pages 269\u2013282, 1979.","DOI":"10.1145\/567752.567778"},{"key":"8_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Saidi. Construction of abstract state graphs with PVS. In Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, 1997."},{"key":"8_CR18","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":"8_CR19","series-title":"Lect Notes Comput Sci","volume-title":"Formal Methods Europe, FME\u201996 Symposium","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal Methods Europe, FME\u201996 Symposium, volume 1051 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. Technical Report CS-R9420, Centrum voor Wiskunde en Informatica (CWI), March 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"M. R. Henzinger, T. A. Henzinger, and P. W. Kopke. Computing simulations on finite and infinite graphs. In 36th Annual Symposium on Foundations of Computer Science (FOCS\u201995), pages 453\u2013462, Los Alamitos, October 1995. IEEE Computer Society Press.","DOI":"10.1109\/SFCS.1995.492576"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, To appear, 2000.","DOI":"10.1006\/inco.2000.3000"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Computer-Aided Verification of Coordinating Processes, the automata theoretic approach. Princeton Series in Computer Science. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"David Lee and Mihalis Yannakakis. Online minimization of transition systems (extended abstract). In Proceedings of the Twenty-Fourth Annual ACM Symposium on the Theory of Computing, pages 264\u2013274, Victoria, British Columbia, Canada, 4\u20136 May 1992.","DOI":"10.1145\/129712.129738"},{"key":"8_CR25","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":"8_CR26","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":"8_CR27","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":"8_CR28","unstructured":"S.S. Muchnick and N. D. Jones, editors. Program Flow Analysis. Prentice-Hall, 1981."},{"key":"8_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/10722167_33","volume-title":"Computer Aided Verification","author":"K. S. Namjoshi","year":"2000","unstructured":"K. S. Namjoshi and R. P. Kurshan. Syntactic program transformations for automatic abstraction. In Computer Aided Verification, Lecture Notes in Computer Science, pages 435\u2013449. Springer-Verlag, 2000."},{"key":"8_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/3-540-61474-5_70","volume-title":"8th International Conference on Computer Aided Verification","author":"H. Sipma","year":"1996","unstructured":"H. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. In R. Alur and T.A. Henzinger, editors, 8th International Conference on Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 208\u2013219. Springer-Verlag, 1996."}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,30]],"date-time":"2019-04-30T23:10:24Z","timestamp":1556665824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}