{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:07:43Z","timestamp":1767773263911,"version":"3.40.4"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2014,8,3]],"date-time":"2014-08-03T00:00:00Z","timestamp":1407024000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1007\/s10009-014-0337-y","type":"journal-article","created":{"date-parts":[[2014,8,2]],"date-time":"2014-08-02T18:26:06Z","timestamp":1407003966000},"page":"457-464","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":38,"title":["Rigorous examination of reactive systems"],"prefix":"10.1007","volume":"16","author":[{"given":"Falk","family":"Howar","sequence":"first","affiliation":[]},{"given":"Malte","family":"Isberner","sequence":"additional","affiliation":[]},{"given":"Maik","family":"Merten","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]},{"given":"Dirk","family":"Beyer","sequence":"additional","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,8,3]]},"reference":[{"issue":"2","key":"337_CR1","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1109\/TASE.2006.880857","volume":"4","author":"EE Almeida","year":"2007","unstructured":"Almeida, E.E., Luntz, J.E., Tilbury, D.M.: Event-condition\u2013action systems for reconfigurable logic control. IEEE Trans. Autom. Sci. Eng. 4(2), 167\u2013181 (2007)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"2","key":"337_CR2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"337_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, O., Geske, M., Isberner, M.: Analyzing program behavior through active automata learning. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0333-2 (2014)","DOI":"10.1007\/s10009-014-0333-2"},{"issue":"1","key":"337_CR4","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/MIC.2003.1167338","volume":"7","author":"B Benatallah","year":"2003","unstructured":"Benatallah, B., Sheng, Q.Z., Dumas, M.: The Self\u2013Serv environment for web-services composition. Internet Comput. IEEE 7(1), 40\u201348 (2003)","journal-title":"Internet Comput. IEEE"},{"key":"337_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Competition on software verification (SV-COMP). In: Proceedings of TACAS, LNCS 7214, pp. 504\u2013524. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_38"},{"key":"337_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Second competition on software verification. In: Proceedings od TACAS, LNCS 7795, pp. 594\u2013609. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_43"},{"key":"337_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Status report on software verification. In: Proceedings of TACAS, LNCS 8413, pp. 373\u2013388. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"337_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T. A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of PLDI, pp. 300\u2013309. ACM (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"337_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software model checking with CPAchecker. In: Proceedings of MEMICS, LNCS 7721, pp. 1\u201311. Springer (2013)","DOI":"10.1007\/978-3-642-36046-6_1"},{"key":"337_CR10","doi-asserted-by":"crossref","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification: applications to event-condition\u2013action systems. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0334-1 (2014)","DOI":"10.1007\/s10009-014-0334-1"},{"key":"337_CR11","doi-asserted-by":"crossref","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Proceedings of FSTTCS, LNCS 1026, pp. 499\u2013513. Springer (1995)","DOI":"10.1007\/3-540-60692-0_70"},{"key":"337_CR12","doi-asserted-by":"crossref","unstructured":"Blom, S.C.C., van de Pol, J.C., Weber, L.T., Smin, M.: Distributed and symbolic reachability. In: Proceedings of CAV, LNCS 6174, pp. 354\u2013359. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"337_CR13","doi-asserted-by":"crossref","unstructured":"Boyer, J., Mili, H.: IBM WebSphere ILOG JRules. In: Agile Business Rule Development, pp. 215\u2013242. Springer (2011)","DOI":"10.1007\/978-3-642-19041-4_8"},{"key":"337_CR14","unstructured":"Browne, P.: JBoss Drools Business Rules: Capture, Automate, and Reuse Your Business Processes in a Clear English Language that Your Computer Can Understand. Packt Publishing (2009)"},{"key":"337_CR15","doi-asserted-by":"crossref","unstructured":"Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (editors): Model-based testing of reactive systems. In: LNCS 3472. Springer (2005)","DOI":"10.1007\/b137241"},{"key":"337_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, USA (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"337_CR17","doi-asserted-by":"crossref","unstructured":"Cok, D. R., Griggio, A., Bruttomesso, R., Deters, M.: The 2012 SMT competition. In: Proceedings of SMT, pp. 131\u2013142 (2012)","DOI":"10.29007\/gj66"},{"key":"337_CR18","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Proceedings of CAV, LNCS 2725, pp. 420\u2013432. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"337_CR19","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Signoles, J., Baudin, P., Bonichon, R., Canet, G., Correnson, L., Monate, B., Prevosto, V., Puccetti, A.: Experience report: OCaml for an industrial-strength static analysis framework. In: Proceedings of ICFP, pp. 281\u2013286. ACM (2009)","DOI":"10.1145\/1596550.1596591"},{"key":"337_CR20","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of ICSE, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"issue":"2","key":"337_CR21","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1109\/32.908957","volume":"27","author":"MD Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw. Eng. 27(2), 99\u2013123 (2001)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"337_CR22","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Constraint-based invariant inference over predicate abstraction. In: Proceedings of VMCAI, pp. 120\u2013135 (2009)","DOI":"10.1007\/978-3-540-93900-9_13"},{"issue":"2","key":"337_CR23","first-page":"200","volume":"55","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Ro\u015fu, G.: Monitoring Java programs with Java PathExplorer. ENTCS 55(2), 200\u2013217 (2001)","journal-title":"ENTCS"},{"issue":"9","key":"337_CR24","doi-asserted-by":"crossref","first-page":"921","DOI":"10.1145\/4284.4286","volume":"28","author":"F Hayes-Roth","year":"1985","unstructured":"Hayes-Roth, F.: Rule-based systems. Commun. ACM 28(9), 921\u2013932 (1985)","journal-title":"Commun. ACM"},{"issue":"2","key":"337_CR25","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1002\/stvr.228","volume":"11","author":"GJ Holzmann","year":"2001","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verif. Reliab. 11(2), 65\u201379 (2001)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"337_CR26","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., and Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition-action systems. In: Proceedings of ISoLA, LNCS 7609, pp. 608\u2013614. Springer (2012)","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"337_CR27","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: On the organisation of program-verification competitions. In: Proceedings of COMPARE, CEUR Workshop Proceedings 873, pp. 50\u201359. CEUR-WS.org (2012)"},{"issue":"7","key":"337_CR28","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"issue":"5","key":"337_CR29","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Logic Alg. Progr. 78(5), 293\u2013303 (2009)","journal-title":"J. Logic Alg. Progr."},{"key":"337_CR30","doi-asserted-by":"crossref","unstructured":"Lidman, J., Quinlan, D.J., Liao, C., McKee, S.A.: ROSE:FTTransform\u2014a source-to-source translation framework for exascale fault-tolerance research. In: Proceedings of FTXS. IEEE (2012)","DOI":"10.1109\/DSNW.2012.6264672"},{"key":"337_CR31","doi-asserted-by":"crossref","unstructured":"McCarthy, D., Dayal, U.: The architecture of an active database management system. In: Proceedings of ICMD, pp. 215\u2013224. ACM (1989)","DOI":"10.1145\/66926.66946"},{"key":"337_CR32","doi-asserted-by":"crossref","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Context-bounded model checking of LTL properties for ANSI-C software. In: Proceedings of SEFM, LNCS 7041, pp. 302\u2013317. Springer (2011)","DOI":"10.1007\/978-3-642-24690-6_21"},{"key":"337_CR33","doi-asserted-by":"crossref","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the: RERS greybox challenge, p. 2014. J. Softw. Tools Technol. Transf. Int. doi: 10.1007\/s10009-014-0335-0 (2014)","DOI":"10.1007\/s10009-014-0335-0"},{"key":"337_CR34","doi-asserted-by":"crossref","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York, USA (1999)","DOI":"10.1007\/978-3-662-03811-6"},{"key":"337_CR35","doi-asserted-by":"crossref","unstructured":"Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0338-x (2014)","DOI":"10.1007\/s10009-014-0338-x"},{"key":"337_CR36","doi-asserted-by":"crossref","unstructured":"Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0339-9 (2014)","DOI":"10.1007\/s10009-014-0339-9"},{"key":"337_CR37","doi-asserted-by":"crossref","unstructured":"Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Proceedings of SFM, LNCS 6659, pp. 256\u2013296. Springer (2011)","DOI":"10.1007\/978-3-642-21455-4_8"},{"key":"337_CR38","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0336-z (2014)","DOI":"10.1007\/s10009-014-0336-z"},{"issue":"1","key":"337_CR39","first-page":"35","volume":"19","author":"G Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35\u201348 (2006)","journal-title":"AI Commun."},{"key":"337_CR40","doi-asserted-by":"crossref","unstructured":"van de Pol, J., Ruys, T. C., te Brinke, S.: Thoughtful brute force attack of the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0324-3 (2014)","DOI":"10.1007\/s10009-014-0324-3"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0337-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0337-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0337-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T01:50:37Z","timestamp":1746323437000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0337-y"}},"subtitle":["The RERS challenges 2012 and 2013"],"short-title":[],"issued":{"date-parts":[[2014,8,3]]},"references-count":40,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["337"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0337-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,8,3]]}}}