{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:45:14Z","timestamp":1725727514198},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642391750"},{"type":"electronic","value":"9783642391767"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39176-7_21","type":"book-chapter","created":{"date-parts":[[2013,5,30]],"date-time":"2013-05-30T08:58:44Z","timestamp":1369904324000},"page":"341-357","source":"Crossref","is-referenced-by-count":11,"title":["Property-Driven Benchmark Generation"],"prefix":"10.1007","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","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From States to Transitions: Improving Translation of LTL Formulae to B\u00fcchi Automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0023444","volume-title":"STACS 97","author":"B. Steffen","year":"1997","unstructured":"Steffen, B.: Unifying models. In: Reischuk, R., Morvan, M. (eds.) STACS 1997. LNCS, vol.\u00a01200, pp. 1\u201320. Springer, Heidelberg (1997)"},{"issue":"4","key":"21_CR5","doi-asserted-by":"publisher","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 Transactions on Software Engineering and Methodology (TOSEM)\u00a015(4), 410\u2013457 (2006)","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"21_CR6","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol.\u00a0I & II. Elsevier (2001)"},{"key":"21_CR7","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (February 2009)"},{"issue":"2","key":"21_CR8","doi-asserted-by":"publisher","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. Comm. ACM\u00a022(2), 96\u2013103 (1979)","journal-title":"Comm. ACM"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/3-540-51486-4_94","volume-title":"Mathematical Foundations of Computer Science 1989","author":"B. Steffen","year":"1989","unstructured":"Steffen, B., Knoop, J.: Finite Constants: Characterizations of a New Decidable Set of Constants. In: Kreczmar, A., Mirkowska, G. (eds.) MFCS 1989. LNCS, vol.\u00a0379, pp. 481\u2013491. Springer, Heidelberg (1989)"},{"key":"21_CR10","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 (1988)","DOI":"10.1145\/73560.73562"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy code motion. In: Proc. of the ACM SIGPLAN 1992 Conference on Programming Language Design and Implementation (PLDI), pp. 224\u2013234. ACM (1992)","DOI":"10.1145\/143103.143136"},{"key":"21_CR12","first-page":"71","volume":"1","author":"J. Knoop","year":"1993","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy Strength Reduction. Journal of Programming Languages\u00a01, 71\u201391 (1993)","journal-title":"Journal of Programming Languages"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Briggs, P., Cooper, K.D.: Effective partial redundancy elimination. In: Proc. ACM SIGPLAN Conf. Prog. Lang. Design and Impl. (PLDI 1994), pp. 159\u2013170 (1994)","DOI":"10.1145\/773473.178257"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/978-3-642-34026-0_45","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"F. Howar","year":"2012","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.) ISoLA 2012, Part I. LNCS, vol.\u00a07609, pp. 608\u2013614. Springer, Heidelberg (2012)"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. of the 1999 Int. Conf. on Software Engineering, pp. 411\u2013420. IEEE (1999)","DOI":"10.1145\/302405.302672"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-61739-6_31","volume-title":"Static Analysis","author":"B. Steffen","year":"1996","unstructured":"Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol.\u00a01145, pp. 22\u201341. Springer, Heidelberg (1996)"},{"issue":"9","key":"21_CR17","doi-asserted-by":"publisher","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\u00a028(9), 921\u2013932 (1985)","journal-title":"Commun. ACM"},{"key":"21_CR18","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\/66926.66946"},{"issue":"2","key":"21_CR19","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1109\/TASE.2006.880857","volume":"4","author":"E.E. Almeida","year":"2007","unstructured":"Almeida, E.E., Luntz, J.E., Tilbury, D.M.: Event-Condition-Action Systems for Reconfigurable Logic Control. IEEE T. Automation Science and Engineering\u00a04(2), 167\u2013181 (2007)","journal-title":"IEEE T. Automation Science and Engineering"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer (1991)","DOI":"10.1007\/978-1-4757-4376-0"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Partial Dead Code Elimination. In: Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI), pp. 147\u2013158. ACM (1994)","DOI":"10.1145\/773473.178256"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-540-49051-7_7","volume-title":"Compiler Construction","author":"J. Knoop","year":"1999","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Expansion-Based Removal of Semantic Partial Redundancies. In: J\u00e4hnichen, S. (ed.) CC 1999. LNCS, vol.\u00a01575, pp. 91\u2013107. Springer, Heidelberg (1999)"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 354\u2013359. Springer, Heidelberg (2010)"},{"issue":"5","key":"21_CR24","doi-asserted-by":"crossref","first-page":"1045","DOI":"10.1002\/j.1538-7305.1955.tb03788.x","volume":"34","author":"G.H. Mealy","year":"1955","unstructured":"Mealy, G.H.: A Method for Synthesizing Sequential Circuits. Bell System Technical Journal\u00a034(5), 1045\u20131079 (1955)","journal-title":"Bell System Technical Journal"},{"key":"21_CR25","series-title":"PHI Series in computer science","volume-title":"Communication and concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and concurrency. PHI Series in computer science. Prentice-Hall, Inc., Upper Saddle River (1989)"},{"key":"21_CR26","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)"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Proc. of Symposium on Applied Mathematics. Mathematical aspects of computer science, vol.\u00a019, pp. 19\u201332. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"21_CR28","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-18275-4_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Steffen","year":"2011","unstructured":"Steffen, B., R\u00fcthing, O.: Quality Engineering: Leveraging Heterogeneous Information - (Invited Talk). In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 23\u201337. Springer, Heidelberg (2011)"},{"key":"21_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/00207168808803702","volume":"27","author":"D.M. Dhamdhere","year":"1989","unstructured":"Dhamdhere, D.M.: A new algorithm for composite hoisting and strength reduction optimisation (+ Corrigendum). Int. J. Comp. Math.\u00a027, 1\u201314 (1989)","journal-title":"Int. J. Comp. Math."},{"issue":"4","key":"21_CR31","doi-asserted-by":"publisher","first-page":"1117","DOI":"10.1145\/183432.183443","volume":"16","author":"J. Knoop","year":"1994","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Optimal Code Motion: Theory and Practice. ACM Trans. Program. Lang. Syst.\u00a016(4), 1117\u20131155 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: The Power of Assignment Motion. In: Proceedings of the ACM SIGPLAN 1995 Conference on Programming Language Design and Implementation (PLDI). ACM (1995)","DOI":"10.1145\/207110.207150"},{"key":"21_CR33","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":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/3-540-52592-0_76","volume-title":"ESOP \u201990","author":"B. Steffen","year":"1990","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: The Value Flow Graph: A Program Representation for Optimal Program Transformations. In: Jones, N.D. (ed.) ESOP 1990. LNCS, vol.\u00a0432, pp. 389\u2013405. Springer, Heidelberg (1990)"},{"key":"21_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3540539816_78","volume-title":"TAPSOFT \u201991. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Brighton, UK, April 8-12, 1991","author":"B. Steffen","year":"1991","unstructured":"Steffen, B., Knoop, J., R\u00fcthing, O.: Efficient Code Motion and an Adaption to Strength Reduction. In: Abramsky, S. (ed.) TAPSOFT 1991. LNCS, vol.\u00a0494, pp. 394\u2013415. Springer, Heidelberg (1991)"},{"key":"21_CR36","unstructured":"Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley (2004)"},{"key":"21_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1007\/BFb0035794","volume-title":"Automata, Languages and Programming","author":"B. Steffen","year":"1989","unstructured":"Steffen, B.: Characteristic Formulae. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 723\u2013732. Springer, Heidelberg (1989)"},{"key":"21_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"CONCUR \u201995 Concurrency Theory","author":"B. Steffen","year":"1995","unstructured":"Steffen, B., Cla\u00dfen, A., Klein, M., Knoop, J., Margaria, T.: The Fixpoint-Analysis Machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 72\u201387. Springer, Heidelberg (1995)"},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Automata, Languages and Programming","author":"O. Burkart","year":"1997","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.) ICALP 1997. LNCS, vol.\u00a01256, pp. 419\u2013429. Springer, Heidelberg (1997)"},{"key":"21_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-70889-6_7","volume-title":"Hardware and Software, Verification and Testing","author":"B. Steffen","year":"2007","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.) HVC 2006. LNCS, vol.\u00a04383, pp. 92\u2013108. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39176-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T12:56:51Z","timestamp":1557752211000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39176-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642391750","9783642391767"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39176-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}