{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:28:45Z","timestamp":1750307325331,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,6,27]],"date-time":"2011-06-27T00:00:00Z","timestamp":1309132800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2011,6,27]]},"DOI":"10.1145\/1988932.1988935","type":"proceedings-article","created":{"date-parts":[[2011,7,5]],"date-time":"2011-07-05T13:24:14Z","timestamp":1309872254000},"page":"11-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["SMT-based optimization for synchronous programs"],"prefix":"10.1145","author":[{"given":"Yu","family":"Bai","sequence":"first","affiliation":[{"name":"University of Kaiserslautern, Germany"}]},{"given":"Jens","family":"Brandt","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern, Germany"}]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2011,6,27]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/390013.808479"},{"key":"e_1_3_2_1_2_1","volume-title":"Department of Computer Science","author":"Bai Y.","year":"2010","unstructured":"Y. Bai . Dependency analysis of synchronous programming languages. Master's thesis , Department of Computer Science , University of Kaiserslautern , Germany, November 2010 . Y. Bai. Dependency analysis of synchronous programming languages. Master's thesis, Department of Computer Science, University of Kaiserslautern, Germany, November 2010."},{"key":"e_1_3_2_1_3_1","first-page":"825","volume-title":"Handbook of Satisfiability","author":"Barrett C.","year":"2009","unstructured":"C. Barrett , R. Sebastiani , S. Seshia , and C. Tinelli . Satisfiability modulo theories . In Handbook of Satisfiability , pages 825 -- 885 . IOS Press , 2009 . C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, pages 825--885. IOS Press, 2009."},{"key":"e_1_3_2_1_4_1","unstructured":"G. Berry. The constructive semantics of pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/ July 1999.  G. Berry. The constructive semantics of pure Esterel. http:\/\/www-sop.inria.fr\/esterel.org\/ July 1999."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836090"},{"key":"e_1_3_2_1_7_1","series-title":"ACM International Conference Proceeding Series","first-page":"1","volume-title":"Software and Compilers for Embedded Systems (SCOPES)","author":"Brandt J.","year":"2009","unstructured":"J. Brandt and K. Schneider . Separate compilation for synchronous programs . In H. Falk, editor, Software and Compilers for Embedded Systems (SCOPES) , volume 320 of ACM International Conference Proceeding Series , pages 1 -- 10 , Nice, France , 2009 . ACM. J. Brandt and K. Schneider. Separate compilation for synchronous programs. In H. Falk, editor, Software and Compilers for Embedded Systems (SCOPES), volume 320 of ACM International Conference Proceeding Series, pages 1--10, Nice, France, 2009. ACM."},{"key":"e_1_3_2_1_8_1","first-page":"161","volume-title":"Formal Methods and Models for Codesign (MEMOCODE)","author":"Brandt J.","year":"2009","unstructured":"J. Brandt and K. Schneider . Static data-flow analysis of synchronous programs . In R. Bloem and P. Schaumont, editors, Formal Methods and Models for Codesign (MEMOCODE) , pages 161 -- 170 , Cambridge, Massachusetts, USA , 2009 . IEEE Computer Society . J. Brandt and K. Schneider. Static data-flow analysis of synchronous programs. In R. Bloem and P. Schaumont, editors, Formal Methods and Models for Codesign (MEMOCODE), pages 161--170, Cambridge, Massachusetts, USA, 2009. IEEE Computer Society."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/59087"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/978-3-540-73368-3_5","volume-title":"Computer Aided Verification (CAV)","author":"de Moura L.","year":"2007","unstructured":"L. de Moura , B. Dutertre , and N. Shankar . A tutorial on satisfiability modulo theories . In W. Damm and H. Hermanns, editors, Computer Aided Verification (CAV) , volume 4590 of LNCS , pages 20 -- 36 , Berlin, Germany , 2007 . Springer . L. de Moura, B. Dutertre, and N. Shankar. A tutorial on satisfiability modulo theories. In W. Damm and H. Hermanns, editors, Computer Aided Verification (CAV), volume 4590 of LNCS, pages 20--36, Berlin, Germany, 2007. Springer."},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification (CAV)","author":"Dill D.","year":"1996","unstructured":"D. Dill . The Murphi verification system . In R. Alur and T. Henzinger, editors, Computer Aided Verification (CAV) , volume 1102 of LNCS , pages 390 -- 393 , New Brunswick, New Jersey, USA , 1996 . Springer . D. Dill. The Murphi verification system. In R. Alur and T. Henzinger, editors, Computer Aided Verification (CAV), volume 1102 of LNCS, pages 390--393, New Brunswick, New Jersey, USA, 1996. Springer."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/74382.74475"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_20"},{"key":"e_1_3_2_1_15_1","first-page":"789","volume-title":"System Sciences","author":"Greenstreet M.","year":"1989","unstructured":"M. Greenstreet , K. Li , and J. Straunstrup . ' synchronized transitions' on multiprocessors . In System Sciences , pages 789 -- 797 , Kailua-Kona, Hawaii, USA , 1989 . IEEE Computer Science. M. Greenstreet, K. Li, and J. Straunstrup. 'synchronized transitions' on multiprocessors. In System Sciences, pages 789--797, Kailua-Kona, Hawaii, USA, 1989. IEEE Computer Science."},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-54444-5_100","volume-title":"Programming Language Implementation and Logic Programming (PLILP)","author":"Halbwachs N.","year":"1991","unstructured":"N. Halbwachs , P. Raymond , and C. Ratel . Generating efficient code from data-flow programs . In J. Maluszy\u0144ski and M. Wirsing, editors, Programming Language Implementation and Logic Programming (PLILP) , volume 528 of LNCS , pages 207 -- 218 , Passau, Germany , 1991 . Springer . N. Halbwachs, P. Raymond, and C. Ratel. Generating efficient code from data-flow programs. In J. Maluszy\u0144ski and M. Wirsing, editors, Programming Language Implementation and Logic Programming (PLILP), volume 528 of LNCS, pages 207--218, Passau, Germany, 1991. Springer."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512946"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/321832.321835"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325700"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_1_22_1","volume-title":"Decision Procedures","author":"Kroening D.","year":"2008","unstructured":"D. Kroening and O. Strichman . Decision Procedures . Springer , 2008 . D. Kroening and O. Strichman. Decision Procedures. Springer, 2008."},{"key":"e_1_3_2_1_23_1","volume-title":"Embedded System Design","author":"Marwedel P.","year":"2005","unstructured":"P. Marwedel . Embedded System Design . Springer , 2005 . P. Marwedel. Embedded System Design. Springer, 2005."},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","first-page":"337","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Mendon\u00e7a de Moura L.","year":"2008","unstructured":"L. Mendon\u00e7a de Moura and N. Bj\u00f8rner . Z3: An efficient SMT solver . In C. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , volume 4963 of LNCS , pages 337 -- 340 , Budapest, Hungary , 2008 . Springer . L. Mendon\u00e7a de Moura and N. Bj\u00f8rner. Z3: An efficient SMT solver. In C. Ramakrishnan and J. Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS, pages 337--340, Budapest, Hungary, 2008. Springer."},{"key":"e_1_3_2_1_25_1","volume-title":"Morgan Kaufmann","author":"Muchnick S.","year":"1997","unstructured":"S. Muchnick . Advanced Compiler Design and Implementation . Morgan Kaufmann , 1997 . S. Muchnick. Advanced Compiler Design and Implementation. Morgan Kaufmann, 1997."},{"key":"e_1_3_2_1_26_1","volume-title":"Compiling Esterel","author":"Potop-Butucaru D.","year":"2007","unstructured":"D. Potop-Butucaru , S. Edwards , and G. Berry . Compiling Esterel . Springer , 2007 . D. Potop-Butucaru, S. Edwards, and G. Berry. Compiling Esterel. Springer, 2007."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/359842.359849"},{"key":"e_1_3_2_1_28_1","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"Schneider K.","year":"2001","unstructured":"K. Schneider . Improving automata generation for linear temporal logic by considering the automata hierarchy . In R. Nieuwenhuis and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) , volume 2250 of LNAI , pages 39 -- 54 , Havana, Cuba , 2001 . Springer . K. Schneider. Improving automata generation for linear temporal logic by considering the automata hierarchy. In R. Nieuwenhuis and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 2250 of LNAI, pages 39--54, Havana, Cuba, 2001. Springer."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1023833.1023859"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.028"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_2_1_33_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/3-540-44898-5_6","volume-title":"Static Analysis Symposium (SAS)","author":"Tardieu O.","year":"2003","unstructured":"O. Tardieu and R. de Simone . Instantaneous termination in pure Esterel . In R. Cousot, editor, Static Analysis Symposium (SAS) , volume 2694 of LNCS , pages 91 -- 108 . Springer , 2003 . O. Tardieu and R. de Simone. Instantaneous termination in pure Esterel. In R. Cousot, editor, Static Analysis Symposium (SAS), volume 2694 of LNCS, pages 91--108. Springer, 2003."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459813"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/993644"}],"event":{"name":"SCOPES '11: International Workshop on Software and Compilers for Embedded Systems","sponsor":["EDAA European Design Automation Association","HiPEAC HiPEAC Network of Excellence","ArtistDesign European NoE","SIGBED ACM Special Interest Group on Embedded Systems"],"location":"St. Goar Germany","acronym":"SCOPES '11"},"container-title":["Proceedings of the 14th International Workshop on Software and Compilers for Embedded Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1988932.1988935","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1988932.1988935","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:06:00Z","timestamp":1750244760000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1988932.1988935"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,27]]},"references-count":33,"alternative-id":["10.1145\/1988932.1988935","10.1145\/1988932"],"URL":"https:\/\/doi.org\/10.1145\/1988932.1988935","relation":{},"subject":[],"published":{"date-parts":[[2011,6,27]]},"assertion":[{"value":"2011-06-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}