{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:16:57Z","timestamp":1759033017777},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2014,8,26]],"date-time":"2014-08-26T00:00:00Z","timestamp":1409011200000},"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-0339-9","type":"journal-article","created":{"date-parts":[[2014,8,25]],"date-time":"2014-08-25T07:47:14Z","timestamp":1408952834000},"page":"543-558","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Tailored generation of concurrent benchmarks"],"prefix":"10.1007","volume":"16","author":[{"given":"Bernhard","family":"Steffen","sequence":"first","affiliation":[]},{"given":"Falk","family":"Howar","sequence":"additional","affiliation":[]},{"given":"Malte","family":"Isberner","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Naujokat","sequence":"additional","affiliation":[]},{"given":"Tiziana","family":"Margaria","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,8,26]]},"reference":[{"issue":"3","key":"339_CR1","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507\u2013535 (1995)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"339_CR2","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"339_CR3","doi-asserted-by":"crossref","unstructured":"Briggs, P., Cooper, K.D.: Effective partial redundancy elimination. In: Proceedings of the ACM SIGPLAN\u201993 Conference on Programming Language Design and Implementation (PLDI\u201994), pp. 159\u2013170 (1994)","DOI":"10.1145\/773473.178257"},{"key":"339_CR4","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. Lecture Notes in Computer Science, vol. 1256, pp. 419\u2013429. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63165-8_198"},{"key":"339_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"339_CR6","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1016\/0167-6423(83)90013-8","volume":"2","author":"T Elrad","year":"1982","unstructured":"Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2, 155\u2013173 (1982)","journal-title":"Sci. Comput. Program."},{"key":"339_CR7","doi-asserted-by":"crossref","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: G\u00e9rard, B., Hubert, C., Alain, F. (eds.) Proceedings of CAV\u201901. LNCS, vol 2102, pp. 53\u201365, Paris, France. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_6"},{"key":"339_CR8","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 FORTE\u201902, pp. 308\u2013326, London, UK. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36135-9_20"},{"key":"339_CR9","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc., Upper Saddle River (1985)"},{"key":"339_CR10","series-title":"The SPIN Model Checker\u2014Primer and Reference Manual","volume-title":"Holzmann","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: Holzmann. The SPIN Model Checker\u2014Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"339_CR11","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-action systems. In: Margaria, T., Steffen, B. (eds.) Proceedings of ISOLA\u201912. LNCS, vol. 7609, pp. 608\u2013614. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"339_CR12","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":"339_CR13","first-page":"71","volume":"1","author":"J Knoop","year":"1993","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy strength reduction. J. Program. Lang. 1, 71\u201391 (1993)","journal-title":"J. Program. Lang."},{"key":"339_CR14","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. In: Pierre, L., Kropf, T. (eds.) Correct Hardware Design and Verification Methods. LNCS, vol. 1703, pp. 82\u201398. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48153-2_8"},{"key":"339_CR15","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":"339_CR16","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice-Hall Inc, Upper Saddle River (1989)"},{"issue":"2","key":"339_CR17","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":"339_CR18","unstructured":"Naujokat, S., Lybecait, M., Steffen, B., Kopetzki, D., Margaria, T.: Full generation of domain-specific graphical modeling tools: a meta $$^2$$ 2 modeling approach (2014 under submission)"},{"key":"339_CR19","doi-asserted-by":"crossref","unstructured":"Naujokat, S., Traonouez, L-M., Isberner, M., Steffen, B., Axel, L.: Domain-specific code generator modeling: a case study for multi-faceted concurrent systems. In: Proceedings of the 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2014) (2014 to appear)","DOI":"10.1007\/978-3-662-45234-9_33"},{"key":"339_CR20","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. I & II. Elsevier, Amsterdam (2001)"},{"key":"339_CR21","doi-asserted-by":"crossref","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages. ACM Press, New York (1988)","DOI":"10.1145\/73560.73562"},{"issue":"4","key":"339_CR22","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1145\/1178625.1178628","volume":"15","author":"G Snelting","year":"2006","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)","journal-title":"ACM Trans. Softw. Eng. Methodol (TOSEM)"},{"key":"339_CR23","series-title":"Lecture Notes in Computer Science, vol. 372","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1007\/BFb0035794","volume-title":"Automata, Languages and Programming","author":"B Steffen","year":"1989","unstructured":"Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R. (eds.) Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 372, pp. 723\u2013732. Springer, Berlin (1989)"},{"key":"339_CR24","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 (1997)","DOI":"10.1007\/BFb0023444"},{"key":"339_CR25","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. Lecture Notes in Computer Science, vol. 962, pp. 72\u201387. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60218-6_6"},{"key":"339_CR26","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). LNCS, vol. 7976, pp. 341\u2013357. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39176-7_21"},{"key":"339_CR27","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"},{"key":"339_CR28","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). LNCS, vol. 379, pages 481\u2013491. Springer, Berlin (1989)","DOI":"10.1007\/3-540-51486-4_94"},{"key":"339_CR29","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. LNCS, vol. 4383, pp. 92\u2013108. Springer, Berlin (2006)","DOI":"10.1007\/978-3-540-70889-6_7"}],"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-0339-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0339-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0339-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,14]],"date-time":"2019-08-14T07:57:37Z","timestamp":1565769457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0339-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8,26]]},"references-count":29,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["339"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0339-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,8,26]]}}}