{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T20:09:38Z","timestamp":1648670978928},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2014,8,5]],"date-time":"2014-08-05T00:00:00Z","timestamp":1407196800000},"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-0338-x","type":"journal-article","created":{"date-parts":[[2014,8,4]],"date-time":"2014-08-04T21:48:36Z","timestamp":1407188916000},"page":"493-505","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges"],"prefix":"10.1007","volume":"16","author":[{"given":"Markus","family":"Schordan","sequence":"first","affiliation":[]},{"given":"Adrian","family":"Prantl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,8,5]]},"reference":[{"issue":"2","key":"338_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\u2013condition\u2013action systems for reconfigurable logic control. IEEE Trans. Autom. Sci. Eng. 4(2), 167\u2013181 (2007)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"1","key":"338_CR2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"Alessandro Armando","year":"2009","unstructured":"Armando, Alessandro, Mantovani, Jacopo, Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers. Int. J. Softw. Tools Technol. Transf. 11(1), 69\u201383 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"3","key":"338_CR3","doi-asserted-by":"crossref","first-page":"651","DOI":"10.1093\/logcom\/exn075","volume":"20","author":"Andreas Bauer","year":"2010","unstructured":"Bauer, Andreas, Leucker, Martin, Schallhart, Christian: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3), 651\u2013674 (2010)","journal-title":"J. Logic Comput."},{"key":"338_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T.A., Th\u00e9oduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Proc. CAV, LNCS 4590, pp. 504\u2013518. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_51"},{"issue":"5","key":"338_CR5","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"Dirk Beyer","year":"2007","unstructured":"Beyer, Dirk, Henzinger, Thomas A., Jhala, Ranjit, Majumdar, Rupak: The software model checker Blast: applications to software engineering. Int. J. Softw. Tools Technol. Transf. 9(5), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"338_CR6","doi-asserted-by":"crossref","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification. Applications to event\u2013condition\u2013action systems. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0334-1 (2014)","DOI":"10.1007\/s10009-014-0334-1"},{"key":"338_CR7","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ 10 20 states and beyond. In: Fifth Annual IEEE Symposium on Logic in Computer Science, 1990. LICS \u201990, Proceedings, pp. 428\u2013439, Jun 1990"},{"issue":"9","key":"338_CR8","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1145\/357766.351266","volume":"35","author":"K Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of Haskell programs. SIGPLAN Not. 35(9), 268\u2013279 (2000)","journal-title":"SIGPLAN Not."},{"issue":"1","key":"338_CR9","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Form. Methods Syst. Des."},{"key":"338_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M.: 25 years of model checking. In: The Birth of Model Checking, pp. 1\u201326. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-69850-0_1"},{"key":"338_CR11","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of the 2009 IEEE\/ACM International Conference on Automated Software Engineering, ASE \u201909, pp. 137\u2013148. IEEE Computer Society, Washington, DC (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"338_CR12","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A.: LTL translation improvements in spot. In: Proceedings of the Fifth International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS\u201911, pp. 72\u201383. British Computer Society, Swinton (2011)","DOI":"10.14236\/ewic\/VECOS2011.8"},{"key":"338_CR13","doi-asserted-by":"crossref","unstructured":"Alexandre, D.L.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput.-Based Syst. 5(1\/2):31\u201354 (2014)","DOI":"10.1504\/IJCCBS.2014.059594"},{"issue":"5","key":"338_CR14","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"Gerard J Holzmann","year":"1997","unstructured":"Holzmann, Gerard J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"338_CR15","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: Parallelizing the spin model checker. In: Proceedings of the 19th International Conference on Model Checking Software, SPIN\u201912, pp. 155\u2013171. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31759-0_12"},{"key":"338_CR16","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Bosnacki, D.: Multi-core model checking with spin. In: Parallel and Distributed Processing Symposium, 2007. IPDPS 2007. IEEE International, pp. 1\u20138, March (2007)","DOI":"10.1109\/IPDPS.2007.370410"},{"key":"338_CR17","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event\u2013condition\u2013action systems. In: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change\u20145th International Symposium, ISoLA 2012, LNCS 4590, pp. 608\u2013614. Springer, Berlin (2007)","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"338_CR18","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems. In: The RERS Challenges 2012 and 2013. Software Tools for Technology Transfer. doi: 10.1007\/s10009-014-0337-y (2014)","DOI":"10.1007\/s10009-014-0337-y"},{"key":"338_CR19","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009)","DOI":"10.1145\/1592434.1592438"},{"key":"338_CR20","doi-asserted-by":"crossref","unstructured":"Lerda, F., Sinha, N., Theobald, M.: Symbolic model checking of software. Electron. Notes Theoret. Comput. Sci., 89(3), 480\u2013498 (2003). SoftMC 2003, Workshop on Software Model Checking (Satellite Workshop of CAV \u201903)","DOI":"10.1016\/S1571-0661(05)80008-8"},{"key":"338_CR21","doi-asserted-by":"crossref","unstructured":"McCarthy, D., Dayal, U.: The architecture of an active database management system. In: Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, SIGMOD \u201989, pp. 215\u2013224. ACM, New York (1989)","DOI":"10.1145\/67544.66946"},{"key":"338_CR22","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0336-z (2014)","DOI":"10.1007\/s10009-014-0336-z"}],"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-0338-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0338-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0338-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,22]],"date-time":"2020-08-22T22:23:41Z","timestamp":1598135021000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0338-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,5]]},"references-count":22,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["338"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0338-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,5]]}}}