{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T23:40:08Z","timestamp":1749598808334,"version":"3.41.0"},"publisher-location":"Cham","reference-count":96,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471686"},{"type":"electronic","value":"9783319471693"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_47","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T21:56:23Z","timestamp":1475618183000},"page":"609-625","source":"Crossref","is-referenced-by-count":3,"title":["Software that Meets Its Intent"],"prefix":"10.1007","author":[{"given":"Marieke","family":"Huisman","sequence":"first","affiliation":[]},{"given":"Herbert","family":"Bos","sequence":"additional","affiliation":[]},{"given":"Sjaak","family":"Brinkkemper","sequence":"additional","affiliation":[]},{"given":"Arie","family":"van Deursen","sequence":"additional","affiliation":[]},{"given":"Jan Friso","family":"Groote","sequence":"additional","affiliation":[]},{"given":"Patricia","family":"Lago","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"given":"Eelco","family":"Visser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"issue":"1\u20132","key":"47_CR1","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/s10994-013-5405-0","volume":"96","author":"F Aarts","year":"2014","unstructured":"Aarts, F., Kuppens, H., Tretmans, J., Vaandrager, F.W., Verwer, S.: Improving active Mealy machine learning for protocol conformance testing. Mach. Learn. 96(1\u20132), 189\u2013224 (2014)","journal-title":"Mach. Learn."},{"key":"47_CR2","unstructured":"Abreu, R., Zoeteweij, P., Van Gemund, A.J.C.: A new Bayesian approach to multiple intermittent fault diagnosis. In: International Joint Conference on Artificial Intelligence, IJCAI 2009, pp. 653\u2013658 (2009)"},{"key":"47_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B - System and Software Engineering","author":"J Abrial","year":"2010","unstructured":"Abrial, J.: Modeling in Event-B - System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"47_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-540-74792-5_4","volume-title":"Formal Methods for Components and Objects","author":"W Ahrendt","year":"2007","unstructured":"Ahrendt, W., Beckert, B., H\u00e4hnle, R., R\u00fcmmer, P., Schmitt, P.H.: Verifying object-oriented programs with KeY: a tutorial. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 70\u2013101. Springer, Heidelberg (2007)"},{"issue":"1","key":"47_CR5","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/j.infsof.2012.06.013","volume":"55","author":"R Ali","year":"2013","unstructured":"Ali, R., Dalpiaz, F., Giorgini, P.: Reasoning with contextual requirements: detecting inconsistency and conflicts. Inf. Softw. Technol. 55(1), 35\u201357 (2013)","journal-title":"Inf. Softw. Technol."},{"key":"47_CR6","doi-asserted-by":"crossref","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. Logical Methods Comput. Sci. 11(1:2), 1\u201366 (2015) paper 2","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"47_CR7","doi-asserted-by":"crossref","unstructured":"Andriesse, D., Bos, H., Slowinska, A.: Parallax: implicit code integrity verification using return-oriented programming. In: IEEE\/IFIP IC on Dependable Systems and Networks, DSN 2015, pp. 125\u2013135. IEEE Computer Society (2015)","DOI":"10.1109\/DSN.2015.12"},{"key":"47_CR8","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"issue":"5","key":"47_CR9","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1145\/1538917.1538919","volume":"31","author":"G Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. ACM Trans. Program. Lang. Syst. 31(5), 18 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"4","key":"47_CR10","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"47_CR11","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"47_CR12","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"47_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-319-06410-9_9","volume-title":"FM 2014: Formal Methods","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127\u2013131. Springer, Heidelberg (2014)"},{"key":"47_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/978-3-642-31424-7_4","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, p. 4. Springer, Heidelberg (2012)"},{"key":"47_CR15","doi-asserted-by":"crossref","unstructured":"Breaux, T.D., Vail, M.W., Ant\u00f3n, A.I.: Towards regulatory compliance: extracting rights and obligations to align requirements with regulations. In: IEEE International Requirements Engineering Conference, pp. 46\u201355 (2006)","DOI":"10.1109\/RE.2006.68"},{"key":"47_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-642-02161-9_3","volume-title":"Software Engineering for Self-Adaptive Systems","author":"Y Brun","year":"2009","unstructured":"Brun, Y., Di Marzo Serugendo, G., Gacek, C., Giese, H., Kienle, H., Litoiu, M., M\u00fcller, H., Pezz\u00e8, M., Shaw, M.: Engineering self-adaptive systems through feedback loops. In: Cheng, B.H.C., Lemos, R., Giese, H., Inverardi, P., Magee, J. (eds.) Software Engineering for Self-Adaptive Systems. LNCS, vol. 5525, pp. 48\u201370. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02161-9_3"},{"key":"47_CR17","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic manipulation of Boolean functions using a graphical representation. In: Ofek, H., O\u2019Neill, L.A. (eds.) 22nd ACM\/IEEE Conference on Design Automation, (DAC 1985), pp. 688\u2013694. ACM (1985)","DOI":"10.1109\/DAC.1985.1586017"},{"key":"47_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-15260-3","volume-title":"Introduction to Reliable and Secure Distributed Programming","author":"C Cachin","year":"2011","unstructured":"Cachin, C., Guerraoui, R., Rodrigues, L.E.T.: Introduction to Reliable and Secure Distributed Programming, 2nd edn. Springer, Heidelberg (2011)","edition":"2"},{"issue":"2","key":"47_CR19","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/s00165-016-0355-5","volume":"28","author":"S Cassel","year":"2016","unstructured":"Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. Formal Aspects Comput. 28(2), 233\u2013263 (2016)","journal-title":"Formal Aspects Comput."},{"key":"47_CR20","doi-asserted-by":"crossref","unstructured":"Chen, T.-H., Nagappan, M., Shihab, E., Hassan, A.E.: An empirical study of dormant bugs. In: 11th Working Conference on Mining Software Repositories, MSR 2014, pp. 82\u201391. ACM (2014)","DOI":"10.1145\/2597073.2597108"},{"key":"47_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"issue":"7","key":"47_CR22","doi-asserted-by":"crossref","first-page":"1113","DOI":"10.1109\/TCAD.2004.829807","volume":"23","author":"EM Clarke","year":"2004","unstructured":"Clarke, E.M., Gupta, A., Strichman, O.: SAT-based counterexample-guided abstraction refinement. IEEE Trans. CAD Integr. Circ. Syst. 23(7), 1113\u20131123 (2004)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"key":"47_CR23","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) 1st Workshop on Formal Integrated Development Environment, (F-IDE 2014). EPTCS, vol. 149, pp. 79\u201392 (2014)","DOI":"10.4204\/EPTCS.149.8"},{"key":"47_CR24","volume-title":"Security Requirements Engineering: Designing Secure Socio-Technical Systems","author":"F Dalpiaz","year":"2016","unstructured":"Dalpiaz, F., Paja, E., Giorgini, P.: Security Requirements Engineering: Designing Secure Socio-Technical Systems, 1st edn. MIT Press, Cambridge (2016)","edition":"1"},{"issue":"7","key":"47_CR25","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"47_CR26","unstructured":"de Bruijn, N.: A survey of the project AUTOMATH. In: To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pp. 579\u2013606. Academic Press (1980)"},{"key":"47_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-319-21690-4_16","volume-title":"Computer Aided Verification","author":"S Gouw de","year":"2015","unstructured":"de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273\u2013289. Springer, Heidelberg (2015)"},{"key":"47_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-35813-5_3","volume-title":"Software Engineering for Self-Adaptive Systems II","author":"R Lemos de","year":"2013","unstructured":"de Lemos, R., et al.: Software engineering processes for self-adaptive systems. In: Lemos, R., Giese, H., M\u00fcller, H.A., Shaw, M. (eds.) Software Engineering for Self-Adaptive Systems II. LNCS, vol. 7475, pp. 51\u201375. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35813-5_3"},{"key":"47_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"8","key":"47_CR30","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/2755501","volume":"58","author":"A Deursen van","year":"2015","unstructured":"van Deursen, A.: Testing web applications with state objects. Commun. ACM 58(8), 36\u201343 (2015)","journal-title":"Commun. ACM"},{"key":"47_CR31","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.tcs.2014.02.052","volume":"537","author":"V Diekert","year":"2014","unstructured":"Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29\u201341 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"47_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"47_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"47_CR34","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"47_CR35","first-page":"24","volume":"44","author":"S Erdweg","year":"2015","unstructured":"Erdweg, S., et al.: Evaluating and comparing language workbenches: existing results and benchmarks for the future. Comput. Lang. Syst. Struct. 44, 24\u201347 (2015)","journal-title":"Comput. Lang. Syst. Struct."},{"issue":"8","key":"47_CR36","first-page":"569","volume":"20","author":"A Finkelstein","year":"1994","unstructured":"Finkelstein, A., Gabbay, D., Hunter, A., Kramer, J., Nuseibeh, B.: Inconsistency handling in multiperspective specifications. IEEE TSE 20(8), 569\u2013578 (1994)","journal-title":"IEEE TSE"},{"issue":"1","key":"47_CR37","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1142\/S0218194092000038","volume":"2","author":"A Finkelstein","year":"1992","unstructured":"Finkelstein, A., Kramer, J., Nuseibeh, B., Finkelstein, L., Goedicke, M.: Viewpoints: a framework for integrating multiple perspectives in system development. Int. J. Softw. Eng. Knowl. Eng. 2(1), 31\u201357 (1992)","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"47_CR38","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511626975","volume-title":"Modelling Systems: Practical Tools and Techniques for Software Development","author":"J Fitzgerald","year":"2009","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques for Software Development, 2nd edn. Cambridge University Press, Cambridge (2009)","edition":"2"},{"key":"47_CR39","unstructured":"Fowler, M.: Language workbenches: The killer-app. for domain specific languages? (2005). http:\/\/www.martinfowler.com\/articles\/languageWorkbench.html"},{"key":"47_CR40","volume-title":"Domain-Specific Languages","author":"M Fowler","year":"2010","unstructured":"Fowler, M.: Domain-Specific Languages. Addison Wesley, Boston (2010)"},{"key":"47_CR41","doi-asserted-by":"crossref","unstructured":"Ganapathi, A., Patterson, D.A.: Crash data collection: a windows case study. In: DSN, pp. 280\u2013285. IEEE Computer Society (2005)","DOI":"10.1109\/DSN.2005.32"},{"key":"47_CR42","unstructured":"Gartner Inc. Smart cities will include 10 billion things by 2020 (2015). https:\/\/www.gartner.com\/doc\/3004417\/smart-cities-include-billion"},{"key":"47_CR43","doi-asserted-by":"crossref","unstructured":"Ghardallou, W., Diallo, N., Mili, A.: Program derivation by correctness enhancements. In: Refinement (2015)","DOI":"10.18293\/SEKE2016-095"},{"key":"47_CR44","doi-asserted-by":"crossref","unstructured":"Giuffrida, C., Cavallaro, L., Tanenbaum, A.S.: Practical automated vulnerability monitoring using program state invariants. In: DSN, October 2013","DOI":"10.1109\/DSN.2013.6575318"},{"key":"47_CR45","unstructured":"Giuffrida, C., Iorgulescu, C., Kuijsten, A., Tanenbaum, A.S.: Back to the future: fault-tolerant live update with time-traveling state transfer. In: LISA, October 2013"},{"key":"47_CR46","volume-title":"Starting with COMAL","author":"I Gratte","year":"1985","unstructured":"Gratte, I.: Starting with COMAL. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"47_CR47","doi-asserted-by":"crossref","unstructured":"Groote, J., Koorn, J., van Vlijmen, S.: The safety guaranteeing system at station Hoorn-Kersenboogerd (extended abstract). In: 10th Annual Conference on Computer Assurance (COMPASS 1995), pp. 57\u201368 (1995)","DOI":"10.1109\/CMPASS.1995.521887"},{"key":"47_CR48","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"J Groote","year":"2014","unstructured":"Groote, J., Mousavi, M.: Modeling and Analysis of Communicating Systems. The MIT Press, Cambridge (2014)"},{"issue":"1\/2","key":"47_CR49","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/A:1006366304347","volume":"24","author":"JF Groote","year":"2000","unstructured":"Groote, J.F., Warners, J.P.: The propositional formula checker HeerHugo. J. Autom. Reasoning 24(1\/2), 101\u2013125 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"47_CR50","volume-title":"Explore It!: Reduce Risk and Increase Confidence with Exploratory Testing","author":"E Hendrickson","year":"2013","unstructured":"Hendrickson, E.: Explore It!: Reduce Risk and Increase Confidence with Exploratory Testing. The Pragmatic Bookshelf, Raleigh (2013)"},{"issue":"10","key":"47_CR51","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"47_CR52","unstructured":"Huisman, M.: Reasoning about Java Programs in Higher Order Logic with PVS and Isabelle. Ph.D. thesis, University of Nijmegen (2001)"},{"key":"47_CR53","doi-asserted-by":"crossref","first-page":"2435","DOI":"10.1016\/j.scico.2012.11.009","volume":"78","author":"Y Hwong","year":"2013","unstructured":"Hwong, Y., Keiren, J., Kusters, V., Leemans, S., Willemse, T.: Formalising and analysing the control software of the compact muon solenoid experiment at the large hadron collider. Sci. Comput. Program. 78, 2435\u20132452 (2013)","journal-title":"Sci. Comput. Program."},{"key":"47_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-24606-7_5","volume-title":"Conceptual Modeling \u2013 ER 2011","author":"S Ingolfo","year":"2011","unstructured":"Ingolfo, S., Siena, A., Mylopoulos, J.: Establishing regulatory compliance for software requirements. In: Jeusfeld, M., Delcambre, L., Ling, T.-W. (eds.) ER 2011. LNCS, vol. 6998, pp. 47\u201361. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24606-7_5"},{"key":"47_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015)"},{"key":"47_CR56","series-title":"Synthesis Lectures on Data Management","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01839-8","volume-title":"Database Replication","author":"B Kemme","year":"2010","unstructured":"Kemme, B., Jim\u00e9nez, R., Pati\u00f1o-Martin\u00ednez, M.: Database Replication. Synthesis Lectures on Data Management. Morgan & Claypool Publishers, San Rafael (2010)"},{"issue":"10","key":"47_CR57","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/2714560","volume":"58","author":"P Lago","year":"2015","unstructured":"Lago, P., Ko\u00e7ak, S.A., Crnkovic, I., Penzenstadler, B.: Framing sustainability as a property of software quality. Commun. ACM 58(10), 70\u201378 (2015)","journal-title":"Commun. ACM"},{"issue":"1","key":"47_CR58","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"C Goues Le","year":"2012","unstructured":"Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: GenProg: a generic method for automatic software repair. IEEE Trans. Softw. Eng. 38(1), 54\u201372 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"47_CR59","unstructured":"Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual, Dept. of Computer Science, Iowa State University, February 2007. http:\/\/www.jmlspecs.org"},{"key":"47_CR60","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52, 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"47_CR61","doi-asserted-by":"crossref","unstructured":"Lewis, G.A., Lago, P., Avgeriou, P.: A decision model for cyber-foraging systems. In: Proceedings of the 13th Working IEEE\/IFIP Conference on Software Architecture (WICSA 2016), pp. 51\u201360. IEEE (2016)","DOI":"10.1109\/WICSA.2016.38"},{"key":"47_CR62","doi-asserted-by":"crossref","unstructured":"Matias, R., Prince, M., Borges, L., Sousa, C., Henrique, L.: An empirical exploratory study on operating system reliability. In: 29th Annual ACM Symposium on Applied Computing, SAC 2014, pp. 1523\u20131528. ACM (2014)","DOI":"10.1145\/2554850.2555021"},{"issue":"1","key":"47_CR63","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/2109205.2109208","volume":"6","author":"A Mesbah","year":"2012","unstructured":"Mesbah, A., van Deursen, A., Lenselink, S.: Crawling Ajax-based web applications through dynamic analysis of user interface state changes. ACM Trans. Web 6(1), 3 (2012)","journal-title":"ACM Trans. Web"},{"issue":"1","key":"47_CR64","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1109\/TSE.2011.28","volume":"38","author":"A Mesbah","year":"2012","unstructured":"Mesbah, A., van Deursen, A., Roest, D.: Invariant-based automated testing of modern web applications. IEEE Trans. Softw. Eng. 38(1), 35\u201353 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"47_CR65","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-92145-5","volume-title":"Touch of Class: Learning to Program Well with Objects and Contracts","author":"B Meyer","year":"2009","unstructured":"Meyer, B.: Touch of Class: Learning to Program Well with Objects and Contracts. Springer, Heidelberg (2009)"},{"key":"47_CR66","series-title":"Lectures in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"Calculus of Communicating Systems","author":"R Milner","year":"1980","unstructured":"Milner, R.: Calculus of Communicating Systems. Lectures in Computer Science, vol. 92. Springer, Heidelberg (1980)"},{"key":"47_CR67","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages (1997)","DOI":"10.1145\/263699.263712"},{"key":"47_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/978-3-662-46669-8_9","volume-title":"Programming Languages and Systems","author":"P Neron","year":"2015","unstructured":"Neron, P., Tolmach, A., Visser, E., Wachsmuth, G.: A theory of name resolution. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 205\u2013231. Springer, Heidelberg (2015)"},{"key":"47_CR69","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/s10009-015-0374-1","volume":"18","author":"A Osaiweran","year":"2016","unstructured":"Osaiweran, A., Schuts, M., Hooman, J., Groote, J., van Rijnsoever, B.: Evaluating the effect a lightweight formal technique in industry. Int. J. Softw. Tools Technol. Transf. 18, 93\u2013108 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"47_CR70","doi-asserted-by":"crossref","unstructured":"Ostrand, T.J., Weyuker, E.J.: The distribution of faults in a large industrial software system. In: 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2002, pp. 55\u201364. ACM (2002)","DOI":"10.1145\/566172.566181"},{"key":"47_CR71","doi-asserted-by":"crossref","unstructured":"Ostrand, T.J., Weyuker, E.J., Bell, R.M.: Where the bugs are. In: 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, pp. 86\u201396. ACM (2004)","DOI":"10.1145\/1007512.1007524"},{"key":"47_CR72","doi-asserted-by":"crossref","unstructured":"Patikirikorala, T., Colman, A., Han, J., Wang, L.: A systematic survey on the design of self-adaptive software systems using control engineering approaches. In: Proceedings of the 7th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, pp. 33\u201342. IEEE Press (2012)","DOI":"10.1109\/SEAMS.2012.6224389"},{"issue":"5","key":"47_CR73","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1109\/TSE.2014.2312918","volume":"40","author":"Y Pei","year":"2014","unstructured":"Pei, Y., Furia, C.A., Nordio, M., Wei, Y., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. IEEE Trans. Softw. Eng. 40(5), 427\u2013449 (2014)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"47_CR74","unstructured":"Perez, A., Abreu, R., van Deursen, A.: A unifying metric for test adequacy and diagnosability. In: Automated Software Engineering (2016, Submitted)"},{"key":"47_CR75","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/j.jss.2016.02.035","volume":"117","author":"G Procaccianti","year":"2016","unstructured":"Procaccianti, G., Fern\u00e1ndez, H., Lago, P.: Empirical evaluation of two best practices for energy-efficient software development. J. Syst. Softw. 117, 185\u2013198 (2016)","journal-title":"J. Syst. Softw."},{"key":"47_CR76","doi-asserted-by":"crossref","unstructured":"Procaccianti, G., Lago, P., Lewis, G.A.: A catalogue of green architectural tactics for the cloud. In: Maintenance and Evolution of Service-Oriented and Cloud-Based Systems (MESOCA 2014), pp. 29\u201336. IEEE (2014)","DOI":"10.1109\/MESOCA.2014.12"},{"key":"47_CR77","doi-asserted-by":"crossref","unstructured":"Procaccianti, G., Lago, P., Vetro, A., Fern\u00e1ndez, D.M., Wieringa, R.: The green lab: experimentation in software energy efficiency. In: Proceedings of the 37th International Conference on Software Engineering-Volume 2 (2015)","DOI":"10.1109\/ICSE.2015.297"},{"key":"47_CR78","volume-title":"Software Systems Architecture: Working with Stakeholders using Viewpoints and Perspectives","author":"N Rozanski","year":"2012","unstructured":"Rozanski, N., Woods, E.: Software Systems Architecture: Working with Stakeholders using Viewpoints and Perspectives. Addison-Wesley, Boston (2012)"},{"key":"47_CR79","doi-asserted-by":"crossref","unstructured":"Salvesen, K., Galeotti, J.P., Gross, F., Fraser, G., Zeller, A.: Using dynamic symbolic execution to generate inputs in search-based GUI testing. In: Gay, G., Antoniol, G. (eds.) 8th IEEE\/ACM International Workshop on Search-Based Software Testing, SBST 2015, pp. 32\u201335. IEEE (2015)","DOI":"10.1109\/SBST.2015.15"},{"issue":"1","key":"47_CR80","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., St\u00e5lmarck, G.: A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Formal Methods Syst. Des. 16(1), 23\u201358 (2000)","journal-title":"Formal Methods Syst. Des."},{"key":"47_CR81","unstructured":"Slowinska, A., Stancescu, T., Bos, H.: Body armor for binaries: preventing buffer overflows without recompilation. In: Proceedings of USENIX Annual Technical Conference, Boston, MA, June 2012"},{"key":"47_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-78917-8_1","volume-title":"Formal Methods and Testing","author":"J Tretmans","year":"2008","unstructured":"Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) FORTEST. LNCS, vol. 4949, pp. 1\u201338. Springer, Heidelberg (2008)"},{"key":"47_CR83","doi-asserted-by":"crossref","unstructured":"van der Veen, V., Goktas, E., Contag, M., Pawlowski, A., Chen, X., Rawat, S., Bos, H., Holz, T., Athanasopoulos, E., Giuffrida, C.: A tough call: mitigating advanced code-reuse attacks at the binary level. In: Proceedings of the 37th IEEE Symposium on Security and Privacy (Oakland), San Jose, CA, USA, IEEE, May 2016","DOI":"10.1109\/SP.2016.60"},{"issue":"2","key":"47_CR84","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1002\/(SICI)1096-908X(199803\/04)10:2<75::AID-SMR168>3.0.CO;2-5","volume":"10","author":"A Deursen van","year":"1998","unstructured":"van Deursen, A., Klint, P.: Little languages: little maintenance? J. Softw. Maintenance 10(2), 75\u201392 (1998)","journal-title":"J. Softw. Maintenance"},{"issue":"5\/6","key":"47_CR85","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1016\/S0747-7171(06)80004-0","volume":"15","author":"A Deursen van","year":"1993","unstructured":"van Deursen, A., Klint, P., Tip, F.: Origin tracking. J. Symbolic Comput. 15(5\/6), 523\u2013545 (1993)","journal-title":"J. Symbolic Comput."},{"issue":"6","key":"47_CR86","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/352029.352035","volume":"35","author":"A Deursen van","year":"2000","unstructured":"van Deursen, A., Klint, P., Visser, J.: Domain-specific languages: an annotated bibliography. SIGPLAN Not. 35(6), 26\u201336 (2000)","journal-title":"SIGPLAN Not."},{"key":"47_CR87","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1109\/MS.2013.81","volume":"30","author":"M Genuchten van","year":"2013","unstructured":"van Genuchten, M., Hatton, L.: Metrics with impact. IEEE Softw. 30, 99\u2013101 (2013)","journal-title":"IEEE Softw."},{"key":"47_CR88","first-page":"29","volume":"33","author":"M Genuchten van","year":"2016","unstructured":"van Genuchten, M., Hatton, L.: When software crosses a line. IEEE Softw. 33, 29\u201331 (2016)","journal-title":"IEEE Softw."},{"key":"47_CR89","doi-asserted-by":"crossref","unstructured":"van Lamsweerde, A.: Requirements engineering in the year 00: a research perspective. In: Proceedings of the IEEE International Symposium on Requirements Engineering, pp. 5\u201319 (2000)","DOI":"10.1145\/337180.337184"},{"key":"47_CR90","volume-title":"Requirements Engineering: From System Goals to UML Models to Software Specifications","author":"A Lamsweerde van","year":"2009","unstructured":"van Lamsweerde, A.: Requirements Engineering: From System Goals to UML Models to Software Specifications. Wiley, Hoboken (2009)"},{"key":"47_CR91","volume-title":"UNIX Filesystems: Evolution, Design, and Implementation","author":"W Hagen von","year":"2002","unstructured":"von Hagen, W., Filesystems, U.: UNIX Filesystems: Evolution, Design, and Implementation. SAMS, Indianapolis (2002)"},{"key":"47_CR92","doi-asserted-by":"crossref","unstructured":"Weyns, D., Iftikhar, M.U., de la Iglesia, D.G., Ahmad, T.: A survey of formal methods in self-adaptive systems. In: Proceedings of the IC on Computer Science and Software Engineering, pp. 67\u201379. ACM (2012)","DOI":"10.1145\/2347583.2347592"},{"key":"47_CR93","volume-title":"Exploratory Software Testing: Tips, Tricks, Tours, and Techniques to Guide Test Design","author":"JA Whittaker","year":"2009","unstructured":"Whittaker, J.A.: Exploratory Software Testing: Tips, Tricks, Tours, and Techniques to Guide Test Design. Addison-Wesley, Boston (2009)"},{"key":"47_CR94","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1038\/nature.2016.19835","volume":"533","author":"A Witze","year":"2016","unstructured":"Witze, A.: Software error doomed Japanese Hitomi spacecraft. Nature 533, 18\u201319 (2016)","journal-title":"Nature"},{"key":"47_CR95","doi-asserted-by":"crossref","unstructured":"Wurster, G., van Oorschot, P.C., Somayaji, A.: A generic attack on checksumming-based software tamper resistance. In: 2005 IEEE Symposium on Security and Privacy (S&P 2005), pp. 127\u2013138. IEEE Computer Society (2005)","DOI":"10.1109\/SP.2005.2"},{"key":"47_CR96","doi-asserted-by":"crossref","DOI":"10.1007\/978-4-431-54565-1","volume-title":"Software Reliability Modeling","author":"S Yamada","year":"2014","unstructured":"Yamada, S.: Software Reliability Modeling. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T23:10:18Z","timestamp":1749597018000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":96,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}