Smart Play-out of Behavioral Requirements. - David Harel; Hillel Kugler; Rami Marelly; Amir Pnueli (FMCAD, 2002)

Multiple instances and symbolic variables in executable sequence charts. - Rami Marelly; David Harel; Hillel Kugler (OOPSLA, 2002)

Specifying and executing requirements: the play-in/play-out approach. - Rami Marelly; David Harel; Hillel Kugler (OOPSLA Companion, 2002)

Synthesizing State-Based Object Systems from LSC Specifications. - David Harel; Hillel Kugler (Int. J. Found. Comput. Sci., 2002)

Formal Modeling of C. elegans Development: A Scenario-Based Approach. - Na'aman Kam; David Harel; Hillel Kugler; Rami Marelly; Amir Pnueli; E. Jane Albert Hubbard; Michael J. Stern (CMSB, 2003)

Some Methodological Observations Resulting from Experience Using LSCs and the Play-In/Play-Out Approach. - David Harel; Hillel Kugler; Gera Weiss (Scenarios: Models, Transformations and Tools, 2003)

Smart play-out. - David Harel; Hillel Kugler; Rami Marelly; Amir Pnueli (OOPSLA Companion, 2003)

The Rhapsody Semantics of Statecharts (or, On the Executable Core of the UML) - Preliminary Version. - David Harel; Hillel Kugler (SoftSpez Final Report, 2004)

Smart Play-Out Extended: Time and Forbidden Elements. - David Harel; Hillel Kugler; Amir Pnueli (QSIC, 2004)

Deductive Verification of UML Models in TLPVS. - Tamarah Arons; Jozef Hooman; Hillel Kugler; Amir Pnueli; Mark van der Zwaag (UML, 2004)

Formalizing UML Models and OCL Constraints in PVS. - Marcel Kyas; Harald Fecher; Frank S. de Boer; Joost Jacob; Jozef Hooman; Mark van der Zwaag; Tamarah Arons; Hillel Kugler (SFEDL@ETAPS, 2004)

Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. - David Harel; Hillel Kugler; Amir Pnueli (Formal Methods in Software and Systems Modeling, 2005)

Temporal Logic for Scenario-Based Specifications. - Hillel Kugler; David Harel; Amir Pnueli; Yuan Lu; Yves Bontemps (TACAS, 2005)

Testing Scenario-Based Models. - Hillel Kugler; Michael J. Stern; E. Jane Albert Hubbard (FASE, 2007)

Synthesizing reactive systems from LSC requirements using the play-engine. - Hillel Kugler; Cory Plock; Amir Pnueli (OOPSLA Companion, 2007)

"Don't Care" Modeling: A Logical Framework for Developing Predictive System Models. - Hillel Kugler; Amir Pnueli; Michael J. Stern; E. Jane Albert Hubbard (TACAS, 2007)

Crafting game-models using reactive system design. - David Harel; Itai Segall; Hillel Kugler; Yaki Setty (Future Play, 2008)

Modeling and verification of a telecommunication application using live sequence charts and the Play-Engine tool. - Pierre Combes; David Harel; Hillel Kugler (Softw. Syst. Model., 2008)

Supporting UML-based development of embedded systems by formal techniques. - Jozef Hooman; Hillel Kugler; Iulian Ober; Anjelika Votintseva; Yuri Yushtein (Softw. Syst. Model., 2008)

Controller Synthesis from LSC Requirements. - Hillel Kugler; Cory Plock; Amir Pnueli (FASE, 2009)

Compositional Synthesis of Reactive Systems from Live Sequence Chart Specifications. - Hillel Kugler; Itai Segall (TACAS, 2009)

Some Thoughts on the Semantics of Biocharts. - David Harel; Hillel Kugler (Essays in Memory of Amir Pnueli, 2010)

Accelerating Smart Play-Out. - David Harel; Hillel Kugler; Shahar Maoz; Itai Segall (SOFSEM, 2010)

Synthesizing Biological Theories. - Hillel Kugler; Cory Plock; Andy Roberts (CAV, 2011)

Model Checking Using SMT and Theory of Lists. - Aleksandar Milicevic; Hillel Kugler (NASA Formal Methods, 2011)

Functional Analysis of Large-Scale DNA Strand Displacement Circuits. - Boyan Yordanov; Christoph M. Wintersteiger; Youssef Hamadi; Andrew Phillips; Hillel Kugler (DNA, 2013)

Biocharts: Unifying Biological Hypotheses with Models and Experiments. - Hillel Kugler (e-Science, 2013)

SMT-Based Analysis of Biological Computation. - Boyan Yordanov; Christoph M. Wintersteiger; Youssef Hamadi; Hillel Kugler (NASA Formal Methods, 2013)

Runtime Verification and Refutation for Biological Systems. - Hillel Kugler (RV, 2013)

Analyzing and Synthesizing Genomic Logic Functions. - Nicola Paoletti; Boyan Yordanov; Youssef Hamadi; Christoph M. Wintersteiger; Hillel Kugler (CAV, 2014)

Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains. - Markus N. Rabe; Christoph M. Wintersteiger; Hillel Kugler; Boyan Yordanov; Youssef Hamadi (QEST, 2014)

Switching Gene Regulatory Networks. - Yoli Shavit; Boyan Yordanov; Sara-Jane Dunn; Christoph M. Wintersteiger; Youssef Hamadi; Hillel Kugler (IPCAT, 2015)

