| 2026 | CONCUR | Classification Under Uncertainty. | Orna Kupferman, Ofer Leshkowitz |
| 2026 | CSL | Memory Requirements in Non-Zero-Sum Games. | Yoav Feinstein, Orna Kupferman |
| 2025 | ATVA | Energy Games with Weight Uncertainty. | Orna Kupferman, Naama Shamash Halevy |
| 2025 | CONCUR | Coverage Games. | Orna Kupferman, Noam Shenwald |
| 2025 | MFCS | Positional-Player Games. | Orna Kupferman, Noam Shenwald |
| 2025 | TACAS | Non-Zero-Sum Games with Multiple Weighted Objectives. | Yoav Feinstein, Orna Kupferman, Noam Shenwald |
| 2025 | TACAS | Synthesis with Guided Environments. | Orna Kupferman, Ofer Leshkowitz |
| 2024 | ATVA | Playing Games on Automata. | Orna Kupferman |
| 2024 | ATVA | Games with Weighted Multiple Objectives. | Orna Kupferman, Noam Shenwald |
| 2024 | ATVA | Easy Complementation of History-Deterministic Bchi Automata. | Bader Abu Radi, Orna Kupferman, Ofer Leshkowitz |
| 2024 | FOSSACS | Synthesis with Privacy Against an Observer. | Orna Kupferman, Ofer Leshkowitz, Naama Shamash Halevy |
| 2023 | CONCUR | Games with Trading of Control. | Orna Kupferman, Noam Shenwald |
| 2023 | ICALP | On Semantically-Deterministic Automata. | Bader Abu Radi, Orna Kupferman |
| 2022 | ATVA | Minimization of Automata for Liveness Languages. | Bader Abu Radi, Orna Kupferman |
| 2022 | CONCUR | CONCUR Test-Of-Time Award 2022 (Invited Paper). | Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, Davide Sangiorgi |
| 2022 | CONCUR | Energy Games with Resource-Bounded Environments. | Orna Kupferman, Naama Shamash Halevy |
| 2022 | TACAS | The Complexity of LTL Rational Synthesis. | Orna Kupferman, Noam Shenwald |
| 2021 | ATVA | Certifying DFA Bounds for Recognition and Separation. | Orna Kupferman, Nir Lavee, Salomon Sickert |
| 2021 | FOSSACS | Certifying Inexpressibility. | Orna Kupferman, Salomon Sickert |
| 2021 | LICS | Perspective Multi-Player Games. | Orna Kupferman, Noam Shenwald |
| 2021 | MFCS | A Hierarchy of Nondeterminism. | Bader Abu Radi, Orna Kupferman, Ofer Leshkowitz |
| 2020 | ATVA | On (I/O)-Aware Good-For-Games Automata. | Rachel Faran, Orna Kupferman |
| 2020 | CAV | Good-Enough Synthesis. | Shaull Almagor, Orna Kupferman |
| 2020 | CSL | Coverage and Vacuity in Network Formation Games. | Gili Bielous, Orna Kupferman |
| 2020 | ECAI | Reasoning About Quality and Fuzziness of Strategic Behaviours. | Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, Giuseppe Perelli |
| 2020 | FMCAD | From Correctness to High Quality. | Orna Kupferman |
| 2020 | MFCS | Unary Prime Languages. | Ismal Jecker, Orna Kupferman, Nicolas Mazzocchi |
| 2020 | MFCS | On Repetition Languages. | Orna Kupferman, Ofer Leshkowitz |
| 2020 | SOFSEM | On Synthesis of Specifications with Arithmetic. | Rachel Faran, Orna Kupferman |
| 2019 | CONCUR | Register-Bounded Synthesis. | Ayrat Khalimov, Orna Kupferman |
| 2019 | ICALP | Minimizing GFG Transition-Based Automata. | Bader Abu Radi, Orna Kupferman |
| 2019 | IJCAI | Reasoning about Quality and Fuzziness of Strategic Behaviours. | Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, Giuseppe Perelli |
| 2019 | LICS | Perspective Games. | Orna Kupferman, Gal Vardi |
| 2018 | FM | Timed Vacuity. | Hana Chockler, Shibashis Guha, Orna Kupferman |
| 2018 | ICALP | The Unfortunate-Flow Problem. | Orna Kupferman, Gal Vardi |
| 2018 | IJCAI | Synthesis of Controllable Nash Equilibria in Quantitative Objective Game. | Shaull Almagor, Orna Kupferman, Giuseppe Perelli |
| 2018 | LPAR | LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems. | Rachel Faran, Orna Kupferman |
| 2018 | LPAR | Playing with the Maximum-Flow Problem. | Orna Kupferman |
| 2018 | LPAR | Alternating Reachability Games with Behavioral and Revenue Objectives. | Orna Kupferman, Tami Tamir |
| 2018 | MFCS | Timed Network Games with Clocks. | Guy Avni, Shibashis Guha, Orna Kupferman |
| 2018 | MFCS | Spanning-Tree Games. | Dan Hefetz, Orna Kupferman, Amir Lellouche, Gal Vardi |
| 2017 | CAV | Quantitative Assume Guarantee Synthesis. | Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, Yaron Velner |
| 2017 | CONCUR | Flow Logic. | Orna Kupferman, Gal Vardi |
| 2017 | IJCAI | An Abstraction-Refinement Methodology for Reasoning about Network Games. | Guy Avni, Shibashis Guha, Orna Kupferman |
| 2017 | MFCS | Timed Network Games. | Guy Avni, Shibashis Guha, Orna Kupferman |
| 2017 | STOC | Examining classical graph-theory problems from the viewpoint of formal-verification methods (invited talk). | Orna Kupferman |
| 2017 | TACAS | Hierarchical Network Formation Games. | Orna Kupferman, Tami Tamir |
| 2016 | CONCUR | Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis. | Shaull Almagor, Orna Kupferman, Yaron Velner |
| 2016 | CSL | High-Quality Synthesis Against Stochastic Environments. | Shaull Almagor, Orna Kupferman |
| 2016 | CSR | On High-Quality Synthesis. | Orna Kupferman |
| 2016 | LATA | On the Capacity of Capacitated Automata. | Orna Kupferman, Sarai Sheinvald |
| 2016 | MFCS | Eulerian Paths with Regular Constraints. | Orna Kupferman, Gal Vardi |
| 2016 | SAGT | Dynamic Resource Allocation Games. | Guy Avni, Thomas A. Henzinger, Orna Kupferman |
| 2015 | ATVA | Spanning the Spectrum from Safety to Liveness. | Rachel Faran, Orna Kupferman |
| 2015 | CONCUR | Repairing Multi-Player Games. | Shaull Almagor, Guy Avni, Orna Kupferman |
| 2015 | CSL | On Relative and Probabilistic Finite Counterability. | Orna Kupferman, Gal Vardi |
| 2015 | MFCS | Stochastization of Weighted Automata. | Guy Avni, Orna Kupferman |
| 2014 | ATVA | A Game-Theoretic Approach to Simulation of Data-Parameterized Systems. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2014 | CADE | From Reachability to Temporal Specifications in Cost-Sharing Games. | Guy Avni, Orna Kupferman, Tami Tamir |
| 2014 | CONCUR | Synthesis from Component Libraries with Costs. | Guy Avni, Orna Kupferman |
| 2014 | EUMAS | Synthesis with Rational Environments. | Orna Kupferman, Giuseppe Perelli, Moshe Y. Vardi |
| 2014 | FOSSACS | Latticed-LTL Synthesis in the Presence of Noisy Inputs. | Shaull Almagor, Orna Kupferman |
| 2014 | FOSSACS | Network-Formation Games with Regular Objectives. | Guy Avni, Orna Kupferman, Tami Tamir |
| 2014 | TACAS | Discounting in LTL. | Shaull Almagor, Udi Boker, Orna Kupferman |
| 2014 | TACAS | Variations on Safety. | Orna Kupferman |
| 2013 | ATVA | A Framework for Ranking Vacuity Results. | Shoham Ben-David, Orna Kupferman |
| 2013 | ATVA | An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2013 | ATVA | Weighted Safety. | Sigal Weiner, Matan Hasson, Orna Kupferman, Eyal Pery, Zohar Shevach |
| 2013 | CAV | Automatic Generation of Quality Specifications. | Shaull Almagor, Guy Avni, Orna Kupferman |
| 2013 | FOSSACS | Parameterized Weighted Containment. | Guy Avni, Orna Kupferman |
| 2013 | ICALP | Formalizing and Reasoning about Quality. | Shaull Almagor, Udi Boker, Orna Kupferman |
| 2013 | ICALP | Nondeterminism in the Presence of a Diverse or Unknown Future. | Udi Boker, Denis Kuperberg, Orna Kupferman, Michal Skrzypczak |
| 2013 | MFCS | Prime Languages. | Orna Kupferman, Jonathan Mosheiff |
| 2012 | ATVA | Model Checking Systems and Specifications with Parameterized Atomic Propositions. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2012 | ATVA | Approximating Deterministic Lattice Automata. | Shulamit Halamish, Orna Kupferman |
| 2012 | CONCUR | Making Weighted Containment Feasible: A Heuristic Based on Simulation and Abstraction. | Guy Avni, Orna Kupferman |
| 2012 | SOFSEM | Recent Challenges and Ideas in Temporal Synthesis. | Orna Kupferman |
| 2011 | ATVA | What's Decidable about Weighted Automata? | Shaull Almagor, Udi Boker, Orna Kupferman |
| 2011 | ATVA | Max and Sum Semantics for Alternating Weighted Automata. | Shaull Almagor, Orna Kupferman |
| 2011 | ATVA | Formal Analysis of Online Algorithms. | Benjamin Aminof, Orna Kupferman, Robby Lampert |
| 2011 | CSL | Unifying Bchi Complementation Constructions. | Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, Thomas Wilke |
| 2011 | FOSSACS | Co-Bching Them All. | Udi Boker, Orna Kupferman |
| 2011 | FOSSACS | Minimizing Deterministic Lattice Automata. | Shulamit Halamish, Orna Kupferman |
| 2011 | LICS | Rigorous Approximated Determinization of Weighted Automata. | Benjamin Aminof, Orna Kupferman, Robby Lampert |
| 2011 | LICS | Temporal Specifications with Accumulative Values. | Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman |
| 2011 | STACS | Temporal Synthesis for Bounded Systems and Environments. | Orna Kupferman, Yoad Lustig, Moshe Y. Vardi, Mihalis Yannakakis |
| 2011 | SAS | An Abstraction-Refinement Framework for Trigger Querying. | Guy Avni, Orna Kupferman |
| 2010 | ATVA | Promptness in | Shaull Almagor, Yoram Hirshfeld, Orna Kupferman |
| 2010 | ICALP | Alternation Removal in Bchi Automata. | Udi Boker, Orna Kupferman, Adin Rosenberg |
| 2010 | LATA | Variable Automata over Infinite Alphabets. | Orna Grumberg, Orna Kupferman, Sarai Sheinvald |
| 2010 | LPAR | Coping with Selfish On-Going Behaviors. | Orna Kupferman, Tami Tamir |
| 2010 | LPAR | Synthesis of Trigger Properties. | Orna Kupferman, Moshe Y. Vardi |
| 2010 | TACAS | Rational Synthesis. | Dana Fisman, Orna Kupferman, Yoad Lustig |
| 2010 | VMCAI | Improved Model Checking of Hierarchical Systems. | Benjamin Aminof, Orna Kupferman, Aniello Murano |
| 2009 | FOSSACS | Lower Bounds on Witnesses for Nonemptiness of Universal Co-Bchi Automata. | Orna Kupferman, Nir Piterman |
| 2009 | LICS | Co-ing Bchi Made Tight and Useful. | Udi Boker, Orna Kupferman |
| 2009 | SODA | Reasoning about online algorithms with weighted automata. | Benjamin Aminof, Orna Kupferman, Robby Lampert |
| 2008 | FMCAD | A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance. | Orna Kupferman, Wenchao Li, Sanjit A. Seshia |
| 2008 | LPAR | On the Relative Succinctness of Nondeterministic Bchi and co-Bchi Word Automata. | Benjamin Aminof, Orna Kupferman, Omer Lev |
| 2008 | TACAS | On Verifying Fault Tolerance of Distributed Protocols. | Dana Fisman, Orna Kupferman, Yoad Lustig |
| 2008 | TAP | Vacuity in Testing. | Thomas Ball, Orna Kupferman |
| 2008 | VMCAI | Multi-valued Logics, Automata, Simulations, and Games. | Orna Kupferman, Yoad Lustig |
| 2007 | ATVA | Latticed Simulation Relations and Games. | Orna Kupferman, Yoad Lustig |
| 2007 | CAV | Leaping Loops in the Presence of Abstraction. | Thomas Ball, Orna Kupferman, Mooly Sagiv |
| 2007 | CAV | From Liveness to Promptness. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2007 | CSL | Tightening the Exchange Rates Between Automata. | Orna Kupferman |
| 2007 | FMCAD | What Triggers a Behavior? | Orna Kupferman, Yoad Lustig |
| 2007 | VMCAI | Better Under-Approximation of Programs by Hiding Variables. | Thomas Ball, Orna Kupferman |
| 2007 | VMCAI | Lattice Automata. | Orna Kupferman, Yoad Lustig |
| 2006 | ATVA | On the Succinctness of Nondeterminism. | Benjamin Aminof, Orna Kupferman |
| 2006 | ATVA | On the Construction of Fine Automata for Safety Properties. | Orna Kupferman, Robby Lampert |
| 2006 | CAV | Safraless Compositional Synthesis. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2006 | CONCUR | Sanity Checks in Formal Verification. | Orna Kupferman |
| 2006 | CONCUR | Finding Shortest Witnesses to the Nonemptiness of Automata on Infinite Words. | Orna Kupferman, Sarai Sheinvald-Faragy |
| 2006 | LICS | An Abstraction-Refinement Framework for Multi-Agent Systems. | Thomas Ball, Orna Kupferman |
| 2006 | LICS | Avoiding Determinization. | Orna Kupferman |
| 2006 | LICS | Memoryful Branching-Time Logic. | Orna Kupferman, Moshe Y. Vardi |
| 2006 | LPAR | On Locally Checkable Properties. | Orna Kupferman, Yoad Lustig, Moshe Y. Vardi |
| 2005 | CAV | Abstraction for Falsification. | Thomas Ball, Orna Kupferman, Greta Yorsh |
| 2005 | FOCS | Safraless Decision Procedures. | Orna Kupferman, Moshe Y. Vardi |
| 2005 | TACAS | Complementation Constructions for Nondeterministic Automata on Infinite Words. | Orna Kupferman, Moshe Y. Vardi |
| 2004 | ATVA | Bchi Complementation Made Tighter. | Ehud Friedgut, Orna Kupferman, Moshe Y. Vardi |
| 2004 | ATVA | Typeness for omega-Regular Automata. | Orna Kupferman, Gila Morgenstern, Aniello Murano |
| 2004 | LPAR | Reasoning About Systems with Transition Fairness. | Benjamin Aminof, Thomas Ball, Orna Kupferman |
| 2004 | STACS | A Measured Collapse of the Modal -Calculus Alternation Hierarchy. | Doron Bustan, Orna Kupferman, Moshe Y. Vardi |
| 2004 | TACAS | From Complementation to Certification. | Orna Kupferman, Moshe Y. Vardi |
| 2003 | ICALP | Π | Orna Kupferman, Moshe Y. Vardi |
| 2003 | TACAS | Resets vs. Aborts in Linear Temporal Logic. | Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi |
| 2003 | TACAS | On the Universal and Existential Fragments of the -Calculus. | Thomas A. Henzinger, Orna Kupferman, Rupak Majumdar |
| 2002 | CADE | The Complexity of the Graded µ-Calculus. | Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi |
| 2002 | CAV | Model Checking Linear Properties of Prefix-Recognizable Systems. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2002 | CSL | Trading Probability for Fairness. | Marcin Jurdzinski, Orna Kupferman, Thomas A. Henzinger |
| 2002 | ICALP | Synthesis of Uninitialized Systems. | Thomas A. Henzinger, Sriram C. Krishnan, Orna Kupferman, Freddy Y. C. Mang |
| 2002 | LPAR | Pushdown Specifications. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2002 | MFCS | An Improved Algorithm for the Membership Problem for Extended Regular Expressions. | Orna Kupferman, Sharon Zuhovitzky |
| 2001 | CAV | A Practical Approach to Coverage in Model Checking. | Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi |
| 2001 | CONCUR | Extended Temporal Logic Revisited. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2001 | FOSSACS | On the Complexity of Parity Word Automata. | Valerie King, Orna Kupferman, Moshe Y. Vardi |
| 2001 | LICS | Synthesizing Distributed Systems. | Orna Kupferman, Moshe Y. Vardi |
| 2001 | LPAR | On Bounded Specifications. | Orna Kupferman, Moshe Y. Vardi |
| 2001 | TACAS | Coverage Metrics for Temporal Logic Model Checking. | Hana Chockler, Orna Kupferman, Moshe Y. Vardi |
| 2000 | CAV | An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. | Orna Kupferman, Moshe Y. Vardi |
| 2000 | CONCUR | Open Systems in Reactive Environments: Control and Synthesis. | Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, Moshe Y. Vardi |
| 2000 | MFCS | µ-Calculus Synthesis. | Orna Kupferman, Moshe Y. Vardi |
| 1999 | CAV | Model Checking of Safety Properties. | Orna Kupferman, Moshe Y. Vardi |
| 1999 | CONCUR | Robust Satisfaction. | Orna Kupferman, Moshe Y. Vardi |
| 1999 | STACS | The Weakness of Self-Complementation. | Orna Kupferman, Moshe Y. Vardi |
| 1998 | CAV | From | Thomas A. Henzinger, Orna Kupferman, Shaz Qadeer |
| 1998 | CONCUR | Alternating Refinement Relations. | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi |
| 1998 | FOCS | Concurrent Reachability Games. | Luca de Alfaro, Thomas A. Henzinger, Orna Kupferman |
| 1998 | LICS | Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time. | Orna Kupferman, Moshe Y. Vardi |
| 1998 | STOC | Weak Alternating Automata and Tree Automata Emptiness. | Orna Kupferman, Moshe Y. Vardi |
| 1997 | CAV | Module Checking Revisited. | Orna Kupferman, Moshe Y. Vardi |
| 1997 | CONCUR | On the Complexity of Verifying Concurrent Transition Systems. | David Harel, Orna Kupferman, Moshe Y. Vardi |
| 1997 | CONCUR | Fair Simulation. | Thomas A. Henzinger, Orna Kupferman, Sriram K. Rajamani |
| 1997 | CSL | Existence of Reduction Hierarchies. | Orna Kupferman, Robert P. Kurshan, Mihalis Yannakakis |
| 1997 | FOCS | Alternating-time Temporal Logic. | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman |
| 1996 | CAV | Module Checking. | Orna Kupferman, Moshe Y. Vardi |
| 1996 | CAV | Verification of Fair Transisiton Systems. | Orna Kupferman, Moshe Y. Vardi |
| 1996 | CONCUR | A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. | Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi |
| 1996 | LICS | Relating Word and Tree Automata. | Orna Kupferman, Shmuel Safra, Moshe Y. Vardi |
| 1995 | CAV | Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. | Orna Kupferman |
| 1995 | CONCUR | On the Complexity of Branching Modular Model Checking (Extended Abstract). | Orna Kupferman, Moshe Y. Vardi |
| 1995 | LICS | Once and For All | Orna Kupferman, Amir Pnueli |