Hillel Kugler
Scientist
Biological Computation
Computational Science Laboratory
Microsoft Research Cambridge
Selected Papers:
SMT-based analysis of biological computation (NFM, 2013)
A model of stem cell population dynamics (Development, 2012)
Tools and project websites:
Upcoming Events:
TACAS'13 (PC) Tools and Algorithms for the Construction and Analysis of Systems
Research Interests:
- Systems Biology (Modeling and Analysis of Biological Systems, in particular in the fileds of developmental biology and stem cells)
- Software and System Engineering (Visual Languages, Formal Verification, Synthesis)
Publications : Bibtex file
Previously I was a member of Jane Hubbard's lab at the Biology Department and the Analysis of Computer Systems Group , Department of Computer Science, Courant Institute New York University
I did my Ph.D at the Weizmann Institute under the supervision of David Harel and Amir Pnueli
Post-doctoral, Ph.D positions and Internships available, for information please email me with an updated CV.
Publications
- Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi, and Hillel Kugler, Z34Bio: An SMT-based Framework for Analyzing Biological Computation, in SMT'13, July 2013
- Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi, and Hillel Kugler, SMT-based Analysis of Biological Computation, in NASA Formal Methods Symposium 2013, Springer Verlag, May 2013
- Boyan Yordanov, Christoph M. Wintersteiger, Youssef Hamadi, and Hillel Kugler, Z3-4biology SMT-based analysis of biological computation, no. MSR-TR-2012-31, 12 March 2012
- Yaki Setty, Diana Dalfó, Dorota Z. Korta, E. Jane Albert Hubbard, and Hillel Kugler, A model of stem cell population dynamics: in-silico analysis and in-vivo validation, in Development, vol. 139, pp. 47 - 56, January 2012
- Hillel Kugler, Cory Plock, and Andy Roberts, Synthesizing Biological Theories, in Computer Aided Verification (CAV'11), Springer Verlag, July 2011
- Aleks Milicevic and Hillel Kugler, Model Checking Using SMT and Theory of Lists , in Nasa Formal Methods Symposium , Springer Verlag, April 2011
- H. Kugler, A. Larjo, and D. Harel, Biocharts: A Visual Formalism for Complex Biological Systems, in Journal of the Royal Society Interface, vol. 7, no. 48, pp. 1015-1024, July 2010
- D. Harel, H. Kugler, S. Maoz, and I. Segall, Accelerating Smart Play-Out, in SOFSEM 2010: Theory and Practice of Computer Science, Springer Verlag, January 2010
- D. Harel and H. Kugler, Some Thoughts on the Semantics of Biocharts, in Essays in Memory of Amir Pnueli, Springer Verlag, 2010
- H. Kugler and I. Segall, Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications, in Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09), Springer Verlag, March 2009
- H. Kugler, C. Plock, and A. Pnueli, Controller Synthesis from LSC Requirements, in Fundamental Approaches to Software Engineering (FASE'09), Springer Verlag, March 2009
- D. Harel, H. Kugler, S. Maoz, and I. Segall, How Hard is Smart Play-Out? On the Complexity of Verification-Driven Execution, in Perspectives in Concurrency Theory (Festschrift for P.S. Thiagarajan), (K. Lodaya et al, eds.), University Press (India), 2009
- Harel, D., Segall, I., Kugler, H., Setty, and Y., Crafting Game-Models using Reactive System Design , in Future Play, Association for Computing Machinery, Inc., November 2008
- Kam N., Kugler H., Marelly R., Appleby L., Fisher J., A. Pnueli, D. Harel, M.J. Stern, and E.J.A. Hubbard, A scenario-based approach to modeling development: A prototype model of C. elegans vulval fate specification , in Developmental Biology, vol. 323, no. 1, pp. 1-5, Elsevier , August 2008
- P. Combes, D. Harel, and H. Kugler, Modeling and Verification of a Telecommunication Application using Live Sequence Charts and the Play-Engine Tool, in Software and Systems Modeling, vol. 7, no. 2, pp. 157-175, Springer Verlag, March 2008
- J. Hooman, H. Kugler, I. Ober, A. Votintseva, and Y. Yushtein, Supporting UML-based development of embedded systems by formal techniques, in Software and Systems Modeling, vol. 7, no. 2, pp. 131-155, Springer Verlag, 2008
- H. Kugler, C. Plock, and A. Pnueli, Synthesizing Reactive Systems from LSC Requirements using the Play-Engine, in Companion to the 22nd ACM SIGPLAN conference on object oriented programming systems and applications (OOPSLA’07), October 2007
- H. Kugler, M.J. Stern, and E.J.A. Hubbard, Testing Scenario-Based Models, in Fundamental Approaches to Software Engineering (FASE'07), Springer Verlag, 2007
- H. Kugler, A. Pnueli, M.J. Stern, and E.J.A. Hubbard, “Don’t Care” Modeling: A Logical Framework for Developing Predictive System Models, in Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), Springer Verlag, 2007
- H. Kugler, D. Harel, A. Pnueli, Y. Lu, and Y. Bontemps, Temporal Logic for Scenario-Based Specifications, Springer Verlag, 2005
- D. Harel, H. Kugler, and A. Pnueli, Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements, in Formal Methods in Software and Systems Modeling, Springer Verlag, 2005
- M. Kyas, H. Fecher, F.S. de Boer, J. Jacob, J. Hooman, M. van der Zwaag, T. Arons, and H. Kugler, Formalizing UML Models and OCL Constraints in PVS, in Proceedings of the Second Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 2004) , Elsevier, 2005
- D. Harel and H. Kugler, The Rhapsody Semantics of Statecharts, in Integration of Software Specification Techniques for Applications in Engineering, Springer Verlag, 2004
- D. Harel, H. Kugler, and A. Pnueli, Smart Play-Out Extended: Time and Forbidden Elements, in International Conference on Quality Software, IEEE Computer Society, 2004
- T. Arons, J. Hooman, H. Kugler, A. Pnueli, and M. van der Zwaag, Deductive Verification of UML Models in TLPVS, Springer Verlag, 2004
- N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, E.J.A. Hubbard, and M.J. Stern, Formal Modeling of C. elegans Development: A Scenario-Based Approach, Springer Verlag, 2003
- D. Harel, H. Kugler, and G. Weiss, Some Methodological Observations Resulting from Experience Using LSCs and the Play-In/Play-Out Approach, Springer Verlag, 2003
- R. Marelly, D. Harel, and H. Kugler, Multiple Instances and Symbolic Variables in Executable Sequence Charts, in Proc. 17th Ann. ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA'02), Seattle, WA, Association for Computing Machinery, Inc., November 2002
- D. Harel, H. Kugler, R. Marelly, and A. Pnueli, Smart Play-Out of Behavioral Requirements, in Proc. 4th Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD'02), Portland, Oregon, Springer Verlag, November 2002
- D. Harel and H. Kugler, Synthesizing State-Based Object Systems from LSC Specifications, in International Journal of Foundations of Computer Science, vol. 13, no. 1, pp. 5–51, World Scientific Publishing, February 2002
