{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T19:10:13Z","timestamp":1729624213590,"version":"3.28.0"},"reference-count":28,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1109\/sefm.2010.37","type":"proceedings-article","created":{"date-parts":[[2010,11,23]],"date-time":"2010-11-23T15:30:30Z","timestamp":1290526230000},"page":"244-254","source":"Crossref","is-referenced-by-count":9,"title":["SMT-based Verification of LTL Specification with Integer Constraints and its Application to Runtime Checking of Service Substitutability"],"prefix":"10.1109","author":[{"given":"Marcello M.","family":"Bersani","sequence":"first","affiliation":[]},{"given":"Luca","family":"Cavallaro","sequence":"additional","affiliation":[]},{"given":"Achille","family":"Frigeri","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Pradella","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2004.02.002"},{"key":"17","first-page":"27","article-title":"Automated generation of BPEL adapters","author":"brogi","year":"2006","journal-title":"Proceedings of ICSOC"},{"journal-title":"Web Services Business Process Execution Language Version 2 0","year":"2007","key":"18"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1109\/SERVICES-1.2008.52"},{"journal-title":"WS-ResourceProperties","year":"2003","author":"schaeck","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.22"},{"journal-title":"Improving Schema Mapping by Exploiting Domain Knowledge","year":"2008","author":"drumm","key":"14"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287669"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_47"},{"key":"21","first-page":"213","article-title":"Proving safety properties of infinite state systems by compilation into presburger arithmetic","author":"fribourg","year":"1997","journal-title":"Proc CONCUR"},{"journal-title":"Proc of FOCLASA","article-title":"Automatic generation of adaptation contracts","year":"2008","author":"marti?n","key":"20"},{"key":"22","first-page":"268","article-title":"Multiple counters automata, safety analysis and presburger arithmetic","author":"comon","year":"1998","journal-title":"Proc CAV"},{"journal-title":"Symbolic methods for exploring infinite state spaces","year":"1998","author":"boigelot","key":"23"},{"key":"24","first-page":"368","article-title":"TReX: A tool for reachability analysis of complex systems","author":"annichini","year":"2001","journal-title":"Proc CAV"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_10"},{"key":"26","first-page":"121","article-title":"An automata-theoretic approach to constraint LTL","author":"demri","year":"2002","journal-title":"Proc of FSTTCS"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/11901914_36"},{"key":"28","first-page":"155","article-title":"Lazy theorem proving for bounded model checking over infinite domains","author":"de moura","year":"2002","journal-title":"Proc CADE"},{"key":"3","first-page":"159","article-title":"An automatic approach to enabfe repfacement of conversational services","author":"cavallaro","year":"2009","journal-title":"Proc ICSOC\/ServiceWave"},{"journal-title":"LSDIS Lab Tech Rep LSDIS 05-001","article-title":"The METEOR-S approach for configuring and executing dynamic web processes","year":"2005","author":"verma","key":"2"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.696"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2010.21"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/PESOS.2009.5068824"},{"journal-title":"SMT-LIB 1 2","year":"2006","author":"ranise","key":"5"},{"key":"4","doi-asserted-by":"crossref","DOI":"10.1145\/1808984.1808996","article-title":"Synthesizing adapters for conversational web-services from their WSDL interface","author":"cavalfaro","year":"2010","journal-title":"Proceedings of SEAMS"},{"key":"9","first-page":"118","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Advances in Computers"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_17"}],"event":{"name":"2010 8th IEEE International Conference on Software Engineering and Formal Methods (SEFM)","start":{"date-parts":[[2010,9,13]]},"location":"Pisa, Italy","end":{"date-parts":[[2010,9,18]]}},"container-title":["2010 8th IEEE International Conference on Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5635422\/5637151\/05637436.pdf?arnumber=5637436","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,19]],"date-time":"2017-06-19T12:28:15Z","timestamp":1497875295000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5637436\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":28,"URL":"https:\/\/doi.org\/10.1109\/sefm.2010.37","relation":{},"subject":[],"published":{"date-parts":[[2010,9]]}}}
