| 2026 | CAV | Fast Obligation Translation and Synthesis. | Alexandre Duret-Lutz, Giuseppe De Giacomo, Marcin Jurdzinski, Nir Piterman, Moshe Y. Vardi, Shufang Zhu |
| 2026 | CP | Computing Short SAT Implicants via Ising/QUBO Encodings. | Giuseppe Spallitta, Leonardo Dueas-Osorio, Moshe Y. Vardi |
| 2026 | KR | On-the-fly LTLf Synthesis under Partial Observability. | Nadav Alon, Supratik Chakraborty, Alexandre Duret-Lutz, Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi, Shufang Zhu |
| 2025 | AAAI | LTLf Synthesis Under Unreliable Input. | Christian Hagemeier, Giuseppe De Giacomo, Moshe Y. Vardi |
| 2025 | IJCAI | LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces. | Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi |
| 2025 | NeSy | Understanding Boolean Function Learnability on Deep Neural Networks: PAC Learning Meets Neurosymbolic Models. | Mrcio Nicolau, Anderson R. Tavares, Zhiwei Zhang, Pedro H. C. Avelar, Joo Marcos Flach, Lus C. Lamb, Moshe Y. Vardi |
| 2024 | CAV | The MoXI Model Exchange Tool Suite. | Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier |
| 2024 | CAV | Dynamic Programming for Symbolic Boolean Realizability and Synthesis. | Yi Lin, Lucas Martinelli Tabajara, Moshe Y. Vardi |
| 2024 | CSL | Logical Algorithmics: From Theory to Practice (Invited Talk). | Moshe Y. Vardi |
| 2024 | IJCAI | The Trembling-Hand Problem for LTLf Planning. | Pian Yu, Shufang Zhu, Giuseppe De Giacomo, Marta Kwiatkowska, Moshe Y. Vardi |
| 2024 | ICRA | Accelerating Long-Horizon Planning with Affordance-Directed Dynamic Grounding of Abstract Strategies. | Khen Elimelech, Zachary Kingston, Wil Thomason, Moshe Y. Vardi, Lydia E. Kavraki |
| 2024 | ICRA | Stochastic Games for Interactive Manipulation Domains. | Karan Muvvala, Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi |
| 2024 | KR | Probabilistic Synthesis and Verification for LTL on Finite Traces. | Benjamin Aminof, Linus Cooper, Sasha Rubin, Moshe Y. Vardi, Florian Zuleger |
| 2023 | ATVA | Model Checking Strategies from Synthesis over Finite Traces. | Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi, Andrew M. Wells |
| 2023 | CONCUR | Singly Exponential Translation of Alternating Weak Bchi Automata to Unambiguous Bchi Automata. | Yong Li, Sven Schewe, Moshe Y. Vardi |
| 2023 | FMCAD | Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. | Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi |
| 2023 | IJCAI | Multi-Agent Systems with Quantitative Satisficing Goals. | Senthil Rajasekaran, Suguman Bansal, Moshe Y. Vardi |
| 2023 | IJCAI | Solving Quantum-Inspired Perfect Matching Problems via Tutte-Theorem-Based Hybrid Boolean Constraints. | Moshe Y. Vardi, Zhiwei Zhang |
| 2023 | ICRA | Extracting generalizable skills from a single plan execution using abstraction-critical state detection. | Khen Elimelech, Lydia E. Kavraki, Moshe Y. Vardi |
| 2022 | AAAI | Synthesis from Satisficing and Temporal Goals. | Suguman Bansal, Lydia E. Kavraki, Moshe Y. Vardi, Andrew M. Wells |
| 2022 | AAAI | Constraint-Driven Explanations for Black-Box ML Models. | Aditya A. Shrotri, Nina Narodytska, Alexey Ignatiev, Kuldeep S. Meel, Joo Marques-Silva, Moshe Y. Vardi |
| 2022 | CAV | Divide-and-Conquer Determinization of Bchi Automata Based on SCC Decomposition. | Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, Lijun Zhang |
| 2022 | IJCAI | DPSampler: Exact Weighted Sampling Using Dynamic Programming. | Jeffrey M. Dudek, Aditya A. Shrotri, Moshe Y. Vardi |
| 2022 | IJCAI | LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work. | Giuseppe De Giacomo, Marco Favorito, Jianwen Li, Moshe Y. Vardi, Shengping Xiao, Shufang Zhu |
| 2022 | ICSoft | Program Verification: A 70+-Year History. | Moshe Y. Vardi |
| 2022 | ISRR | Efficient Task Planning Using Abstract Skills and Dynamic Road Map Matching. | Khen Elimelech, Lydia E. Kavraki, Moshe Y. Vardi |
| 2022 | KR | Public and Private Affairs in Strategic Reasoning. | Nathanal Fijalkow, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi |
| 2022 | KR | Verification and Realizability in Finite-Horizon Multiagent Systems. | Senthil Rajasekaran, Moshe Y. Vardi |
| 2021 | AAAI | On Continuous Local BDD-Based Search for Hybrid SAT Solving. | Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang |
| 2021 | AAAI | On-the-fly Synthesis for LTL over Finite Traces. | Shengping Xiao, Jianwen Li, Shufang Zhu, Yingying Shi, Geguang Pu, Moshe Y. Vardi |
| 2021 | ATVA | Linear Temporal Logic - From Infinite to Finite Horizon. | Lucas M. Tabajara, Moshe Y. Vardi |
| 2021 | CAV | Adapting Behaviors via Reactive Synthesis. | Gal Amram, Suguman Bansal, Dror Fried, Lucas Martinelli Tabajara, Moshe Y. Vardi, Gera Weiss |
| 2021 | FM | Congruence Relations for Bchi Automata. | Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang |
| 2021 | IJCAI | Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis. | Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, Shufang Zhu |
| 2021 | IJCAI | Synthesizing Good-Enough Strategies for LTLf Specifications. | Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang |
| 2021 | ICRA | Finite-Horizon Synthesis for Probabilistic Manipulation Domains. | Andrew M. Wells, Zachary Kingston, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi |
| 2021 | SIGCSE | Deep Tech Ethics: An Approach to Teaching Social Justice in Computer Science. | Rodrigo Ferreira, Moshe Y. Vardi |
| 2020 | AAAI | Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. | Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi |
| 2020 | AAAI | ADDMC: Weighted Model Counting with Algebraic Decision Diagrams. | Jeffrey M. Dudek, Vu Phan, Moshe Y. Vardi |
| 2020 | AAAI | FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints. | Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Y. Vardi, Zhiwei Zhang |
| 2020 | AAAI | LTLƒ Synthesis with Fairness and Stability Assumptions. | Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi |
| 2020 | CP | DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees. | Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi |
| 2020 | FMCAD | Runtime Verification on FPGAs with LTLf Specifications. | Tommy Tracy II, Lucas M. Tabajara, Moshe Y. Vardi, Kevin Skadron |
| 2020 | ICCAD | On Uniformly Sampling Traces of a Transition System. | Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi |
| 2020 | IJCAI | Assume-Guarantee Synthesis for Prompt Linear Temporal Logic. | Nathanal Fijalkow, Bastien Maubert, Aniello Murano, Moshe Y. Vardi |
| 2020 | IJCAI | Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective. | Lus C. Lamb, Artur S. d'Avila Garcez, Marco Gori, Marcelo O. R. Prates, Pedro H. C. Avelar, Moshe Y. Vardi |
| 2020 | KR | Two-Stage Technique for LTLf Synthesis Under LTL Assumptions. | Giuseppe De Giacomo, Antonio Di Stasio, Moshe Y. Vardi, Shufang Zhu |
| 2019 | AAAI | Unbounded Orchestrations of Transducers for Manufacturing. | Natasha Alechina, Toms Brzdil, Giuseppe De Giacomo, Paolo Felli, Brian Logan, Moshe Y. Vardi |
| 2019 | AAAI | On the Hardness of Probabilistic Inference Relaxations. | Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |
| 2019 | AAAI | Labor Division with Movable Walls: Composing Executable Specifications with Machine Learning and Search (Blue Sky Idea). | David Harel, Assaf Marron, Ariel Rosenfeld, Moshe Y. Vardi, Gera Weiss |
| 2019 | AAAI | SAT-Based Explicit LTLf Satisfiability Checking. | Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi |
| 2019 | AAAI | Learning to Solve NP-Complete Problems: A Graph Neural Network for Decision TSP. | Marcelo O. R. Prates, Pedro H. C. Avelar, Henrique Lemos, Lus C. Lamb, Moshe Y. Vardi |
| 2019 | CAV | Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion. | Suguman Bansal, Moshe Y. Vardi |
| 2019 | CAV | Satisfiability Checking for Mission-Time LTL. | Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier |
| 2019 | CP | On Symbolic Approaches for Computing the Matrix Permanent. | Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi |
| 2019 | IJCAI | Not All FPRASs are Equal: Demystifying FPRASs for DNF-Counting (Extended Abstract). | Kuldeep S. Meel, Aditya A. Shrotri, Moshe Y. Vardi |
| 2019 | IJCAI | Partitioning Techniques in LTLf Synthesis. | Lucas Martinelli Tabajara, Moshe Y. Vardi |
| 2019 | ICRA | Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks. | Keliang He, Andrew M. Wells, Lydia E. Kavraki, Moshe Y. Vardi |
| 2018 | AAAI | Synthesis of Orchestrations of Transducers for Manufacturing. | Giuseppe De Giacomo, Moshe Y. Vardi, Paolo Felli, Natasha Alechina, Brian Logan |
| 2018 | CAV | Automata vs Linear-Programming Discounted-Sum Inclusion. | Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi |
| 2018 | CAV | SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability. | Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi |
| 2018 | CONCUR | The Siren Song of Temporal Synthesis (Invited Talk). | Moshe Y. Vardi |
| 2018 | FMCAD | Functional Synthesis via Input-Output Separation. | Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi |
| 2018 | FOSSACS | Comparator Automata in Quantitative Verification. | Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi |
| 2018 | LICS | Sequential Relational Decomposition. | Dror Fried, Axel Legay, Jol Ouaknine, Moshe Y. Vardi |
| 2017 | AAAI | Counting-Based Reliability Estimation for Power-Transmission Grids. | Leonardo Dueas-Osorio, Kuldeep S. Meel, Roger Paredes, Moshe Y. Vardi |
| 2017 | FMCAD | Factored boolean functional synthesis. | Lucas M. Tabajara, Moshe Y. Vardi |
| 2017 | ICCAD | Safety model checking with complementary approximations. | Jianwen Li, Shufang Zhu, Yueling Zhang, Geguang Pu, Moshe Y. Vardi |
| 2017 | IJCAI | The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas. | Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi |
| 2017 | IJCAI | Symbolic LTLf Synthesis. | Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi |
| 2017 | IROS | Reactive synthesis for finite tasks under resource constraints. | Keliang He, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi |
| 2017 | LICS | The homomorphism problem for regular graph patterns. | Miguel Romero, Pablo Barcel, Moshe Y. Vardi |
| 2017 | LICS | Strategy logic with imperfect information. | Raphal Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi |
| 2017 | PODS | 2017 ACM PODS Alberto O. Mendelzon Test-of-Time Award. | Leonid Libkin, Moshe Y. Vardi |
| 2016 | AAAI | Approximate Probabilistic Inference via Word-Level Counting. | Supratik Chakraborty, Kuldeep S. Meel, Rakesh Mistry, Moshe Y. Vardi |
| 2016 | AAAI | Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. | Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, Sharad Malik |
| 2016 | CAV | BDD-Based Boolean Functional Synthesis. | Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi |
| 2016 | IJCAI | Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls. | Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |
| 2016 | IJCAI | Combining the k-CNF and XOR Phase-Transitions. | Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi |
| 2016 | IJCAI | LTL | Giuseppe De Giacomo, Moshe Y. Vardi |
| 2016 | KR | Regular Open APIs. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2016 | PODS | A Theory of Regular Queries. | Moshe Y. Vardi |
| 2015 | AAAI | This Time the Robot Settles for a Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction. | Morteza Lahijanian, Shaull Almagor, Dror Fried, Lydia E. Kavraki, Moshe Y. Vardi |
| 2015 | ICALP | The Complexity of Synthesis from Probabilistic Components. | Krishnendu Chatterjee, Laurent Doyen, Moshe Y. Vardi |
| 2015 | ICDT | Regular Queries on Graph Databases. | Juan L. Reutter, Miguel Romero, Moshe Y. Vardi |
| 2015 | IJCAI | From Weighted to Unweighted Model Counting. | Supratik Chakraborty, Dror Fried, Kuldeep S. Meel, Moshe Y. Vardi |
| 2015 | IJCAI | Synthesis for LTL and LDL on Finite Traces. | Giuseppe De Giacomo, Moshe Y. Vardi |
| 2015 | ICRA | Towards manipulation planning with temporal logic specifications. | Keliang He, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi |
| 2014 | AAAI | Distribution-Aware Sampling and Weighted Model Counting for SAT. | Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi |
| 2014 | DAC | Validation of SoC Firmware-Hardware Flows: Challenges and Solution Directions. | Yael Abarbanel, Eli Singerman, Moshe Y. Vardi |
| 2014 | DAC | Balancing Scalability and Uniformity in SAT Witness Generator. | Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |
| 2014 | ECAI | LTLf Satisfiability Checking. | Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, Jifeng He |
| 2014 | EUMAS | Synthesis with Rational Environments. | Orna Kupferman, Giuseppe Perelli, Moshe Y. Vardi |
| 2014 | FOSSACS | The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. | Krishnendu Chatterjee, Laurent Doyen, Sumit Nain, Moshe Y. Vardi |
| 2014 | ICRA | A sampling-based strategy planner for nondeterministic hybrid systems. | Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi |
| 2014 | MEMOCODE | Assertion-based flow monitoring of SystemC models. | Sonali Dutta, Moshe Y. Vardi |
| 2014 | MEMOCODE | From visual to logical formalisms for SoC validation. | Ranan Fraer, Doron Keren, Zurab Khasidashvili, Alexander Novakovsky, Avi Puder, Eli Singerman, Eran Talmor, Moshe Y. Vardi, Jin Yang |
| 2014 | PODS | Does query evaluation tractability help query containment? | Pablo Barcel, Miguel Romero, Moshe Y. Vardi |
| 2013 | CAV | A Scalable and Nearly Uniform Generator of SAT Witnesses. | Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |
| 2013 | CP | A Scalable Approximate Model Counter. | Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi |
| 2013 | FMCAD | CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models. | Sonali Dutta, Moshe Y. Vardi, Deian Tabakov |
| 2013 | IJCAI | Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. | Giuseppe De Giacomo, Moshe Y. Vardi |
| 2013 | LICS | Regular Real Analysis. | Swarat Chaudhuri, Sriram Sankaranarayanan, Moshe Y. Vardi |
| 2013 | LICS | Solving Partial-Information Stochastic Parity Games. | Sumit Nain, Moshe Y. Vardi |
| 2013 | PODS | Semantic acyclicity on graph databases. | Pablo Barcel Baeza, Miguel Romero, Moshe Y. Vardi |
| 2012 | CAV | Bma: Visual Tool for Modeling and Analyzing Biological Networks. | David Benqu, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex S. Taylor, Moshe Y. Vardi |
| 2012 | CONCUR | What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic. | Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi |
| 2012 | FOSSACS | Synthesizing Probabilistic Composers. | Sumit Nain, Moshe Y. Vardi |
| 2011 | CAV | Temporal Property Verification as a Program Analysis Task. | Byron Cook, Eric Koskinen, Moshe Y. Vardi |
| 2011 | CONCUR | Dynamic Reactive Modules. | Jasmin Fisher, Thomas A. Henzinger, Dejan Nickovic, Nir Piterman, Anmol V. Singh, Moshe Y. Vardi |
| 2011 | CSL | Unifying Bchi Complementation Constructions. | Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, Thomas Wilke |
| 2011 | CSL | Synthesis from Probabilistic Components. | Yoad Lustig, Sumit Nain, Moshe Y. Vardi |
| 2011 | CSL | Branching vs. Linear Time: Semantical Perspective. | Moshe Y. Vardi |
| 2011 | FM | The Only Way Is Up. | Jasmin Fisher, Nir Piterman, Moshe Y. Vardi |
| 2011 | FM | A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. | Kristin Y. Rozier, Moshe Y. Vardi |
| 2011 | ICDT | Simplifying schema mappings. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2011 | STACS | Temporal Synthesis for Bounded Systems and Environments. | Orna Kupferman, Yoad Lustig, Moshe Y. Vardi, Mihalis Yannakakis |
| 2010 | AAAI | Node Selection Query Languages for Trees. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2010 | CP | Constraints, Graphs, Algebra, Logic, and Complexity. | Moshe Y. Vardi |
| 2010 | ICRA | Sampling-based motion planning with temporal goals. | Amit Bhatia, Lydia E. Kavraki, Moshe Y. Vardi |
| 2010 | LPAR | Synthesis of Trigger Properties. | Orna Kupferman, Moshe Y. Vardi |
| 2010 | LPAR | Relentful Strategic Reasoning in Alternating-Time Temporal Logic. | Fabio Mogavero, Aniello Murano, Moshe Y. Vardi |
| 2010 | MEMOCODE | Monitoring temporal SystemC properties. | Deian Tabakov, Moshe Y. Vardi |
| 2009 | FOSSACS | Synthesis from Component Libraries. | Yoad Lustig, Moshe Y. Vardi |
| 2009 | LICS | Trace Semantics is Fully Abstract. | Sumit Nain, Moshe Y. Vardi |
| 2008 | FMCAD | A Temporal Language for SystemC. | Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman |
| 2008 | ICALP | Open Implication. | Karin Greimel, Roderick Bloem, Barbara Jobstmann, Moshe Y. Vardi |
| 2008 | ICRA | Impact of workspace decompositions on discrete search leading continuous exploration (DSLX) motion planning. | Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
| 2007 | ASPDAC | Deeper Bound in BMC by Combining Constant Propagation and Abstraction. | Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Y. Vardi, Yakir Vizel, Yael Zbar |
| 2007 | ATVA | Branching vs. Linear Time: Semantical Perspective. | Sumit Nain, Moshe Y. Vardi |
| 2007 | CAV | From Liveness to Promptness. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2007 | CAV | Hybrid Systems: From Verification to Falsification. | Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
| 2007 | CONCUR | Pushdown Module Checking with Imperfect Information. | Benjamin Aminof, Aniello Murano, Moshe Y. Vardi |
| 2007 | CP | An Analysis of Slow Convergence in Interval Propagation. | Lucas Bordeaux, Youssef Hamadi, Moshe Y. Vardi |
| 2007 | DAC | Formal Techniques for SystemC Verification; Position Paper. | Moshe Y. Vardi |
| 2007 | DATE | Interactive presentation: PowerQuest: trace driven data mining for power optimization. | Pietro Babighian, Gila Kamhi, Moshe Y. Vardi |
| 2007 | ICRA | A Motion Planner for a Hybrid Robotic System with Kinodynamic Constraints. | Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
| 2007 | LATA | Model Checking Buechi Specifications. | Deian Tabakov, Moshe Y. Vardi |
| 2007 | POPL | Proving that programs eventually do something good. | Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi |
| 2006 | CAV | Safraless Compositional Synthesis. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2006 | ICALP | The Complexity of Enriched | Piero A. Bonatti, Carsten Lutz, Aniello Murano, Moshe Y. Vardi |
| 2006 | LICS | Memoryful Branching-Time Logic. | Orna Kupferman, Moshe Y. Vardi |
| 2006 | LICS | Fixed-Parameter Hierarchies inside PSPACE. | Guoqiang Pan, Moshe Y. Vardi |
| 2006 | LPAR | On Locally Checkable Properties. | Orna Kupferman, Yoad Lustig, Moshe Y. Vardi |
| 2006 | SIGCSE | Automata theory: its relevance to computer science students and course contents. | Michal Armoni, Susan H. Rodger, Moshe Y. Vardi, Rakesh M. Verma |
| 2006 | SIGCSE | educational response to offshore outsourcing. | William Aspray, A. Frank Mayadas, Moshe Y. Vardi, Stuart H. Zweben |
| 2005 | CAV | Formal Verification of Backward Compatibility of Microcode. | Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Lenore D. Zuck |
| 2005 | CAV | Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
| 2005 | FOCS | Safraless Decision Procedures. | Orna Kupferman, Moshe Y. Vardi |
| 2005 | ICCAD | Efficient LTL compilation for SAT-based model checking. | Roy Armoni, Sergey Egorov, Ranan Fraer, Dmitry Korchemny, Moshe Y. Vardi |
| 2005 | ICDT | View-Based Query Processing: On the Relationship Between Rewriting, Answering and Losslessness. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2005 | ICDT | Model Checking for Database Theoreticians. | Moshe Y. Vardi |
| 2005 | LPAR | Treewidth in Verification: Local vs. Global. | Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi |
| 2005 | LPAR | Experimental Evaluation of Classical Automata Constructions. | Deian Tabakov, Moshe Y. Vardi |
| 2004 | ATVA | Bchi Complementation Made Tighter. | Ehud Friedgut, Orna Kupferman, Moshe Y. Vardi |
| 2004 | CAV | Verifying omega-Regular Properties of Markov Chains. | Doron Bustan, Sasha Rubin, Moshe Y. Vardi |
| 2004 | CAV | Global Model-Checking of Infinite-State Systems. | Nir Piterman, Moshe Y. Vardi |
| 2004 | CAV | GSTE Is Partitioned Model Checking. | Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi |
| 2004 | CP | Constraint Propagation as a Proof System. | Albert Atserias, Phokion G. Kolaitis, Moshe Y. Vardi |
| 2004 | CP | Symbolic Decision Procedures for QBF. | Guoqiang Pan, Moshe Y. Vardi |
| 2004 | EDBT | Projection Pushing Revisited. | Benjamin J. McMahan, Guoqiang Pan, Patrick Porter, Moshe Y. Vardi |
| 2004 | STACS | A Measured Collapse of the Modal -Calculus Alternation Hierarchy. | Doron Bustan, Orna Kupferman, Moshe Y. Vardi |
| 2003 | CADE | Optimizing a BDD-Based Modal Solver. | Guoqiang Pan, Moshe Y. Vardi |
| 2003 | CAV | Enhanced Vacuity Detection in Linear Temporal Logic. | Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi |
| 2003 | ICALP | Π | Orna Kupferman, Moshe Y. Vardi |
| 2003 | ICALP | Logic and Automata: A Match Made in Heaven. | Moshe Y. Vardi |
| 2003 | ICDT | Decidable Containment of Recursive Queries. | Diego Calvanese, Giuseppe De Giacomo, Moshe Y. Vardi |
| 2003 | IJCAI | Automated Verification: Graphs, Logic, and Automata. | Moshe Y. Vardi |
| 2003 | LICS | Homomorphism Closed vs. Existential Positive. | Toms Feder, Moshe Y. Vardi |
| 2003 | LICS | The Planning Spectrum - One, Two, Three, Infinity. | Marco Pistore, Moshe Y. Vardi |
| 2003 | LICS | Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems. | Nir Piterman, Moshe Y. Vardi |
| 2003 | PODS | View-based query containment. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2002 | CADE | The Complexity of the Graded µ-Calculus. | Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi |
| 2002 | CADE | BDD-Based Decision Procedures for K. | Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi |
| 2002 | CAV | Model Checking Linear Properties of Prefix-Recognizable Systems. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2002 | CP | Constraint Satisfaction, Bounded Treewidth, and Finite-Variable Logics. | Vctor Dalmau, Phokion G. Kolaitis, Moshe Y. Vardi |
| 2002 | JELIA | Alternation. | Moshe Y. Vardi |
| 2002 | KR | Eliminating Incoherence from Subjective Estimates of Chance. | Randy Batsell, Lyle Brenner, Daniel N. Osherson, Spyros Tsavachidis, Moshe Y. Vardi |
| 2002 | KR | Reasoning about Actions and Planning in LTL Action Theories. | Diego Calvanese, Giuseppe De Giacomo, Moshe Y. Vardi |
| 2002 | LPAR | Pushdown Specifications. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2002 | PODS | Lossless Regular Views. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2001 | CADE | The Hybrid µ-Calculus. | Ulrike Sattler, Moshe Y. Vardi |
| 2001 | CAV | A Practical Approach to Coverage in Model Checking. | Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi |
| 2001 | CAV | Benefits of Bounded Model Checking at an Industrial Setting. | Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi |
| 2001 | CONCUR | Extended Temporal Logic Revisited. | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
| 2001 | CP | Random 3-SAT and BDDs: The Plot Thickens Further. | Alfonso San Miguel Aguirre, 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 | MFCS | From Bidirectionality to Alternation. | Nir Piterman, Moshe Y. Vardi |
| 2000 | AAAI | A Game-Theoretic Approach to Constraint Satisfaction. | Phokion G. Kolaitis, Moshe Y. Vardi |
| 2000 | CAV | Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. | Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix |
| 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 | CP | Random 3-SAT: The Plot Thickens. | Cristian Coarfa, Demetrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika Subramanian, Moshe Y. Vardi |
| 2000 | CSL | Automated Verification = Graphs, Automata, and Logic. | Moshe Y. Vardi |
| 2000 | ICDE | Answering Regular Path Queries Using Views. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2000 | KR | Containment of Conjunctive Regular Path Queries with Inverse. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2000 | LICS | View-Based Query Processing and Constraint Satisfaction. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2000 | MFCS | 0-1 Laws for Fragments of Existential Second-Order Logic: A Survey. | Phokion G. Kolaitis, Moshe Y. Vardi |
| 2000 | MFCS | µ-Calculus Synthesis. | Orna Kupferman, Moshe Y. Vardi |
| 2000 | PODS | View-Based Query Processing for Regular Path Queries with Inverse. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 2000 | PODS | Constraint Satisfaction and Database Theory: a Tutorial. | Moshe Y. Vardi |
| 1999 | CAV | Improved Automata Generation for Linear Temporal Logic. | Marco Daniele, Fausto Giunchiglia, 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 | FORTE | Black Box Checking. | Doron A. Peled, Moshe Y. Vardi, Mihalis Yannakakis |
| 1999 | PODS | Rewriting of Regular Expressions and Regular Path Queries. | Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi |
| 1999 | STACS | The Weakness of Self-Complementation. | Orna Kupferman, Moshe Y. Vardi |
| 1998 | CONCUR | Alternating Refinement Relations. | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi |
| 1998 | CONCUR | Synthesis from Knowledge-Based Specifications (Extended Abstract). | Ron van der Meyden, Moshe Y. Vardi |
| 1998 | CONCUR | Sometimes and Not Never Re-revisited: On Branching Versus Linear Time. | Moshe Y. Vardi |
| 1998 | FMCAD | Bisimulation Minimization in an Automata-Theoretic Verification Framework. | Kathi Fisler, Moshe Y. Vardi |
| 1998 | ICALP | Reasoning about The Past with Two-Way Automata. | Moshe Y. Vardi |
| 1998 | LICS | Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time. | Orna Kupferman, Moshe Y. Vardi |
| 1998 | LICS | Linear vs. Branching Time: A Complexity-Theoretic Perspective. | Moshe Y. Vardi |
| 1998 | PODS | Conjunctive-Query Containment and Constraint Satisfaction. | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1998 | SIGCSE | Panel: logic in the computer science curriculum. | Kim B. Bruce, Phokion G. Kolaitis, Daniel Leivant, Moshe Y. Vardi |
| 1998 | STOC | Weak Alternating Automata and Tree Automata Emptiness. | Orna Kupferman, Moshe Y. Vardi |
| 1998 | STACS | Complexity of Problems on Graphs Represented as OBDDs (Extended Abstract). | Joan Feigenbaum, Sampath Kannan, Moshe Y. Vardi, Mahesh Viswanathan |
| 1997 | CADE | Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. | Moshe Y. Vardi |
| 1997 | CAV | Model Checking and Transitive-Closure Logic. | Neil Immerman, 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 | LICS | First-Order Logic with Two Variables and Unary Temporal Logic. | Kousha Etessami, Moshe Y. Vardi, Thomas Wilke |
| 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 | ICDE | Database Research: Lead, Follow, or Get Out of the Way? - Panel Abstract. | Surajit Chaudhuri, Ashok K. Chandra, Umeshwar Dayal, Jim Gray, Michael Stonebraker, Gio Wiederhold, Moshe Y. Vardi |
| 1996 | LICS | On the Expressive Power of Variable-Confined Logics. | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1996 | LICS | Relating Word and Tree Automata. | Orna Kupferman, Shmuel Safra, Moshe Y. Vardi |
| 1996 | PODS | In Memoriam: Paris C. Kanellakis. | Serge Abiteboul, Gabriel M. Kuper, Christos H. Papadimitriou, Moshe Y. Vardi |
| 1995 | CAV | An Automata-Theoretic Approach to Fair Realizability and Synthesis. | Moshe Y. Vardi |
| 1995 | CONCUR | On the Complexity of Branching Modular Model Checking (Extended Abstract). | Orna Kupferman, Moshe Y. Vardi |
| 1995 | LICS | On the Complexity of Modular Model Checking | Moshe Y. Vardi |
| 1995 | PODC | Knowledge-Based Programs. | Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi |
| 1995 | PODS | On the Complexity of Bounded-Variable Queries. | Moshe Y. Vardi |
| 1994 | AAAI | An Operational Semantics for Knowledge Bases. | Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi |
| 1994 | CAV | An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract). | Orna Bernholtz, Moshe Y. Vardi, Pierre Wolper |
| 1994 | PODS | On the Complexity of Equivalence between Recursive and Nonrecursive Datalog Programs. | Surajit Chaudhuri, Moshe Y. Vardi |
| 1993 | CSL | The Complexity of Set Constraints. | Alexander Aiken, Dexter Kozen, Moshe Y. Vardi, Edward L. Wimmers |
| 1993 | PODS | Optimization of | Surajit Chaudhuri, Moshe Y. Vardi |
| 1993 | STOC | Parametric real-time reasoning. | Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi |
| 1993 | STOC | Monotone monadic SNP and constraint satisfaction. | Toms Feder, Moshe Y. Vardi |
| 1992 | ICALP | Infinitary Logic for Computer Science. | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1992 | ICDT | Computing with Infinitary Logic. | Serge Abiteboul, Moshe Y. Vardi, Victor Vianu |
| 1992 | LICS | Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1992 | PODS | On the Equivalence of Recursive and Nonrecursive Datalog Programs. | Surajit Chaudhuri, Moshe Y. Vardi |
| 1991 | KR | Model Checking vs. Theorem Proving: A Manifesto. | Joseph Y. Halpern, Moshe Y. Vardi |
| 1991 | LICS | Logic Programs as Types for Logic Programs | Thom W. Frhwirth, Ehud Shapiro, Moshe Y. Vardi, Eyal Yardeni |
| 1991 | PODS | Tools for Datalog Boundedness. | Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson, Moshe Y. Vardi |
| 1990 | CAV | Memory Efficient Algorithms for the Verification of Temporal Properties. | Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis |
| 1990 | ICLP | Global Optimization Problems for Database Logic Programs. | Moshe Y. Vardi |
| 1990 | LICS | On the Power of Bounded Concurrency~III: Reasoning About Programs (Preliminary Report) | David Harel, Roni Rosner, Moshe Y. Vardi |
| 1990 | LICS | 0-1 Laws for Infinitary Logics (Preliminary Report) | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1990 | PODS | On the Expressive Power of Datalog: Tools and a Case Study. | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1989 | LICS | On the Complexity of Epistemic Reasoning | Moshe Y. Vardi |
| 1989 | PODS | Proof-Tree Transformation Theorems and Their Applications. | Raghu Ramakrishnan, Yehoshua Sagiv, Jeffrey D. Ullman, Moshe Y. Vardi |
| 1989 | PODS | Safety of Datalog Queries over Infinite Databases. | Yehoshua Sagiv, Moshe Y. Vardi |
| 1989 | PODS | Automata Theory for Database Theoreticans. | Moshe Y. Vardi |
| 1989 | STOC | On omega-Automata and Temporal Logic (Preliminary Report) | Shmuel Safra, Moshe Y. Vardi |
| 1988 | CONCUR | An Automata-Theoretic Approach to Protocol Verification (Abstract). | Moshe Y. Vardi |
| 1988 | ICDT | On the Complexity of Queries in the Logical Data Model (Extended Abstract). | Gabriel M. Kuper, Moshe Y. Vardi |
| 1988 | LICS | 0-1 Laws and Decision Problems for Fragments of Second-Order Logic | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1988 | PODS | The Complexity of Ordering Subgoals. | Jeffrey D. Ullman, Moshe Y. Vardi |
| 1988 | PODS | Decidability and Undecidability Results for Boundedness of Linear Recursive Queries. | Moshe Y. Vardi |
| 1988 | POPL | A Temporal Fixpoint Calculus. | Moshe Y. Vardi |
| 1988 | SIGMOD | Database Logic Programming, Deductive Databases, and Expert Database Systems. | Moshe Y. Vardi |
| 1988 | STOC | Decidable Optimization Problems for Database Logic Programs (Preliminary Report) | Stavros S. Cosmadakis, Haim Gaifman, Paris C. Kanellakis, Moshe Y. Vardi |
| 1988 | STOC | Reasoning about Knowledge and Time in Asynchronous Systems | Joseph Y. Halpern, Moshe Y. Vardi |
| 1987 | LICS | Undecidable Optimization Problems for Database Logic Programs | Haim Gaifman, Harry G. Mairson, Yehoshua Sagiv, Moshe Y. Vardi |
| 1987 | LICS | Verification of Concurrent Programs: The Automata-Theoretic Framework | Moshe Y. Vardi |
| 1987 | STOC | The Decision Problem for the Probabilities of Higher-Order Properties | Phokion G. Kolaitis, Moshe Y. Vardi |
| 1986 | AAAI | What Can Machines Know? On the Epistemic Properties of Machines. | Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi |
| 1986 | LICS | An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) | Moshe Y. Vardi, Pierre Wolper |
| 1986 | PODS | On the Integrity of Databases with Incomplete Information. | Moshe Y. Vardi |
| 1986 | STOC | Reasoning about Fair Concurrent Programs | Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper |
| 1986 | STOC | The Complexity of Reasoning about Knowledge and Time: Extended Abstract | Joseph Y. Halpern, Moshe Y. Vardi |
| 1985 | FOCS | Automatic Verification of Probabilistic Concurrent Finite-State Programs | Moshe Y. Vardi |
| 1985 | ICALP | The Complementation Problem for Bchi Automata with Applications to Temporal Logic (Extended Abstract). | A. Prasad Sistla, Moshe Y. Vardi, Pierre Wolper |
| 1985 | IJCAI | A Model-Theoretic Analysis of Monotonic Knowledge. | Moshe Y. Vardi |
| 1985 | PODS | Querying Logical Databases. | Moshe Y. Vardi |
| 1985 | SIGMOD | On the Expressive Power of the Logical Data Model (Preliminary Report). | Gabriel M. Kuper, Moshe Y. Vardi |
| 1985 | STOC | An Internal Semantics for Modal Logic: Preliminary Report | Ronald Fagin, Moshe Y. Vardi |
| 1985 | STOC | Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report | Moshe Y. Vardi, Larry J. Stockmeyer |
| 1984 | FOCS | A Model-Theoretic Analysis of Knowledge: Preliminary Report | Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi |
| 1984 | ICALP | The Theory of Data Dependencies - An Overview. | Ronald Fagin, Moshe Y. Vardi |
| 1984 | PODS | On the Complexity and Axiomatizability of Consistent Database States. | Marc H. Graham, Moshe Y. Vardi |
| 1984 | PODS | On the Equivalence of Logical Databases. | Gabriel M. Kuper, Jeffrey D. Ullman, Moshe Y. Vardi |
| 1984 | PODS | A New Approach to Database Logic. | Gabriel M. Kuper, Moshe Y. Vardi |
| 1984 | STOC | Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract) | Moshe Y. Vardi, Pierre Wolper |
| 1983 | FOCS | Reasoning about Infinite Computation Paths (Extended Abstract) | Pierre Wolper, Moshe Y. Vardi, A. Prasad Sistla |
| 1983 | PODS | On the Semantics of Updates in Databases. | Ronald Fagin, Jeffrey D. Ullman, Moshe Y. Vardi |
| 1983 | PODS | The Revenge of the JD. | David Maier, Jeffrey D. Ullman, Moshe Y. Vardi |
| 1983 | STOC | Unary Inclusion Dependencies have Polynomial Time Inference Problems (Extended Abstract) | Paris C. Kanellakis, Stavros S. Cosmadakis, Moshe Y. Vardi |
| 1982 | FOCS | On Decomposition of Relational Databases | Moshe Y. Vardi |
| 1982 | PODS | The Implication and Finite Implication Problems for Typed Template Dependencies. | Moshe Y. Vardi |
| 1982 | STOC | The Complexity of Relational Query Languages (Extended Abstract) | Moshe Y. Vardi |
| 1981 | FOCS | Global Decision Problems for Relational Databases | Moshe Y. Vardi |
| 1981 | ICALP | The Implication Problem for Data Dependencies. | Catriel Beeri, Moshe Y. Vardi |