{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:43:36Z","timestamp":1725522216235},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540899815"},{"type":"electronic","value":"9783540899822"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-89982-2_39","type":"book-chapter","created":{"date-parts":[[2008,12,14]],"date-time":"2008-12-14T22:09:15Z","timestamp":1229292555000},"page":"440-454","source":"Crossref","is-referenced-by-count":9,"title":["Verification from Declarative Specifications Using Logic Programming"],"prefix":"10.1007","author":[{"given":"Marco","family":"Montali","sequence":"first","affiliation":[]},{"given":"Paolo","family":"Torroni","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Alberti","sequence":"additional","affiliation":[]},{"given":"Federico","family":"Chesani","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Gavanelli","sequence":"additional","affiliation":[]},{"given":"Evelina","family":"Lamma","sequence":"additional","affiliation":[]},{"given":"Paola","family":"Mello","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"7","key":"39_CR1","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1145\/359131.359136","volume":"22","author":"R.A. Kowalski","year":"1979","unstructured":"Kowalski, R.A.: Algorithm = logic + control. Communications of the ACM\u00a022(7), 424\u2013436 (1979)","journal-title":"Communications of the ACM"},{"key":"39_CR2","doi-asserted-by":"crossref","unstructured":"Singh, M.P.: Agent communication language: rethinking the principles. IEEE Computer, 40\u201347 (December 1998)","DOI":"10.1109\/2.735849"},{"issue":"4","key":"39_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1380572.1380578","volume":"9","author":"M. Alberti","year":"2008","unstructured":"Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Verifiable agent interaction in abductive logic programming: the SCIFF framework. ACM Transactions on Computational Logic\u00a09(4), 1\u201343 (2008)","journal-title":"ACM Transactions on Computational Logic"},{"key":"39_CR4","doi-asserted-by":"crossref","unstructured":"Nalepa, G.: Proposal of business process and rules modeling with the xtt method. In: International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 500\u2013506 (2007)","DOI":"10.1109\/SYNASC.2007.58"},{"key":"39_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/11837862_18","volume-title":"Business Process Management Workshops","author":"M. Pesic","year":"2006","unstructured":"Pesic, M., van der Aalst, W.M.P.: A declarative approach for flexible business processes management. In: Eder, J., Dustdar, S. (eds.) BPM Workshops 2006. LNCS, vol.\u00a04103, pp. 169\u2013180. Springer, Heidelberg (2006)"},{"key":"39_CR6","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 995\u20131072. MIT Press, Cambridge (1990)"},{"key":"39_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-73370-6_11","volume-title":"Model Checking Software","author":"K.Y. Rozier","year":"2007","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Model Checking Software. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 149\u2013167. Springer, Heidelberg (2007)"},{"key":"39_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1993.1025","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Information and Computation\u00a0104, 35\u201377 (1993)","journal-title":"Information and Computation"},{"issue":"6","key":"39_CR9","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1093\/logcom\/2.6.719","volume":"2","author":"A.C. Kakas","year":"1992","unstructured":"Kakas, A.C., Kowalski, R.A., Toni, F.: Abductive logic programming. J. Log. Comput.\u00a02(6), 719\u2013770 (1992)","journal-title":"J. Log. Comput."},{"key":"39_CR10","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0004-3702(94)90027-2","volume":"66","author":"H. B\u00fcrckert","year":"1994","unstructured":"B\u00fcrckert, H.: A resolution principle for constrained logics. Artificial Intelligence\u00a066, 235\u2013271 (1994)","journal-title":"Artificial Intelligence"},{"key":"39_CR11","unstructured":"Montali, M., Pesic, M., van der Aalst, W.M., Chesani, F., Mello, P., Storari, S.: Declarative specification and verification of service choreographies. ACM Transaction on the Web (submitted, 2008)"},{"key":"39_CR12","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1109\/EDOC.2007.14","volume-title":"11th IEEE International Enterprise Distributed Object Computing Conference (EDOC 2007)","author":"M. Pesic","year":"2007","unstructured":"Pesic, M., Schonenberg, H., van der Aalst, W.: Declare: Full support for loosely-structured processes. In: 11th IEEE International Enterprise Distributed Object Computing Conference (EDOC 2007), Annapolis, Maryland, USA, October 15-19, 2007, pp. 287\u2013300. IEEE Computer Society, Los Alamitos (2007)"},{"key":"39_CR13","series-title":"Lecture Notes in Artificial Intelligence","first-page":"157","volume-title":"CLIMA VIII","author":"V. Bryl","year":"2008","unstructured":"Bryl, V., Mello, P., Montali, M., Torroni, P., Zannone, N.: B-Tropos: Agent-oriented requirements engineering meets computational logic for declarative business process modeling and verification. In: Sadri, F., Satoh, K. (eds.) CLIMA VIII. LNCS (LNAI), vol.\u00a05056, pp. 157\u2013176. Springer, Heidelberg (2008)"},{"issue":"20","key":"39_CR14","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. Journal of Logic Programming\u00a019(20), 503\u2013582 (1994)","journal-title":"Journal of Logic Programming"},{"issue":"1-3","key":"39_CR15","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0743-1066(98)10005-5","volume":"37","author":"T. Fr\u00fchwirth","year":"1998","unstructured":"Fr\u00fchwirth, T.: Theory and practice of constraint handling rules. Journal of Logic Programming\u00a037(1-3), 95\u2013138 (1998)","journal-title":"Journal of Logic Programming"},{"key":"39_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/11562931_14","volume-title":"Proceedings of Logic Programming, 21st International Conference, ICLP 2005","author":"H. Christiansen","year":"2005","unstructured":"Christiansen, H., Dahl, V.: HYPROLOG: A new logic programming language with assumptions and abduction. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol.\u00a03668, pp. 159\u2013173. Springer, Heidelberg (2005)"},{"key":"39_CR17","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., Vardi, M.Y.: Model checking vs. theorem proving: A manifesto. In: Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, pp. 151\u2013176 (1991)","DOI":"10.1016\/B978-0-12-450010-5.50015-3"},{"key":"39_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-45619-8_3","volume-title":"Logic Programming","author":"A. Russo","year":"2002","unstructured":"Russo, A., Miller, R., Nuseibeh, B., Kramer, J.: An abductive approach for analysing event-based requirements specifications. In: Stuckey, P. (ed.) ICLP 2002. LNCS, vol.\u00a02401, pp. 22\u201337. Springer, Heidelberg (2002)"},{"issue":"4","key":"39_CR19","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer\u00a02(4), 410\u2013425 (2000)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"3\/4","key":"39_CR20","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1504\/IJAOSE.2007.016267","volume":"1","author":"G. Casella","year":"2007","unstructured":"Casella, G., Mascardi, V.: West2east: exploiting web service technologies to engineer agent-based software. IJAOSE\u00a01(3\/4), 396\u2013434 (2007)","journal-title":"IJAOSE"},{"key":"39_CR21","doi-asserted-by":"crossref","unstructured":"Li, B., Iijima, J.: Architecture on a hybrid business process design and verification system. In: International Conference on Wireless Communications, Networking and Mobile Computing (WiCom), pp. 6199\u20136204 (2007)","DOI":"10.1109\/WICOM.2007.1520"},{"issue":"1","key":"39_CR22","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M. Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic\u00a02(1), 12\u201356 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"39_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","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 clp. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"39_CR24","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1109\/REAL.1997.641285","volume-title":"Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 1997)","author":"G. Gupta","year":"1997","unstructured":"Gupta, G., Pontelli, E.: A constraint-based approach for specification and verification of real-time systems. In: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 1997), pp. 230\u2013239. IEEE Computer Society, Los Alamitos (1997)"},{"key":"39_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-74610-2_4","volume-title":"Logic Programming","author":"G. Gupta","year":"2007","unstructured":"Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive logic programming and its applications. In: Dahl, V., Niemel\u00e4, I. (eds.) ICLP 2007. LNCS, vol.\u00a04670, pp. 27\u201344. Springer, Heidelberg (2007)"},{"key":"39_CR26","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1109\/REAL.2004.5","volume-title":"Proceedings of the 25th IEEE Real-Time Systems Symposium (RTSS 2004)","author":"J. Jaffar","year":"2004","unstructured":"Jaffar, J., Santosa, A.E., Voicu, R.: A clp proof method for timed automata. In: Proceedings of the 25th IEEE Real-Time Systems Symposium (RTSS 2004), pp. 175\u2013186. IEEE Computer Society, Los Alamitos (2004)"}],"container-title":["Lecture Notes in Computer Science","Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-89982-2_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T04:05:47Z","timestamp":1557979547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-89982-2_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540899815","9783540899822"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-89982-2_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}