{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:27Z","timestamp":1776305247357,"version":"3.50.1"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2014,8,9]],"date-time":"2014-08-09T00:00:00Z","timestamp":1407542400000},"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-0336-z","type":"journal-article","created":{"date-parts":[[2014,8,8]],"date-time":"2014-08-08T10:40:19Z","timestamp":1407494419000},"page":"465-479","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Property-driven benchmark generation: synthesizing programs of realistic structure"],"prefix":"10.1007","volume":"16","author":[{"given":"Bernhard","family":"Steffen","sequence":"first","affiliation":[]},{"given":"Malte","family":"Isberner","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Naujokat","sequence":"additional","affiliation":[]},{"given":"Tiziana","family":"Margaria","sequence":"additional","affiliation":[]},{"given":"Maren","family":"Geske","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,8,9]]},"reference":[{"key":"336_CR1","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)"},{"key":"336_CR2","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer, New York, NY, USA (1991)","DOI":"10.1007\/978-1-4757-4376-0"},{"key":"336_CR3","doi-asserted-by":"crossref","unstructured":"Bauer, O., Geske, M., Isberner, M.: Analyzing program behavior through active automata learning. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0333-2 (2014)","DOI":"10.1007\/s10009-014-0333-2"},{"key":"336_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification. Applications to event-condition\u2013action systems. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0334-1 (2014)","DOI":"10.1007\/s10009-014-0334-1"},{"key":"336_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D. Competition on software verification\u2014(SV-COMP). In: Proceedings of of 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), vol. 7214 of LNCS, pp. 504\u2013524. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_38"},{"key":"336_CR6","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (editors): Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, NL (2009)"},{"key":"336_CR7","doi-asserted-by":"crossref","unstructured":"Blom, S.C.C., van de Pol, J.C., Weber, M.: Ltsmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. Edinburgh, vol. 6174 of Lecture Notes in Computer Science, pp. 354\u2013359. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"336_CR8","doi-asserted-by":"crossref","unstructured":"Briggs, P., Cooper, K.D.: Effective partial redundancy elimination. In: Proceedings of ACM SIGPLAN Conf. Prog. Lang. Design and Impl. (PLDI\u201994), pp. 159\u2013170 (1994)","DOI":"10.1145\/773473.178257"},{"key":"336_CR9","doi-asserted-by":"crossref","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal Mu-Calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Automata. Languages and Programming, vol. 1256 of Lecture Notes in Computer Science, pp. 419\u2013429. Springer, Berlin Heidelberg (1997)","DOI":"10.1007\/3-540-63165-8_198"},{"key":"336_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA, USA (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"336_CR11","doi-asserted-by":"crossref","unstructured":"Combe, D., de la Higuera, C., Zulu, J.-C.J.: An interactive learning competition. In: Revised Selected Papers of 8th International Workshop on Finite-State Methods and Natural Language Processing (FSMNLP 2009), vol. 6062, pp. 139\u2013146. Springer (2010)","DOI":"10.1007\/978-3-642-14684-8_15"},{"key":"336_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1080\/00207168808803702","volume":"27","author":"DM Dhamdhere","year":"1989","unstructured":"Dhamdhere, D.M.: A new algorithm for composite hoisting and strength reduction optimisation (+ Corrigendum). Int. J. Comp. Math. 27, 1\u201314 (1989)","journal-title":"Int. J. Comp. Math."},{"key":"336_CR13","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 the 1999 Int. Conf. on Software Engineering, pp. 411\u2013420. IEEE (1999)","DOI":"10.1145\/302405.302672"},{"key":"336_CR14","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Proceedongs of Symposium on Applied Mathematics, vol. 19 of Mathematical aspects of computer science, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"336_CR15","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In: Berry, G., Comon, H., Finkel, A., (eds) Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u201901), vol. 2102 of Lecture Notes in Computer Science, pp. 53\u201365, Paris, France. Springer (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"336_CR16","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to B\u00fcchi Automata. In: Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, FORTE \u201902, pp. 308\u2013326, London, UK. Springer (2002)","DOI":"10.1007\/3-540-36135-9_20"},{"key":"336_CR17","doi-asserted-by":"crossref","unstructured":"Hayes-Roth, F.: Rule-based systems. Commun. ACM 28(9), 921\u2013932 (1985)","DOI":"10.1145\/4284.4286"},{"issue":"10","key":"336_CR18","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"336_CR19","unstructured":"Holzmann, G.J.: The SPIN Model Checker\u2014Primer and Reference Manual. Addison-Wesley, Boston, MA, USA (2004)"},{"key":"336_CR20","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., Pasareanu, C.S.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0337-y (2014)","DOI":"10.1007\/s10009-014-0337-y"},{"key":"336_CR21","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The RERS grey-box challenge 2012: analysis of event-condition\u2013action systems. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, vol. 7609 of Lecture Notes in Computer Science, pp. 608\u2013614. Springer, Berlin Heidelberg (2012)","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"336_CR22","doi-asserted-by":"crossref","unstructured":"Huth, M.: Model checking modal transition systems using kripke structures. In: Revised Papers from the Third International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI \u201902, pp. 302\u2013316, London. Springer (2002)","DOI":"10.1007\/3-540-47813-2_21"},{"key":"336_CR23","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: Timed I\/O Automata: a mathematical framework for modeling and analyzing real-time systems. In: Proceedings of the 24th IEEE Real-Time Systems Symposium (RTSS 2003), pp. 166\u2013177. IEEE Computer Society (2003)","DOI":"10.1109\/REAL.2003.1253264"},{"key":"336_CR24","doi-asserted-by":"crossref","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M.A., Rustan, J.K., Leino, M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Wei\u00df, B.: The 1st verified software competition: experience report. In: Proceedings of the 17th Int. Symposium on Formal Methods (FM 2011), vol. 6664 of LNCS, pp. 154\u2013168 (2011)","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"336_CR25","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Expansion-based removal of semantic partial redundancies. In: Compiler Construction, 8th International Conference, CC\u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, 22\u201328 March, 1999, Proceedings, vol. 1575 of LNCS, pp. 91\u2013106. Springer (1999)","DOI":"10.1007\/978-3-540-49051-7_7"},{"key":"336_CR26","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy code motion. In: Proceedings of the ACM SIGPLAN\u201992 Conference on Programming Language Design and Implementation (PLDI), pp. 224\u2013234. ACM (1992)","DOI":"10.1145\/143103.143136"},{"key":"336_CR27","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy strength reduction. J. Program. Lang. 1, 71\u201391 (1993)"},{"key":"336_CR28","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Optimal code motion: theory and practice. ACM Trans. Program. Lang. Syst. 16(4), 1117\u20131155 (1994)"},{"key":"336_CR29","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Partial dead code elimination. In: Proceedings of the ACM SIGPLAN\u201994 Conference on Programming Language Design and Implementation (PLDI), pp. 147\u2013158. ACM (1994)","DOI":"10.1145\/773473.178256"},{"key":"336_CR30","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B. The power of assignment motion. In: Proceedings of the ACM SIGPLAN\u201995 Conference on Programming Language Design and Implementation (PLDI). ACM (1995)","DOI":"10.1145\/207110.207150"},{"key":"336_CR31","unstructured":"Lamport, L.: What good is temporal logic? Inf. Process. 83, 657\u2013668 (1983)"},{"key":"336_CR32","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, pp. 232\u2013246 (1989)","DOI":"10.1007\/3-540-52148-8_19"},{"key":"336_CR33","doi-asserted-by":"crossref","unstructured":"Margaria, T., Steffen, B.: Continuous model-driven engineering. IEEE Computer 42(10), 106\u2013109 (2009)","DOI":"10.1109\/MC.2009.315"},{"key":"336_CR34","doi-asserted-by":"crossref","unstructured":"McCarthy, D.R., Dayal, U.: The architecture of an active data base management system. In: Proceedings of the 1989 ACM SIGMOD International Conference on Management of Data, pp. 215\u2013224. ACM Press (1989)","DOI":"10.1145\/67544.66946"},{"key":"336_CR35","unstructured":"Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Tech. J. 34(5), 1045\u20131079 (1955)"},{"key":"336_CR36","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice-Hall Inc, Upper Saddle River (1989)"},{"issue":"2","key":"336_CR37","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1145\/359060.359069","volume":"22","author":"E Morel","year":"1979","unstructured":"Morel, E., Renvoise, C.: Global optimization by suppression of partial redundancies. Commun. ACM 22(2), 96\u2013103 (1979)","journal-title":"Commun. ACM"},{"key":"336_CR38","doi-asserted-by":"crossref","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the 2012 RERS greybox challenge. Soft. Tools Technol. Transf. doi: 10.1007\/s10009-014-0335-0 (2014)","DOI":"10.1007\/s10009-014-0335-0"},{"key":"336_CR39","unstructured":"Robinson, A., Voronkov, A. (eds): Handbook of Automated Reasoning, vol. I and II. Elsevier, Amsterdam, NL (2001)"},{"key":"336_CR40","doi-asserted-by":"crossref","unstructured":"Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: Global value numbers and redundant computations. In: Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages. ACM Press (1988)","DOI":"10.1145\/73560.73562"},{"key":"336_CR41","doi-asserted-by":"crossref","unstructured":"R\u00fcthing, O., Knoop, J., Steffen, B.: Sparse code motion. In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), pp. 170\u2013183. ACM (2000)","DOI":"10.1145\/325694.325715"},{"key":"336_CR42","unstructured":"SCCE: Service Centered Continuous Engineering. http:\/\/scce.info . Accessed 26 Feb 2014"},{"key":"336_CR43","doi-asserted-by":"crossref","unstructured":"Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition\u2013action systems in the RERS 2012 and 2013 challenges. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0338-x (2014)","DOI":"10.1007\/s10009-014-0338-x"},{"key":"336_CR44","unstructured":"Snelting, G., Robschnik, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. ACM Trans. Softw. Eng. Methodol. (TOSEM) 15(4), 410\u2013457 (2006)"},{"key":"336_CR45","doi-asserted-by":"crossref","unstructured":"Steffen, B., Cla\u00dfen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds) CONCUR \u201995: Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pp. 72\u201387. Springer, Berlin, Heidelberg (1995)","DOI":"10.1007\/3-540-60218-6_6"},{"key":"336_CR46","doi-asserted-by":"crossref","unstructured":"Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0339-9 (2014)","DOI":"10.1007\/s10009-014-0339-9"},{"key":"336_CR47","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation. In: International SPIN Symposium on Model Checking of Software (SPIN2013), vol. 7976 of LNCS, pp. 341\u2013357. Springer (2013)","DOI":"10.1007\/978-3-642-39176-7_21"},{"key":"336_CR48","doi-asserted-by":"crossref","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: Efficient code motion and an adaption to strength reduction. In: Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT\u201991). Volume 2: Advances in Distributed Computing (ADC) and Colloquium on Combining Paradigms for Software Developmemnt (CCPSD), vol. 494 of LNCS, pp. 394\u2013415. Springer (1991)","DOI":"10.1007\/3540539816_78"},{"key":"336_CR49","doi-asserted-by":"crossref","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: The value flow graph: a program representation for optimal program transformations. In: Jones, N.D. (ed.) 3rd European Symposium on Programming (ESOP\u201990). Lecture Notes in Computer Science, vol. 432, pp. 389\u2013405. Springer, Berlin Heidelberg (1990)","DOI":"10.1007\/3-540-52592-0_76"},{"key":"336_CR50","doi-asserted-by":"crossref","unstructured":"Steffen, B., Knoop, J.: Finite constants: characterizations of a new decidable set of constants. In: Kreczmar, A., Mirkowska, G. (eds) Mathematical Foundations of Computer Science (MFCS\u201989), vol. 379 of LNCS, pp. 481\u2013491. Springer (1989)","DOI":"10.1007\/3-540-51486-4_94"},{"key":"336_CR51","doi-asserted-by":"crossref","unstructured":"Steffen, B., Margaria, T., Nagel, R., J\u00f6rges, S., Kubczak, C.: Model-driven development with the jABC. In: Bin, E., Ziv, A., Ur, S. (eds) Haifa Verification Conference, vol. 4383 of Lecture Notes in Computer Science, pp. 92\u2013108. Springer (2006)","DOI":"10.1007\/978-3-540-70889-6_7"},{"key":"336_CR52","doi-asserted-by":"crossref","unstructured":"Steffen, B., Narayan, P.: Full life-cycle support for end-to-end processes. IEEE Computer 40(11), 64\u201373 (2007)","DOI":"10.1109\/MC.2007.386"},{"key":"336_CR53","doi-asserted-by":"crossref","unstructured":"Steffen, B., R\u00fcthing, O.: Quality engineering: leveraging heterogeneous information\u2014(Invited Talk). In: Proceedings of the 12th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI 2011), LNCS, pp. 23\u201337 (2011)","DOI":"10.1007\/978-3-642-18275-4_4"},{"key":"336_CR54","doi-asserted-by":"crossref","unstructured":"Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R. (eds.) Automata. Languages and Programming, vol. 372 of Lecture Notes in Computer Science, pp. 723\u2013732. Springer, Berlin Heidelberg (1989)","DOI":"10.1007\/BFb0035794"},{"key":"336_CR55","doi-asserted-by":"crossref","unstructured":"Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) Third International Symposium on Static Analysis (SAS \u201996). Lecture Notes in Computer Science, vol. 1145, pp. 22\u201341. Springer, Berlin, Heidelberg (1996)","DOI":"10.1007\/3-540-61739-6_31"},{"key":"336_CR56","doi-asserted-by":"crossref","unstructured":"Steffen, B.: Unifying models. In: Reischuk, R., Morvan, M. (eds.) STACS 97. Lecture Notes in Computer Science, vol. 1200, pp. 1\u201320. Springer, Berlin, Heidelberg (1997)","DOI":"10.1007\/BFb0023444"},{"key":"336_CR57","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. Softw. Tools Technol. Transf. doi: 10.1007\/s10009-014-0324-3 (2014)","DOI":"10.1007\/s10009-014-0324-3"},{"key":"336_CR58","doi-asserted-by":"crossref","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Proceedings of the 32nd ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI 2011) (2011)","DOI":"10.1145\/1993498.1993532"}],"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-0336-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0336-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0336-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T03:24:50Z","timestamp":1746329090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0336-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,9]]},"references-count":58,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["336"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0336-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,9]]}}}