{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T05:16:45Z","timestamp":1737609405575,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540697350"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69738-1_24","type":"book-chapter","created":{"date-parts":[[2007,11,12]],"date-time":"2007-11-12T12:58:07Z","timestamp":1194872287000},"page":"329-345","source":"Crossref","is-referenced-by-count":2,"title":["The Constraint Database Approach to Software Verification"],"prefix":"10.1007","author":[{"given":"Peter","family":"Revesz","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"24_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., et al.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"24_CR2","series-title":"Lecture Notes in Artificial Intelligence","first-page":"1","volume-title":"Abstraction, Reformulation and Approximation","author":"S. Anderson","year":"2005","unstructured":"Anderson, S., Revesz, P.: Verifying the incorrectness of programs and automata. In: Zucker, J.-D., Saitta, L. (eds.) SARA 2005. LNCS (LNAI), vol.\u00a03607, pp. 1\u201313. Springer, Heidelberg (2005)"},{"key":"24_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"24_CR4","unstructured":"Colmerauer, A.: Note sur Prolog III. In: Proc. S\u00e9minaire Programmation en Logique, pp. 159\u2013174 (1986)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/b105073","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 17\u201319. Springer, Heidelberg (2005)"},{"key":"24_CR6","volume-title":"Proc. ACM Principles on Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. ACM Principles on Programming Languages, ACM Press, New York (1977)"},{"key":"24_CR7","volume-title":"Proc. ACM Principles on Programming Languages","author":"P. Cousot","year":"1978","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. ACM Principles on Programming Languages, ACM Press, New York (1978)"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model checking in. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, Springer, Heidelberg (1999)"},{"key":"24_CR9","unstructured":"Dincbas, M., Van Hentenryck, P., Simonis, H., Aggoun, A., Graf, T., Berthier, F.: The constraint logic programming language chip. In: Proc. Fifth Generation Computer Systems, Tokyo, Japan, pp.\u00a0693\u2013702 (1988)"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1009747629591","volume":"2","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Ols\u00e9n, H.: A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints\u00a02, 3\u20134 (1997)","journal-title":"Constraints"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-62718-9_2","volume-title":"Logic Program Synthesis and Transformation","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Richardson, J.D.C.: Symbolic verification with gap-order constraints. In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol.\u00a01207, pp. 20\u201337. Springer, Heidelberg (1997)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Delay analysis in synchronous programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, Springer, Heidelberg (1993)"},{"key":"24_CR14","unstructured":"Harvey, W., Stuckey, P.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proc. Australian Computer Science Conference (Australian Computer Science Communications), pp.\u00a0102\u201311 (1997)"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.L.: Constraint logic programming. In: Proc. 14th ACM Symposium on Principles of Programming Languages, pp.\u00a0111\u2013119 (1987)","DOI":"10.1145\/41625.41635"},{"issue":"20","key":"24_CR16","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: A survey. J. Logic Programming\u00a019(20), 503\u2013581 (1994)","journal-title":"J. Logic Programming"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Kanellakis, P.C., Kuper, G.M., Revesz, P.: Constraint query languages. In: Proc. ACM Symposium on Principles of Database Systems, pp.\u00a0299\u2013313 (1990)","DOI":"10.1145\/298514.298582"},{"issue":"1","key":"24_CR18","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1006\/jcss.1995.1051","volume":"51","author":"P.C. Kanellakis","year":"1995","unstructured":"Kanellakis, P.C., Kuper, G.M., Revesz, P.: Constraint query languages. Journal of Computer and System Sciences\u00a051(1), 26\u201352 (1995)","journal-title":"Journal of Computer and System Sciences"},{"key":"24_CR19","unstructured":"Kerbrat, A.: Reachable state space analysis of lotos specifications. In: Proc. 7th International Conference on Formal Description Techniques, pp.\u00a0161\u201376 (1994)"},{"volume-title":"Constraint Databases","year":"2000","key":"24_CR20","unstructured":"Kuper, G.M., Libkin, L., Paredaens, J. (eds.): Constraint Databases. Springer, Heidelberg (2000)"},{"key":"24_CR21","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5625.001.0001","volume-title":"Programming with Constraints: An Introduction","author":"K. Marriott","year":"1998","unstructured":"Marriott, K., Stuckey, P.J.: Programming with Constraints: An Introduction. MIT Press, Cambridge (1998)"},{"key":"24_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer, Norwell (1993)"},{"key":"24_CR23","first-page":"310","volume-title":"Proceedings Analysis, Slicing and Transformation","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: Proceedings Analysis, Slicing and Transformation, pp. 310\u2013319. IEEE Press, Los Alamitos (2001)"},{"key":"24_CR24","unstructured":"Pratt, V.: Two easy theories whose combination is hard. MIT Technical Report (1977)"},{"issue":"1","key":"24_CR25","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"P. Revesz","year":"1993","unstructured":"Revesz, P.: A closed-form evaluation for Datalog queries with integer (gap)-order constraints. Theoretical Computer Science\u00a0116(1), 117\u2013149 (1993)","journal-title":"Theoretical Computer Science"},{"key":"24_CR26","unstructured":"Revesz, P.: Datalog programs with difference constraints. In: Proc. 12th International Conference on Applications of Prolog. pp.\u00a069\u201376 (1999)"},{"key":"24_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44914-0_12","volume-title":"Abstraction, Reformulation, and Approximation","author":"P. Revesz","year":"2000","unstructured":"Revesz, P.: Reformulation and approximation in model checking. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol.\u00a01864, Springer, Heidelberg (2000)"},{"key":"24_CR28","volume-title":"Introduction to Constraint Databases","author":"P. Revesz","year":"2002","unstructured":"Revesz, P.: Introduction to Constraint Databases. Springer, Heidelberg (2002)"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"Revesz, P., Chen, R., Kanjamala, P., Li, Y., Liu, Y., Wang, Y.: The MLPQ\/GIS constraint database system. In: ACM SIGMOD International Conference on Management of Data (2000)","DOI":"10.1145\/342009.336590"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69738-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T06:57:30Z","timestamp":1737529050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69738-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540697350"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69738-1_24","relation":{},"subject":[]}}