@STRING{lncs = "Lect. Notes in Comp. Sci."} @INPROCEEDINGS{AHKPZ04, AUTHOR = "T. Arons and J. Hooman and H. Kugler and A. Pnueli and M. van der Zwaag", BOOKTITLE = "Proc. 7th International Conference on UML Modeling Languages and Applications (UML 2004)", EDITOR = "T. Baar and A. Strohmeier and A. Moreira and S. J. Mellor", PAGES = "335--349", MONTH = "October", PUBLISHER = springer, SERIES = lncs, TITLE = {{Deductive Verification of UML Models in TLPVS}}, VOLUME = "3273", YEAR = "2004", } @INPROCEEDINGS{BHK03, AUTHOR = "Y. Bontemps and P. Heymans and H. Kugler", BOOKTITLE = "Proc.\2nd Int. Workshop on Scenarios and State Machines (SCESM'03)", TITLE = {{Applying LSCs to an Air Traffic Control Case Study}}, YEAR = "2003", } @INPROCEEDINGS{CHK05, AUTHOR = "P. Combes and D. Harel and H. Kugler", BOOKTITLE = {{Proc. 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA '05)}}, PAGES = "414--428", MONTH = "", PUBLISHER = springer, SERIES = lncs, TITLE = {{Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool}}, VOLUME = "3707", YEAR = "2005", } @INPROCEEDINGS{HK00b, AUTHOR = "D. Harel and H. Kugler", BOOKTITLE = "Proc. 5th Inf. Conf. on Implementation and Application of Automata (CIAA'00)", PAGES = "1--33", MONTH = "July", PUBLISHER = springer, SERIES = lncs, TITLE = "Synthesizing State-Based Object Systems from {LSC} Specifications", VOLUME = "2088", YEAR = "2000", } @ARTICLE{HK01, AUTHOR = "D. Harel and H. Kugler", JOURNAL = "Int. J. of Foundations of Computer Science (IJFCS).", NOTE = "(Also,{\em Proc. Fifth Int. Conf. on Implementation and Application of Automata (CIAA 2000)}, July 2000, Lecture Notes in Computer Science, Springer-Verlag, 2000.)", NUMBER = "1", PAGES = "5--51", TITLE = "Synthesizing State-Based Object Systems from {LSC} Specifications", VOLUME = "13", MONTH = "Febuary", YEAR = "2002", } @INPROCEEDINGS{HK04, AUTHOR = "D. Harel and H. Kugler", BOOKTITLE = "Integration of Software Specification Techniques for Application in Engineering", PAGES = "325--354", MONTH = "", PUBLISHER = springer, SERIES = lncs, TITLE = {{The RHAPSODY Semantics of Statecharts (or, On the Executable Core of the UML)}}, VOLUME = "3147", YEAR = "2004", } @INPROCEEDINGS{HK10, AUTHOR = "D. Harel and H. Kugler", BOOKTITLE = "Time for Verification", EDITOR = "Z. Manna and D. Peled", PAGES = "185-194", PUBLISHER = springer, SERIES = lncs, TITLE = {{Some Thoughts on the Semantics of Biocharts}}, VOLUME = "6200", YEAR = "2010", } @INPROCEEDINGS{HKMP02, AUTHOR = "D. Harel and H. Kugler and R. Marelly and A. Pnueli", BOOKTITLE = fmcad02, SERIES = lncs, VOLUME = "2517", PAGES = "378--398", NOTE = "Also available as Tech. Report MCS02-08, The Weizmann Institute of Science", TITLE = "Smart Play-Out of Behavioral Requirements", YEAR = "2002", } INPROCEEDINGS{HKMP03, AUTHOR = "D. Harel and H. Kugler and R. Marelly and A. Pnueli", BOOKTITLE = {Companion of the 18th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications}, PUBLISHER = "ACM Press", TITLE = "Smart Play-Out", PAGES = "68-69", YEAR = {2003} } @INPROCEEDINGS{HKMS09, AUTHOR = "D. Harel and H. Kugler and S. Maoz and I. Segall", BOOKTITLE = "Perspectives in Concurrency Theory (Festschrift for P.S. Thiagarajan)", PUBLISHER = "University Press (India)", VOLUME = "", PAGES = "208--230", TITLE = {{How Hard is Smart Play-Out? On the Complexity of Verification-Driven Execution}}, YEAR = "2009", } @INPROCEEDINGS{HKP04, AUTHOR = {D. Harel and H. Kugler and A. Pnueli}, BOOKTITLE = "International Conference on Quality Software (QSIC04)", TITLE = {{Smart Play-Out Extended: Time and Forbidden Elements }}, PUBLISHER = "IEEE Press", PAGES = "2--10", YEAR = {2004}, } @INPROCEEDINGS{HKP05, AUTHOR = {D. Harel and H. Kugler and A. Pnueli}, BOOKTITLE = "Formal Methods in Software and System Modeling", SERIES = lncs, VOLUME = "3393", TITLE = {{Synthesis Revisited: Generating Statechart Models from Scenarios-Based Requirements}}, PUBLISHER = springer, PAGES = "309-324", YEAR = {2005}, } @INPROCEEDINGS{HSKS08, AUTHOR = "D. Harel and I. Segall and H. Kugler and Y. Setty", BOOKTITLE = {{Proceedings of the 2008 conference on Future Play (Future Play '08)}}, EDITOR = "", PAGES = "", TITLE = "Crafting Game-Models using Reactive System Design", PUBLISHER = "ACM", YEAR = "2008", } @INPROCEEDINGS{HKMS10, AUTHOR = {D. Harel and H. Kugler and S. Maoz and I. Segall}, BOOKTITLE = {{Proc. 36th Int. Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM 2010)}}, SERIES = lncs, VOLUME = "", TITLE = {{Accelerating Smart Play-Out}}, PUBLISHER = springer, PAGES = "", YEAR = {2010}, } @INPROCEEDINGS{HKW05, AUTHOR = {D. Harel and H. Kugler and G. Weiss}, BOOKTITLE = "Proc.\ Scenarios: Models, Algorithms and Tools", SERIES = lncs, VOLUME = "3466", TITLE = {{Some Methodological Observations Resulting from Experience Using LSCs and the Play-In/Play-Out Approach}}, PUBLISHER = springer, PAGES = "26--42", YEAR = {2005} } @INPROCEEDINGS{KFBJZHAK04, AUTHOR = "M. Kyas and H. Fecher and F.S. de Boer and J. Jacob and M. van der Zwaag and J. Hooman and T. Arons and H. Kugler", PAGES = "39--47", BOOKTITLE = {{Workshop on Semantic Foundations of Engineering Design Languages (SFEDL'04)}}, SERIES = {{Electr. Notes Theor. Comput. Sci.}}, TITLE = {{Formalizing UML Models and OCL Constraints in PVS}}, VOLUME = "115", YEAR = "2005", } @INPROCEEDINGS{KHKMPHS03, AUTHOR = {N. Kam and D. Harel and H. Kugler and R. Marelly and A. Pnueli and E.J.A. Hubbard and M.J. Stern}, TITLE = {{Formal Modeling of C. elegans Development: A Scenario-Based Approach}}, BOOKTITLE = {{Proc. Int. Workshop on Computational Methods in Systems Biology (CMSB 2003)}}, NOTE = {{Extended version appeared in Modeling in Molecular Biology, G.Ciobanu (Ed.), Natural Computing Series, Springer, 2004 .}}, PUBLISHER = springer, SERIES = lncs, VOLUME = "2602", EDITOR = {{Corrado Priami}}, PAGES = "4--20", YEAR = "2003", } @INPROCEEDINGS{KHPLB05, AUTHOR = {H. Kugler and D. Harel and A. Pnueli and Y. Lu and Y. Bontemps}, TITLE = {{Temporal Logic for Scenario-Based Specifications}}, BOOKTITLE = {{Proc.\ $11^{th}$ Intl.\ Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'05)}}, PUBLISHER = springer, SERIES = lncs, VOLUME = "3440", EDITOR = {{N. Halbwachs and L.D. Zuck}}, PAGES = "445--460", YEAR = "2005", } @ARTICLE{KKMAFPHSH08, AUTHOR = "N. Kam and H. Kugler and R. Marelly and L. Appleby and J. Fisher and A. Pnueli and D. Harel and M.J. Stern and E.J.A. Hubbard", JOURNAL = "Developmental Biology", NUMBER = "1", PAGES = "1--5", TITLE = {{A scenario-based approach to modeling development: A prototype model of C. elegans vulval fate specification}}, VOLUME = "323", NOTE = "", YEAR = "2008", } @ARTICLE{KLH10, AUTHOR = "H. Kugler and A. Larjo and D. Harel", JOURNAL = "J. R. Soc. Interface", NUMBER = "48", PAGES = "1015--1024", TITLE = {{Biocharts: A Visual Formalism for Complex Biological Systems}}, VOLUME = "7", YEAR = "2010", } @INPROCEEDINGS{KPP09, AUTHOR = "H. Kugler and C. Plock and A. Pnueli", BOOKTITLE = "12th International Conference on Fundamental Approaches to Software Engineering, (FASE 2009)", PAGES = "79--93", PUBLISHER = springer, SERIES = lncs, TITLE = {{Controller Synthesis from LSC Requirements}}, VOLUME = "5503", YEAR = "2009", } @INPROCEEDINGS{KPR11, AUTHOR = {H. Kugler and C. Plock and A. Roberts}, TITLE = {{Synthesizing Biological Theories}}, BOOKTITLE = {{Proc.\ $23^{rd}$ Int. Conf. on Computer Aided Verification (CAV'11)}}, PUBLISHER = springer, SERIES = lncs, VOLUME = "6806", EDITOR = "G. Gopalakrishnan and S. Qadeer", PAGES = "579--584", YEAR = "2011", } @INPROCEEDINGS{KS09, AUTHOR = {H. Kugler and I. Segall}, TITLE = {{Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications}}, BOOKTITLE = {{Proc.\ $15^{th}$ Intl.\ Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09)}}, PUBLISHER = springer, SERIES = lncs, VOLUME = "", EDITOR = "", PAGES = "", YEAR = "2009", } @TECHREPORT{KW04, AUTHOR = "H.Kugler and G. Weiss", INSTITUTION = "Weizmann Institute", KEY = "MCS04-05", TITLE = {{Planning a Production Line with LSCs}}, YEAR = "2004", } @INPROCEEDINGS{MHK02, AUTHOR = "R. Marelly and D. Harel and H. Kugler", BOOKTITLE = "Proc.\ 17th Ann.\ {ACM} Conf.\ on Object-Oriented Programming, Systems, Languages and Applications {(OOPSLA'02)}", PAGES = "83--100", TITLE = "Multiple Instances and Symbolic Variables in Executable Sequence Charts", ADDRESS = "Seattle, WA", YEAR = "2002", } @INPROCEEDINGS{MK11, AUTHOR = {A. Milicevic and H. Kugler}, TITLE = {{Model Checking Using SMT and Theory of Lists}}, BOOKTITLE = {{Proc.\ $3^{rd}$ NASA Formal Methods Symposium (NFM'11)}}, PUBLISHER = springer, SERIES = lncs, VOLUME = "6617", EDITOR = "M. Bobaru and K. Havelund and G. Holzmann and Gerard R. Joshi", PAGES = "282--297", YEAR = "2011", } @ARTICLE{SDKHK12, AUTHOR = "Y. Setty and D. Dalfo and D.Z. Korta and E.J.A. Hubbard and H. Kugler", JOURNAL = "Development", NUMBER = "1", PAGES = "47--56", TITLE = {{A model of stem cell population dynamics: in-silico analysis and in-vivo validation}}, VOLUME = "139", NOTE = "", YEAR = "2012", }