Unifying Modelling and Programming: A Systems Biology Perspective. - Hillel Kugler (ISoLA (2), 2016)

Automated Synthesis and Analysis of Switching Gene Regulatory Networks. - Yoli Shavit; Boyan Yordanov; Sara-Jane Dunn; Christoph M. Wintersteiger; Tomoki Otani; Youssef Hamadi; Frederick J. Livesey; Hillel Kugler (Biosyst., 2016)

Formal Analysis of Network Motifs. - Hillel Kugler; Sara-Jane Dunn; Boyan Yordanov (CMSB, 2018)

Temporal Reasoning on Incomplete Paths. - Dana Fisman; Hillel Kugler (ISoLA (2), 2018)

Temporal Logic Based Synthesis of Experimentally Constrained Interaction Networks. - Judah Goldfeder; Hillel Kugler (MLCSB, 2018)

Large-scale Genetic Exploration of Genome-wide Models: an Application to Human Cancer Metabolism. - Youssef Hamadi; Claudio Angione; Hillel Kugler; Christoph M. Wintersteiger; Boyan Yordanov (IEEE DataPort, 2018)

BRE: IN - A Backend for Reasoning About Interaction Networks with Temporal Logic. - Judah Goldfeder; Hillel Kugler (CMSB, 2019)

TEMPO: Thermal-Efficient Management of Power in High-Throughput Network Switches. - Tom Munk; Hillel Kugler; Ofir Maori; Adam Teman (VLSI-DAT, 2019)

Formal Verification for Natural and Engineered Biological Systems. - Hillel Kugler (FMCAD, 2020)

Formal Semantics and Verification of Network-Based Biocomputation Circuits. - Michelle Aluf-Medina; Till Korten; Avraham Raviv; Dan V. Nicolau Jr.; Hillel Kugler (VMCAI, 2021)

Physical requirements for scaling up network-based biocomputation. - Jingyuan Zhu; Till Korten; Hillel Kugler; Falco C. M. J. M. van Delft; Alf Månsson; Danny Reuter; Stefan Diez; Heiner Linke (CoRR, 2021)

Formal Analysis of Network Motifs Links Structure to Function in Biological Programs. - Sara-Jane Dunn; Hillel Kugler; Boyan Yordanov (IEEE ACM Trans. Comput. Biol. Bioinform., 2021)

Discovering Essential Multiple Gene Effects Through Large Scale Optimization: An Application to Human Cancer Metabolism. - Annalisa Occhipinti; Youssef Hamadi; Hillel Kugler; Christoph M. Wintersteiger; Boyan Yordanov; Claudio Angione (IEEE ACM Trans. Comput. Biol. Bioinform., 2021)

An SMT-Based Framework for Reasoning About Discrete Biological Models. - Boyan Yordanov; Sara-Jane Dunn; Colin Gravill; Hillel Kugler; Christoph M. Wintersteiger (ISBRA, 2022)

Modeling the C. elegans germline stem cell genetic network using automated reasoning. - Ani Amar; E. Jane Albert Hubbard; Hillel Kugler (Biosyst., 2022)

Solving the 3-Satisfiability Problem Using Network-Based Biocomputation. - Jingyuan Zhu; Aseem Salhotra; Christoph Robert Meinecke; Pradheebha Surendiran; Roman Lyttleton; Danny Reuter; Hillel Kugler; Stefan Diez; Alf Månsson; Heiner Linke; Till Korten (Adv. Intell. Syst., 2022)

Prediction and Control of Stochastic Agents Using Formal Methods. - Avraham Raviv; Yuval Gerber; Liri Benzinou; Michelle Aluf-Medina; Hillel Kugler (FoMLAS@CAV, 2023)

Simulation and Verification of Network-Based Biocomputation Circuits. - Michelle Aluf-Medina; Avraham Raviv; Himanshu Arora; Till Korten; Hillel Kugler (ISCAS, 2023)

Learning Through Imitation by Using Formal Verification. - Avraham Raviv; Eliya Bronshtein; Or Reginiano; Michelle Aluf-Medina; Hillel Kugler (SOFSEM, 2023)

The Reasoning Engine: A Satisfiability Modulo Theories-Based Framework for Reasoning About Discrete Biological Models. - Boyan Yordanov; Sara-Jane Dunn; Colin Gravill; Himanshu Arora; Hillel Kugler; Christoph M. Wintersteiger (J. Comput. Biol., 2023)

Methods and Tools to Facilitate RE:IN Modeling and Analysis of GRNs. - Daniel Grimland; Eitan Tannenbaum; Hillel Kugler (CIBB, 2024)

Synthesis of Boolean Networks with Weak and Strong Regulators. - Noy Biton; Sharon Shoob; Ani Amar; Hillel Kugler (ISBRA (2), 2024)

Formal Verification of Object Detection. - Avraham Raviv; Yizhak Yisrael Elboher; Michelle Aluf-Medina; Yael Leibovich Weiss; Omer Cohen; Roy Assa; Guy Katz; Hillel Kugler (CoRR, 2024)

Robust Deep Reinforcement Learning Using Formal Verification. - Avraham Raviv; Shaiel Vistuch; Boaz Gurevich; Erel Dekel; Hillel Kugler (TASE, 2025)