{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:16:43Z","timestamp":1740097003008,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548031"},{"type":"electronic","value":"9783642548048"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54804-8_19","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T05:59:16Z","timestamp":1395381556000},"page":"276-290","source":"Crossref","is-referenced-by-count":10,"title":["SMT-Based Checking of SOLOIST over Sparse Traces"],"prefix":"10.1007","author":[{"given":"Marcello Maria","family":"Bersani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Domenico","family":"Bianculli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carlo","family":"Ghezzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sr\u0111an","family":"Krsti\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierluigi","family":"San Pietro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"19_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoreotical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoreotical Computer Science"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-40787-1_3","volume-title":"Runtime Verification","author":"D. Basin","year":"2013","unstructured":"Basin, D., Klaedtke, F., Marinovic, S., Z\u0103linescu, E.: Monitoring of temporal first-order properties with aggregations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol.\u00a08174, pp. 40\u201358. Springer, Heidelberg (2013)"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., San Pietro, P.: Bounded reachability for temporal logic over constraint systems. In: Proc. of TIME 2010, pp. 43\u201350. IEEE Computer Society (2010)","DOI":"10.1109\/TIME.2010.21"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-24288-5_7","volume-title":"Reachability Problems","author":"M.M. Bersani","year":"2011","unstructured":"Bersani, M.M., Frigeri, A., Rossi, M., San Pietro, P.: Completeness of the bounded satisfiability problem for constraint LTL. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol.\u00a06945, pp. 58\u201371. Springer, Heidelberg (2011)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-41036-9_8","volume-title":"Reachability Problems","author":"M.M. Bersani","year":"2013","unstructured":"Bersani, M.M., Rossi, M., Pietro, P.S.: Deciding continuous-time metric temporal logic with counting modalities. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol.\u00a08169, pp. 70\u201382. Springer, Heidelberg (2013)"},{"key":"19_CR6","unstructured":"Bersani, M.M., Rossi, M., San Pietro, P.: On the satisfiability of metric temporal logics over the reals. In: Proc. of AVOCS 2013 (2013)"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Bianculli, D., Ghezzi, C., Pautasso, C., Senti, P.: Specification patterns from research to industry: a case study in service-based applications. In: Proc. of ICSE 2012, pp. 968\u2013976. IEEE Computer Society (2012)","DOI":"10.1109\/ICSE.2012.6227125"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-35861-6_4","volume-title":"Formal Aspects of Component Software","author":"D. Bianculli","year":"2013","unstructured":"Bianculli, D., Ghezzi, C., San Pietro, P.: The tale of SOLOIST: a specification language for service compositions interactions. In: P\u0103s\u0103reanu, C.S., Sala\u00fcn, G. (eds.) FACS 2012. LNCS, vol.\u00a07684, pp. 55\u201372. Springer, Heidelberg (2013)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science\u00a02(15) (2006)","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"19_CR10","series-title":"LNBIP","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-20511-8_20","volume-title":"Business Process Management Workshops","author":"A. Burattin","year":"2011","unstructured":"Burattin, A., Sperduti, A.: PLG: A framework for the generation of business process models and their execution logs. In: Muehlen, M.z., Su, J. (eds.) BPM 2010 Workshops. LNBIP, vol.\u00a066, pp. 214\u2013219. Springer, Heidelberg (2011)"},{"issue":"3","key":"19_CR11","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1016\/j.ic.2006.09.006","volume":"205","author":"S. Demri","year":"2007","unstructured":"Demri, S., D\u2019Souza, D.: An automata-theoretic approach to constraint\u00a0LTL. Inf. Comput.\u00a0205(3), 380\u2013415 (2007)","journal-title":"Inf. Comput."},{"key":"19_CR12","unstructured":"van Dongen, B.: BPI challenge 2012 (2012), \n                    \n                      http:\/\/dx.doi.org\/10.4121\/uuid:3926db30-f712-4394-aebc-75976070e91f"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. of FMSP 1998, pp. 7\u201315. ACM (1998)","DOI":"10.1145\/298595.298598"},{"issue":"4","key":"19_CR14","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1145\/201024.201034","volume":"3","author":"M. Felder","year":"1994","unstructured":"Felder, M., Morzenti, A.: Validating real-time systems by history-checking TRIO specifications. ACM Trans. Softw. Eng. Methodol.\u00a03(4), 308\u2013339 (1994)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s10703-005-3399-3","volume":"27","author":"B. Finkbeiner","year":"2005","unstructured":"Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime executions. Form. Method Syst. Des.\u00a027, 253\u2013274 (2005)","journal-title":"Form. Method Syst. Des."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Kindermann, R., Junttila, T.A., Niemel\u00e4, I.: Bounded model checking of an MITL fragment for timed automata. CoRR abs\/1304.7209 (2013)","DOI":"10.1109\/ACSD.2013.25"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proc. of ICSE 2005, pp. 372\u2013381. ACM (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"19_CR18","unstructured":"Krsti\u0107, S.: Verification of quantitative properties of service-based applications. Master\u2019s thesis, Politecnico di Milano (December 2012)"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Leitner, P., Hummer, W., Dustdar, S.: A Monitoring Data Set for Evaluating QoS-Aware Service-Based Systems. In: Proc. of PESOS 2012, pp. 67\u201368 (2012)","DOI":"10.1109\/PESOS.2012.6225945"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-35632-2_14","volume-title":"Runtime Verification","author":"A. Mrad","year":"2013","unstructured":"Mrad, A., Ahmed, S., Hall\u00e9, S., Beaudet, \u00c9.: BabelTrace: A collection of transducers for trace validation. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol.\u00a07687, pp. 126\u2013130. Springer, Heidelberg (2013)"},{"issue":"2","key":"19_CR21","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst.\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In: Proc. of ESEC-FSE 2007, pp. 312\u2013320. ACM (2007)","DOI":"10.1145\/1287624.1287669"},{"key":"19_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2491509.2491514","volume":"20","author":"M. Pradella","year":"2013","unstructured":"Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. Softw.\u00a020, 1\u201320 (2013)","journal-title":"ACM Trans. Softw."},{"key":"19_CR24","unstructured":"Wozna-Szczesniak, B., Zbrzezny, A.: Checking MTL properties of discrete timed automata via bounded model checking. In: CS&P, vol.\u00a01032, pp. 469\u2013477. CEUR-WS.org (2013)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54804-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T08:00:32Z","timestamp":1558857632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54804-8_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548031","9783642548048"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54804-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}