{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:41:03Z","timestamp":1725550863878},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_8","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"97-112","source":"Crossref","is-referenced-by-count":7,"title":["Decidability of Invariant Validation for Paramaterized Systems"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Fontaine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E. Pascal","family":"Gribomont","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"8_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Handling global conditions in parametrized system verification","author":"P. A. Abdulla","year":"1999","unstructured":"P. A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parametrized system verification. In Computer Aided Verification Conference, volume 1633 of Lecture Notes in Computer Science, pages 134\u2013145. Springer-Verlag, July 1999."},{"issue":"6","key":"8_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K. R. Apt","year":"1986","unstructured":"K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22(6):307\u2013309, May 1986.","journal-title":"Information Processing Letters"},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 221\u2013234. Springer-Verlag, July 2001."},{"issue":"2","key":"8_CR4","first-page":"141","volume":"7","author":"K. Baukus","year":"2001","unstructured":"K. Baukus, Y. Lakhnech, and K. Stahl. Verification of Parameterized Protocols. Journal of Universal Computer Science, 7(2):141\u2013158, Feb. 2001.","journal-title":"Journal of Universal Computer Science"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"P. Bernays and M. Sch\u00f6nfinkel. Zum Entscheidungsproblem der mathematischen Logik. Math. Annalen, 99:342\u2013372, 1928.","journal-title":"Math. Annalen"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"N. S. Bj\u00f8rner, Z. Manna, H. B. Sipma, and T. E. Uribe. Deductive verification of real-time systems using STeP. TCS: Theoretical Computer Science, 253, 2001.","DOI":"10.1016\/S0304-3975(00)00088-8"},{"key":"8_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 403\u2013418. Springer-Verlag, July 2000."},{"key":"8_CR8","volume-title":"Parallel Program Design","author":"K. M. Chandy","year":"1988","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, Reading, Massachusetts, 1988."},{"key":"8_CR9","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"8_CR10","volume-title":"The Decision Problem: Solvable Classes of Quantificational Formulas","author":"B. Dreben","year":"1979","unstructured":"B. Dreben and W. D. Goldfarb. The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading, Massachusetts, 1979."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In Computer Aided Verification, volume 1102, pages 87\u201398. Springer-Verlag, July 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"8_CR12","volume-title":"Perspectives in Mathematical Logic","author":"H.-D. Ebbinghaus","year":"1995","unstructured":"H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1995."},{"key":"8_CR13","volume-title":"A Mathematical Introduction to Logic","author":"H. B. Enderton","year":"1972","unstructured":"H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, Inc., Orlando, Florida, 1972."},{"key":"8_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Springer-Verlag, Berlin, 1990."},{"key":"8_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36078-6_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Fontaine","year":"2002","unstructured":"P. Fontaine and E. P. Gribomont. Using BDDs with combinations of theories. In Logic for Programming, Artificial Intelligence, and Reasoning, volume 2514 of Lecture Notes in Computer Science. Springer, 2002."},{"issue":"2","key":"8_CR16","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the ACM, 39(2):377\u2013429, Apr. 1992.","journal-title":"Journal of the ACM"},{"issue":"3","key":"8_CR17","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675\u2013735, July 1992.","journal-title":"Journal of the ACM"},{"key":"8_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-61474-5_69","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1996","unstructured":"S. Graf and H. Sa\u00efdi. Verifying invariants using theorem proving. In Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 196\u2013207. Springer Verlag, 1996."},{"issue":"1","key":"8_CR19","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0304-3975(99)00217-0","volume":"239","author":"E. P. Gribomont","year":"2000","unstructured":"E. P. Gribomont. Simplification of boolean verification conditions. Theoretical Computer Science, 239(1):165\u2013185, May 2000.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"8_CR20","doi-asserted-by":"publisher","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"J. Y. Halpern","year":"1991","unstructured":"J. Y. Halpern. Presburger arithmetic with unary predicates is \u03c011 complete. The Journal of Symbolic Logic, 56(2):637\u2013642, June 1991.","journal-title":"The Journal of Symbolic Logic"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer and N. A. Lynch. The generalized railroad crossing \u2014 a case study in formal verification of real-time systems. In Proceedings 15th IEEE Real-Time Systems Symposium, San Juan, Puerto Rico, pages 120\u2013131, Dec. 1994.","DOI":"10.1109\/REAL.1994.342724"},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/BFb0054186","volume-title":"Tools and Algorithms for Construction and Analysis of Systems","author":"H. E. Jensen","year":"1998","unstructured":"H. E. Jensen and N. A. Lynch. A proof of burns n-process mutual exclusion algorithm using abstraction. In Tools and Algorithms for Construction and Analysis of Systems, volume 1384 of Lecture Notes in Computer Science, pages 409\u2013423. Springer-Verlag, Mar. 1998."},{"key":"8_CR23","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"Computer Aided Verification","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 424\u2013435. Springer-Verlag, 1997."},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. McMillan. A structural induction theorem for processes. In Principles of Distributed Computing, pages 239\u2013248. ACM Press, Aug. 1989.","DOI":"10.1145\/72981.72998"},{"key":"8_CR25","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"N. Lynch. Distributed Algorithms. Morgan Kaufmann, San Francisco, CS, 1996."},{"key":"8_CR26","unstructured":"G. C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, Oct. 1998. Available as Technical Report CMU-CS-98-154."},{"issue":"2","key":"8_CR27","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplifications by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, Oct. 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"A. Pnueli, S. Ruah, and L. D. Zuck. Automatic deductive verification with invisible invariants. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 82\u201397, 2001."},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"F. Ramsey. On a Problem of Formal Logic. Proceedings of the London Mathematical Society, 30:264\u2013286, 1930.","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"8_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-56922-7_23","volume-title":"Computer Aided Verification","author":"N. Shankar","year":"1993","unstructured":"N. Shankar. Verification of Real-Time Systems Using PVS. In Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 280\u2013291. Springer-Verlag, June 1993."},{"key":"8_CR31","series-title":"Lect Notes Comput Sci","first-page":"68","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 68\u201380. Springer-Verlag, June 1989."}],"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-36577-X_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T18:51:34Z","timestamp":1558983094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}