SMT-based Checking of SOLOIST over Sparse Traces

Bersani, Marcello Maria; BIANCULLI, Domenico; Ghezzi, Carlo; Krstić, Srđan; San Pietro, Pierluigi

Communication publiée dans un ouvrage (Colloques, congrès, conférences scientifiques et actes)

Bersani, Marcello Maria; BIANCULLI, Domenico; Ghezzi, Carlo et al.

2014 • In Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)

Peer reviewed

Permalien
https://hdl.handle.net/10993/13535

Documents (1)Envoyer vers Détails Statistiques Bibliographie Publications similaires

Documents

Texte intégral

fase2014.pdf

Preprint Auteur (375.26 kB)

Demander un accès

Tous les documents dans ORBilu sont protégés par une licence d'utilisation.

Envoyer vers

RIS BibTex APA Chicago Permalink X Linkedin

Détails

Centre de recherche :

Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Software Verification and Validation Lab (SVV Lab)

Disciplines :

Sciences informatiques

Auteur, co-auteur :

Bersani, Marcello Maria

BIANCULLI, Domenico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)

Ghezzi, Carlo

Krstić, Srđan

San Pietro, Pierluigi

Co-auteurs externes :

yes

Langue du document :

Anglais

Titre :

SMT-based Checking of SOLOIST over Sparse Traces

Date de publication/diffusion :

2014

Nom de la manifestation :

17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)

Date de la manifestation :

5-13 April 2014

Manifestation à portée :

International

Titre de l'ouvrage principal :

Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)

Maison d'édition :

Springer

Peer reviewed :

Peer reviewed

Disponible sur ORBilu :

depuis le 20 décembre 2013

Statistiques

Nombre de vues

243 (dont 12 Unilu)

Nombre de téléchargements

2 (dont 2 Unilu)

Voir plus de statistiques

citations Scopus^®

citations Scopus^®
sans auto-citations

Bibliographie

Alur, R., Dill, D.L.: A theory of timed automata. Theoreotical Computer Science 126(2), 183-235 (1994)
Basin, D., Klaedtke, F.,Marinovic, S., Zǎlinescu, E.: Monitoring of temporal first-order properties with aggregations. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 40-58. Springer, Heidelberg (2013)
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-50. IEEE Computer Society (2010)
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. 6945, pp. 58-71. Springer, Heidelberg (2011)
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. 8169, pp. 70-82. Springer, Heidelberg (2013)
Bersani, M.M., Rossi, M., San Pietro, P.: On the satisfiability of metric temporal logics over the reals. In: Proc. of AVOCS 2013 (2013)
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-976. IEEE Computer Society (2012)
Bianculli, D., Ghezzi, C., San Pietro, P.: The tale of SOLOIST: a specification language for service compositions interactions. In: Pǎsǎreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 55-72. Springer, Heidelberg (2013)
Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer Science 2(15) (2006)
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. 66, pp. 214-219. Springer, Heidelberg (2011)
Demri, S., D'Souza, D.: An automata-theoretic approach to constraint LTL. Inf. Comput. 205(3), 380-415 (2007)
van Dongen, B.: BPI challenge 2012 (2012), http://dx.doi.org/10.4121/ uuid:3926db30-f712-4394-aebc-75976070e91f
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. of FMSP 1998, pp. 7-15. ACM (1998)
Felder, M., Morzenti, A.: Validating real-time systems by history-checking TRIO specifications. ACM Trans. Softw. Eng. Methodol. 3(4), 308-339 (1994)
Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime executions. Form. Method Syst. Des. 27, 253-274 (2005)
Kindermann, R., Junttila, T.A., Niemelä, I.: Bounded model checking of an MITL fragment for timed automata. CoRR abs/1304.7209 (2013)
Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: Proc. of ICSE 2005, pp. 372-381. ACM (2005)
Krstić, S.: Verification of quantitative properties of service-based applications. Master's thesis, Politecnico di Milano (December 2012)
Leitner, P., Hummer, W., Dustdar, S.: A Monitoring Data Set for Evaluating QoS-Aware Service-Based Systems. In: Proc. of PESOS 2012, pp. 67-68 (2012)
Mrad, A., Ahmed, S., Hallé, S., Beaudet, É.: BabelTrace: A collection of transducers for trace validation. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 126-130. Springer, Heidelberg (2013)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245-257 (1979)
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-320. ACM (2007)
Pradella,M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM Trans. Softw. 20, 1-20 (2013)
Wozna-Szczesniak, B., Zbrzezny, A.: Checking MTL properties of discrete timed automata via bounded model checking. In: CS&P, vol. 1032, pp. 469-477. CEUR-WS.org (2013)