Moshe Y. Vardi

825 papers A* 186A 58B 59C 21Misc 1Journal 363Unranked 121

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	An On-the-Fly Synthesis Framework for LTL over Finite Traces. ACM Trans. Softw. Eng. Methodol. Shengping Xiao, Yongkang Li, Shufang Zhu, Jun Sun, Jianwen Li, Geguang Pu, Moshe Y. Vardi
2026	J	`jnl`	Incremental LTLf Synthesis. CoRR Giuseppe De Giacomo, Yves Lespérance, Gianmarco Parretti, Fabio Patrizi, Moshe Y. Vardi
2026	—	`ch.`	Let's Talk AI with Logician and Computer Science Expert Moshe Y. Vardi. Let's Talk AI Moshe Y. Vardi, Barbara Steffen
2026	J	`jnl`	Modeling Concurrent Multi-Agent Systems. CoRR Senthil Rajasekaran, Moshe Y. Vardi
2026	J	`jnl`	Multi-Property Synthesis. CoRR Christoph Weinhuber, Yannik Schnitzer, Alessandro Abate, David Parker, Giuseppe De Giacomo, Moshe Y. Vardi
2026	J	`jnl`	TIDE: A Trace-Informed Depth-First Exploration for Planning with Temporally Extended Goals. CoRR Yuliia Suprun, Khen Elimelech, Lydia E. Kavraki, Moshe Y. Vardi
2026	J	`jnl`	Techno-Optimism, Techno-Pessimism, and Techno-Realism. Commun. ACM Moshe Y. Vardi
2026	J	`jnl`	WME: Extending CDCL-based Model Enumeration with Weights. CoRR Giuseppe Spallitta, Moshe Y. Vardi
2026	J	`jnl`	Where We Should Discuss Only Computing Research. Commun. ACM Moshe Y. Vardi
2025	—	`conf`	A Theory of Regular Queries - Abstract. SEBD Moshe Y. Vardi
2025	J	`jnl`	Automata Linear Dynamic Logic on Finite Traces. Log. Methods Comput. Sci. Kevin W. Smith, Moshe Y. Vardi
2025	J	`jnl`	Big Tech, You Need Academia. Speak Up! Commun. ACM Moshe Y. Vardi
2025	J	`jnl`	Computing Is Indeed a Discipline in Crisis. Commun. ACM Moshe Y. Vardi
2025	J	`jnl`	Dynamic Boolean Synthesis with Zero-suppressed Decision Diagrams. CoRR Yi Lin, Moshe Y. Vardi
2025	C	`conf`	Engineering an LTL CIAA Alexandre Duret-Lutz, Shufang Zhu, Nir Piterman, Giuseppe De Giacomo, Moshe Y. Vardi
2025	J	`jnl`	Engineering an LTLf Synthesis Tool. CoRR Alexandre Duret-Lutz, Shufang Zhu, Nir Piterman, Giuseppe De Giacomo, Moshe Y. Vardi
2025	J	`jnl`	Homo Ratiocinator (Reckoning Human). Commun. ACM Moshe Y. Vardi
2025	J	`jnl`	I Teach Computer Science, and That Is Not All. Commun. ACM Moshe Y. Vardi
2025	J	`jnl`	I Was Wrong about the Ethics Crisis. Commun. ACM Moshe Y. Vardi
2025	J	`jnl`	It's Not the AI - It's Each of Us! Ten Commandments for the Wise & Responsible Use of AI. CoRR Barbara Steffen, Edward A. Lee, Moshe Y. Vardi, Bernhard Steffen
2025	J	`jnl`	Keeping the Dream Alive: The Power and Promise of Federally Funded Research. Commun. ACM Eric Horvitz, Margaret Martonosi, Moshe Y. Vardi, James R. Larus
2025	A*	`conf`	LTLf Synthesis Under Unreliable Input. AAAI Christian Hagemeier, Giuseppe De Giacomo, Moshe Y. Vardi
2025	A*	`conf`	LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces. IJCAI Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi
2025	J	`jnl`	Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization. CoRR Zhiwei Zhang, Samy Wu Fung, Anastasios Kyrillidis, Stanley J. Osher, Moshe Y. Vardi
2025	C	`conf`	Understanding Boolean Function Learnability on Deep Neural Networks: PAC Learning Meets Neurosymbolic Models. NeSy Márcio Nicolau, Anderson R. Tavares, Zhiwei Zhang, Pedro H. C. Avelar, João Marcos Flach, Luís C. Lamb, Moshe Y. Vardi
2025	J	`jnl`	Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems. CoRR Senthil Rajasekaran, Moshe Y. Vardi
2025	J	`jnl`	Will AI Destroy the World Wide Web? Commun. ACM Moshe Y. Vardi
2024	A*	`conf`	Accelerating Long-Horizon Planning with Affordance-Directed Dynamic Grounding of Abstract Strategies. ICRA Khen Elimelech, Zachary Kingston, Wil Thomason, Moshe Y. Vardi, Lydia E. Kavraki
2024	J	`jnl`	Computing, You Have Blood on Your Hands! Commun. ACM Moshe Y. Vardi
2024	—	`conf`	Dynamic Programming for Symbolic Boolean Realizability and Synthesis. CAV (3) Yi Lin, Lucas Martinelli Tabajara, Moshe Y. Vardi
2024	J	`jnl`	Dynamic Programming for Symbolic Boolean Realizability and Synthesis. CoRR Yi Lin, Lucas M. Tabajara, Moshe Y. Vardi
2024	J	`jnl`	Encoding Reusable Multi-Robot Planning Strategies as Abstract Hypergraphs. CoRR Khen Elimelech, James Motes, Marco Morales, Nancy M. Amato, Moshe Y. Vardi, Lydia E. Kavraki
2024	J	`jnl`	Falsification of Autonomous Systems in Rich Environments. CoRR Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2024	J	`jnl`	Human Intuition and Algorithmic Efficiency Must Be Balanced to Enhance Data Mesh Resilience. Commun. ACM Andrew Strelzoff, Benjamin D. Trump, Christopher L. Cummings, Madison Smith, Stephanie Elisabeth Galaitsi, Kelsey Stoddard, Jeffrey M. Keisler, Moshe Y. Vardi, Nathaniel D. Bastian, Alexander Kott, Igor Linkov
2024	J	`jnl`	Is Computing a Discipline in Crisis? Commun. ACM Moshe Y. Vardi
2024	J	`jnl`	LTLf Synthesis Under Unreliable Input. CoRR Christian Hagemeier, Giuseppe De Giacomo, Moshe Y. Vardi
2024	J	`jnl`	LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces. CoRR Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin, Moshe Y. Vardi
2024	A	`conf`	Logical Algorithmics: From Relational Queries to Boolean Reasoning (Invited Talk). SAT Moshe Y. Vardi
2024	B	`conf`	Logical Algorithmics: From Theory to Practice (Invited Talk). CSL Moshe Y. Vardi
2024	—	`conf`	MoXI: An Intermediate Language for Symbolic Model Checking. SPIN Kristin Yvonne Rozier, Rohit Dureja, Ahmed Irfan, Chris Johannsen, Karthik Nukala, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi
2024	—	`conf`	Model-Guided Synthesis for LTL over Finite Traces. VMCAI (1) Shengping Xiao, Yongkang Li, Xinyue Huang, Yicong Xu, Jianwen Li, Geguang Pu, Ofer Strichman, Moshe Y. Vardi
2024	J	`jnl`	More Is Different, in Social Media Too. Commun. ACM Moshe Y. Vardi
2024	J	`jnl`	On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts. CoRR Shengping Xiao, Yongkang Li, Shufang Zhu, Jun Sun, Jianwen Li, Geguang Pu, Moshe Y. Vardi
2024	A*	`conf`	Probabilistic Synthesis and Verification for LTL on Finite Traces. KR Benjamin Aminof, Linus Cooper, Sasha Rubin, Moshe Y. Vardi, Florian Zuleger
2024	J	`jnl`	Singly exponential translation of alternating weak Büchi automata to unambiguous Büchi automata. Theor. Comput. Sci. Yong Li, Sven Schewe, Moshe Y. Vardi
2024	A*	`conf`	Stochastic Games for Interactive Manipulation Domains. ICRA Karan Muvvala, Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2024	J	`jnl`	Stochastic Games for Interactive Manipulation Domains. CoRR Karan Muvvala, Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2024	J	`jnl`	The Linear Fallacy. Commun. ACM Moshe Y. Vardi
2024	—	`conf`	The MoXI Model Exchange Tool Suite. CAV (1) Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier
2024	A*	`conf`	The Trembling-Hand Problem for LTLf Planning. IJCAI Pian Yu, Shufang Zhu, Giuseppe De Giacomo, Marta Kwiatkowska, Moshe Y. Vardi
2024	J	`jnl`	The Trembling-Hand Problem for LTLf Planning. CoRR Pian Yu, Shufang Zhu, Giuseppe De Giacomo, Marta Kwiatkowska, Moshe Y. Vardi
2024	—	`conf`	What Came First, Mathematics or Computing? SETSS Moshe Y. Vardi
2024	J	`jnl`	What Do Computing and Economics Have to Say to Each Other? Commun. ACM Moshe Y. Vardi
2024	J	`jnl`	What Is Theoretical Computer Science? Commun. ACM Moshe Y. Vardi
2023	J	`jnl`	ACM for the Public Good. Commun. ACM Moshe Y. Vardi
2023	B	`conf`	Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. FMCAD Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi
2023	A*	`conf`	Extracting generalizable skills from a single plan execution using abstraction-critical state detection. ICRA Khen Elimelech, Lydia E. Kavraki, Moshe Y. Vardi
2023	J	`jnl`	How Not to Win a Tech War. Commun. ACM Moshe Y. Vardi
2023	—	`conf`	How to Be An Ethical Technologist. ECBS Moshe Y. Vardi
2023	A	`conf`	Logical Algorithmics: From Theory to Practice (Invited Talk). STACS Moshe Y. Vardi
2023	—	`conf`	Model Checking Strategies from Synthesis over Finite Traces. ATVA (1) Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi, Andrew M. Wells
2023	A*	`conf`	Multi-Agent Systems with Quantitative Satisficing Goals. IJCAI Senthil Rajasekaran, Suguman Bansal, Moshe Y. Vardi
2023	J	`jnl`	Multi-Agent Systems with Quantitative Satisficing Goals. CoRR Senthil Rajasekaran, Suguman Bansal, Moshe Y. Vardi
2023	J	`jnl`	On Strategies in Synthesis Over Finite Traces. CoRR Suguman Bansal, Yong Li, Lucas Martinelli Tabajara, Moshe Y. Vardi, Andrew M. Wells
2023	J	`jnl`	On the power of finite ambiguity in Büchi complementation. Inf. Comput. Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang
2023	J	`jnl`	Revisiting ACM's Open-Conference Principle. Commun. ACM Moshe Y. Vardi
2023	B	`conf`	Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. CONCUR Yong Li, Sven Schewe, Moshe Y. Vardi
2023	J	`jnl`	Singly Exponential Translation of Alternating Weak Büchi Automata to Unambiguous Büchi Automata. CoRR Yong Li, Sven Schewe, Moshe Y. Vardi
2023	J	`jnl`	Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints. CoRR Moshe Y. Vardi, Zhiwei Zhang
2023	A*	`conf`	Solving Quantum-Inspired Perfect Matching Problems via Tutte-Theorem-Based Hybrid Boolean Constraints. IJCAI Moshe Y. Vardi, Zhiwei Zhang
2023	J	`jnl`	To Regulate Tech, Nullify Click-Through Contracts. Commun. ACM Moshe Y. Vardi
2023	J	`jnl`	What Came First, Math or Computing? Commun. ACM Moshe Y. Vardi
2023	J	`jnl`	Who Is Responsible Around Here? Commun. ACM Moshe Y. Vardi
2022	J	`jnl`	ACM, ethics, and corporate behavior. Commun. ACM Moshe Y. Vardi
2022	J	`jnl`	Accountability and liability in computing. Commun. ACM Moshe Y. Vardi
2022	J	`jnl`	An association of the members, by the members, for the members. Commun. ACM Moshe Y. Vardi
2022	C	`conf`	Automatic Cross-domain Task Plan Transfer by Caching Abstract Skills. WAFR Khen Elimelech, Lydia E. Kavraki, Moshe Y. Vardi
2022	J	`jnl`	Comparator automata in quantitative verification. Log. Methods Comput. Sci. Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi
2022	—	`conf`	Compositional Safety LTL Synthesis. VSTTE Suguman Bansal, Giuseppe De Giacomo, Antonio Di Stasio, Yong Li, Moshe Y. Vardi, Shufang Zhu
2022	A*	`conf`	Constraint-Driven Explanations for Black-Box ML Models. AAAI Aditya A. Shrotri, Nina Narodytska, Alexey Ignatiev, Kuldeep S. Meel, João Marques-Silva, Moshe Y. Vardi
2022	J	`jnl`	DPER: Dynamic Programming for Exist-Random Stochastic SAT. CoRR Vu H. N. Phan, Moshe Y. Vardi
2022	J	`jnl`	DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving. CoRR Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang
2022	J	`jnl`	DPO: Dynamic-Programming Optimization on Hybrid Constraints. CoRR Vu H. N. Phan, Moshe Y. Vardi
2022	A*	`conf`	DPSampler: Exact Weighted Sampling Using Dynamic Programming. IJCAI Jeffrey M. Dudek, Aditya A. Shrotri, Moshe Y. Vardi
2022	—	`conf`	Divide-and-Conquer Determinization of Büchi Automata Based on SCC Decomposition. CAV (2) Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, Lijun Zhang
2022	J	`jnl`	Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition. CoRR Yong Li, Andrea Turrini, Weizhi Feng, Moshe Y. Vardi, Lijun Zhang
2022	—	`ch.`	Efficiency vs. Resilience: Lessons from COVID-19. Perspectives on Digital Humanism Moshe Y. Vardi
2022	C	`conf`	Efficient Task Planning Using Abstract Skills and Dynamic Road Map Matching. ISRR Khen Elimelech, Lydia E. Kavraki, Moshe Y. Vardi
2022	J	`jnl`	Finite-trace and generalized-reactivity specifications in temporal synthesis. Formal Methods Syst. Des. Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, Shufang Zhu
2022	J	`jnl`	Functional synthesis via input-output separation. Formal Methods Syst. Des. Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi
2022	A*	`conf`	LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work. IJCAI Giuseppe De Giacomo, Marco Favorito, Jianwen Li, Moshe Y. Vardi, Shengping Xiao, Shufang Zhu
2022	C	`conf`	Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk). TIME Moshe Y. Vardi
2022	C	`conf`	Program Verification: A 70+-Year History. ICSOFT Moshe Y. Vardi
2022	A*	`conf`	Public and Private Affairs in Strategic Reasoning. KR Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi
2022	J	`jnl`	Quantum-Inspired Perfect Matching under Vertex-Color Constraints. CoRR Moshe Y. Vardi, Zhiwei Zhang
2022	J	`jnl`	Satisfiability checking for Mission-time LTL (MLTL). Inf. Comput. Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier
2022	J	`jnl`	Sequential Relational Decomposition. Log. Methods Comput. Sci. Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi
2022	A*	`conf`	Synthesis from Satisficing and Temporal Goals. AAAI Suguman Bansal, Lydia E. Kavraki, Moshe Y. Vardi, Andrew M. Wells
2022	J	`jnl`	Synthesis from Satisficing and Temporal Goals. CoRR Suguman Bansal, Lydia E. Kavraki, Moshe Y. Vardi, Andrew M. Wells
2022	J	`jnl`	Technology and democracy. Commun. ACM Moshe Y. Vardi
2022	—	`conf`	Towards a Grand Unification of Büchi Complementation Constructions. Principles of Systems Design Moshe Y. Vardi, Seth Fogarty, Yong Li, Yih-Kuen Tsay
2022	A*	`conf`	Verification and Realizability in Finite-Horizon Multiagent Systems. KR Senthil Rajasekaran, Moshe Y. Vardi
2022	J	`jnl`	Verification and Realizability in Finite-Horizon Multiagent Systems. CoRR Senthil Rajasekaran, Moshe Y. Vardi
2022	J	`jnl`	War and tech (and ACM). Commun. ACM Moshe Y. Vardi
2022	J	`jnl`	Will AI destroy education? Commun. ACM Moshe Y. Vardi
2022	—	`conf`	ZDD Boolean Synthesis. TACAS (1) Yi Lin, Lucas M. Tabajara, Moshe Y. Vardi
2021	—	`conf`	Adapting Behaviors via Reactive Synthesis. CAV (1) Gal Amram, Suguman Bansal, Dror Fried, Lucas Martinelli Tabajara, Moshe Y. Vardi, Gera Weiss
2021	J	`jnl`	Adapting Behaviors via Reactive Synthesis. CoRR Gal Amram, Suguman Bansal, Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi, Gera Weiss
2021	—	`ch.`	Approximate Model Counting. Handbook of Satisfiability Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2021	J	`jnl`	Automata Linear Dynamic Logic on Finite Traces. CoRR Kevin W. Smith, Moshe Y. Vardi
2021	B	`conf`	Congruence Relations for Büchi Automata. FM Yong Li, Yih-Kuen Tsay, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang
2021	J	`jnl`	Congruence Relations for Büchi Automata. CoRR Yong Li, Yih-Kuen Tsay, Moshe Y. Vardi
2021	A	`conf`	Deep Tech Ethics: An Approach to Teaching Social Justice in Computer Science. SIGCSE Rodrigo Ferreira, Moshe Y. Vardi
2021	A*	`conf`	Finite-Horizon Synthesis for Probabilistic Manipulation Domains. ICRA Andrew M. Wells, Zachary Kingston, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2021	A*	`conf`	Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis. IJCAI Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, Shufang Zhu
2021	—	`conf`	From Linear Temporal Logics to Büchi Automata: The Early and Simple Principle. Model Checking, Synthesis, and Learning Yih-Kuen Tsay, Moshe Y. Vardi
2021	B	`conf`	Linear Temporal Logic - From Infinite to Finite Horizon. ATVA Lucas M. Tabajara, Moshe Y. Vardi
2021	A	`conf`	Nash Equilibria in Finite-Horizon Multiagent Concurrent Games. AAMAS Senthil Rajasekaran, Moshe Y. Vardi
2021	J	`jnl`	Nash Equilibria in Finite-Horizon Multiagent Concurrent Games. CoRR Senthil Rajasekaran, Moshe Y. Vardi
2021	A*	`conf`	On Continuous Local BDD-Based Search for Hybrid SAT Solving. AAAI Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang
2021	—	`conf`	On Satisficing in Quantitative Games. TACAS (1) Suguman Bansal, Krishnendu Chatterjee, Moshe Y. Vardi
2021	J	`jnl`	On Satisficing in Quantitative Games. CoRR Suguman Bansal, Krishnendu Chatterjee, Moshe Y. Vardi
2021	—	`conf`	On the Power of Automata Minimization in Temporal Synthesis. GandALF Shufang Zhu, Lucas M. Tabajara, Geguang Pu, Moshe Y. Vardi
2021	J	`jnl`	On the Power of Finite Ambiguity in Büchi Complementation. CoRR Weizhi Feng, Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang
2021	A*	`conf`	On-the-fly Synthesis for LTL over Finite Traces. AAAI Shengping Xiao, Jianwen Li, Shufang Zhu, Yingying Shi, Geguang Pu, Moshe Y. Vardi
2021	—	`conf`	Panel on "Past and Future of Computer Science Theory" (Discussion Paper). SEBD Ronald Fagin, Georg Gottlob, Christos H. Papadimitriou, Moshe Y. Vardi, Giorgio Ausiello, Maurizio Lenzerini, Domenico Saccà, Luigi Palopoli, Francesco Scarcello
2021	A	`conf`	ProCount: Weighted Projected Model Counting with Graded Project-Join Trees. SAT Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi
2021	Misc	`conf`	Program Verification: a 70+- Year History. TASE Moshe Y. Vardi
2021	J	`jnl`	Program verification: vision and reality. Commun. ACM Moshe Y. Vardi
2021	J	`jnl`	Reboot the computing-research publication systems. Commun. ACM Moshe Y. Vardi
2021	J	`jnl`	Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions. Artif. Intell. Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Y. Vardi, Zhiwei Zhang
2021	J	`jnl`	Strategy Logic with Imperfect Information. ACM Trans. Comput. Log. Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi
2021	A*	`conf`	Synthesizing Good-Enough Strategies for LTLf Specifications. IJCAI Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang
2021	J	`jnl`	The agency trilemma and ACM. Commun. ACM Moshe Y. Vardi
2021	J	`jnl`	The paradox of choice in computing-research conferences. Commun. ACM Moshe Y. Vardi
2021	J	`jnl`	The people vs. tech. Commun. ACM Moshe Y. Vardi
2021	J	`jnl`	The sand-heap paradox of privacy and influence. Commun. ACM Moshe Y. Vardi
2021	—	`ch.`	Verification. Handbook of Automata Theory (II.) Javier Esparza, Orna Kupferman, Moshe Y. Vardi
2020	J	`jnl`	A computational lens on economics. Commun. ACM Moshe Y. Vardi
2020	A*	`conf`	ADDMC: Weighted Model Counting with Algebraic Decision Diagrams. AAAI Jeffrey M. Dudek, Vu Phan, Moshe Y. Vardi
2020	J	`jnl`	Advancing computing as a science and profession: but to what end? Commun. ACM Moshe Y. Vardi
2020	A*	`conf`	Assume-Guarantee Synthesis for Prompt Linear Temporal Logic. IJCAI Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, Moshe Y. Vardi
2020	J	`jnl`	Computer-Aided Personalized Education. CoRR Rajeev Alur, Richard G. Baraniuk, Rastislav Bodík, Ann W. Drobnis, Sumit Gulwani, Bjoern Hartmann, Yasmin B. Kafai, Jeff Karpicke, Ran Libeskind-Hadas, Debra J. Richardson, Armando Solar-Lezama, Candace Thille, Moshe Y. Vardi
2020	A	`conf`	DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees. CP Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi
2020	J	`jnl`	DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees. CoRR Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi
2020	J	`jnl`	Efficiency vs. resilience: what COVID-19 teaches computing. Commun. ACM Moshe Y. Vardi
2020	J	`jnl`	FPRAS Approximation of the Matrix Permanent in Practice. CoRR James E. Newman, Moshe Y. Vardi
2020	A*	`conf`	FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints. AAAI Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Y. Vardi, Zhiwei Zhang
2020	A*	`conf`	Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective. IJCAI Luís C. Lamb, Artur S. d'Avila Garcez, Marco Gori, Marcelo O. R. Prates, Pedro H. C. Avelar, Moshe Y. Vardi
2020	J	`jnl`	Graph Neural Networks Meet Neural-Symbolic Computing: A Survey and Perspective. CoRR Luís C. Lamb, Artur S. d'Avila Garcez, Marco Gori, Marcelo O. R. Prates, Pedro H. C. Avelar, Moshe Y. Vardi
2020	A*	`conf`	Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. AAAI Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi
2020	—	`conf`	LTLf Synthesis on Probabilistic Systems. GandALF Andrew M. Wells, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2020	—	`conf`	LTLf Synthesis under Partial Observability: From Theory to Practice. GandALF Lucas M. Tabajara, Moshe Y. Vardi
2020	A*	`conf`	LTLƒ Synthesis with Fairness and Stability Assumptions. AAAI Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi
2020	J	`jnl`	On Continuous Local BDD-Based Search for Hybrid SAT Solving. CoRR Anastasios Kyrillidis, Moshe Y. Vardi, Zhiwei Zhang
2020	J	`jnl`	On Uniformly Sampling Traces of a Transition System (Extended Version). CoRR Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi
2020	A	`conf`	On Uniformly Sampling Traces of a Transition System. ICCAD Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi
2020	—	`conf`	On the Power of Unambiguity in Büchi Complementation. GandALF Yong Li, Moshe Y. Vardi, Lijun Zhang
2020	—	`ch.`	On the Unreasonable Effectiveness of SAT Solvers. Beyond the Worst-Case Analysis of Algorithms Vijay Ganesh, Moshe Y. Vardi
2020	J	`jnl`	Parallel Weighted Model Counting with Tensor Networks. CoRR Jeffrey M. Dudek, Moshe Y. Vardi
2020	J	`jnl`	Publish Commun. ACM Moshe Y. Vardi
2020	B	`conf`	Runtime Verification on FPGAs with LTLf Specifications. FMCAD Tommy Tracy II, Lucas M. Tabajara, Moshe Y. Vardi, Kevin Skadron
2020	J	`jnl`	SAT-based explicit LTLf satisfiability checking. Artif. Intell. Jianwen Li, Geguang Pu, Yueling Zhang, Moshe Y. Vardi, Kristin Y. Rozier
2020	J	`jnl`	Strategy Logic with Imperfect Information. CoRR Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi
2020	A*	`conf`	Two-Stage Technique for LTLf Synthesis Under LTL Assumptions. KR Giuseppe De Giacomo, Antonio Di Stasio, Moshe Y. Vardi, Shufang Zhu
2020	J	`jnl`	Understanding Boolean Function Learnability on Deep Neural Networks. CoRR Anderson R. Tavares, Pedro H. C. Avelar, João M. Flach, Márcio Nicolau, Luís C. Lamb, Moshe Y. Vardi
2020	J	`jnl`	What should be done about social media? Commun. ACM Moshe Y. Vardi
2020	J	`jnl`	Where have all the domestic graduate students gone? Commun. ACM Moshe Y. Vardi
2019	J	`jnl`	ADDMC: Exact Weighted Model Counting with Algebraic Decision Diagrams. CoRR Jeffrey M. Dudek, Vu H. N. Phan, Moshe Y. Vardi
2019	J	`jnl`	Are we having an ethical crisis in computing? Commun. ACM Moshe Y. Vardi
2019	J	`jnl`	Automated Abstraction of Manipulation Domains for Cost-Based Reactive Synthesis. IEEE Robotics Autom. Lett. Keliang He, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2019	J	`jnl`	Efficient Contraction of Large Tensor Networks for Weighted Model Counting through Graph Decompositions. CoRR Jeffrey M. Dudek, Leonardo Dueñas-Osorio, Moshe Y. Vardi
2019	A*	`conf`	Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks. ICRA Keliang He, Andrew M. Wells, Lydia E. Kavraki, Moshe Y. Vardi
2019	C	`conf`	First-Order vs. Second-Order Encodings for LTL TAMC Shufang Zhu, Geguang Pu, Moshe Y. Vardi
2019	J	`jnl`	First-Order vs. Second-Order Encodings for LTLf-to-Automata Translation. CoRR Shufang Zhu, Geguang Pu, Moshe Y. Vardi
2019	J	`jnl`	FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints. CoRR Anastasios Kyrillidis, Anshumali Shrivastava, Moshe Y. Vardi, Zhiwei Zhang
2019	J	`jnl`	Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications. CoRR Suguman Bansal, Yong Li, Lucas M. Tabajara, Moshe Y. Vardi
2019	—	`conf`	Intersection and Rotation of Assumption Literals Boosts Bug-Finding. VSTTE Rohit Dureja, Jianwen Li, Geguang Pu, Moshe Y. Vardi, Kristin Y. Rozier
2019	J	`jnl`	LTLf Synthesis with Fairness and Stability Assumptions. CoRR Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi
2019	A*	`conf`	Labor Division with Movable Walls: Composing Executable Specifications with Machine Learning and Search (Blue Sky Idea). AAAI David Harel, Assaf Marron, Ariel Rosenfeld, Moshe Y. Vardi, Gera Weiss
2019	A*	`conf`	Learning to Solve NP-Complete Problems: A Graph Neural Network for Decision TSP. AAAI Marcelo O. R. Prates, Pedro H. C. Avelar, Henrique Lemos, Luís C. Lamb, Moshe Y. Vardi
2019	J	`jnl`	Lost in math? Commun. ACM Moshe Y. Vardi
2019	A*	`conf`	Not All FPRASs are Equal: Demystifying FPRASs for DNF-Counting (Extended Abstract). IJCAI Kuldeep S. Meel, Aditya A. Shrotri, Moshe Y. Vardi
2019	J	`jnl`	Not all FPRASs are equal: demystifying FPRASs for DNF-counting. Constraints An Int. J. Kuldeep S. Meel, Aditya A. Shrotri, Moshe Y. Vardi
2019	A	`conf`	On Symbolic Approaches for Computing the Matrix Permanent. CP Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi
2019	J	`jnl`	On Symbolic Approaches for Computing the Matrix Permanent. CoRR Supratik Chakraborty, Aditya A. Shrotri, Moshe Y. Vardi
2019	A*	`conf`	On the Hardness of Probabilistic Inference Relaxations. AAAI Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2019	A*	`conf`	Partitioning Techniques in LTLf Synthesis. IJCAI Lucas Martinelli Tabajara, Moshe Y. Vardi
2019	J	`jnl`	Principled network reliability approximation: A counting-based approach. Reliab. Eng. Syst. Saf. Roger Paredes, Leonardo Dueñas-Osorio, Kuldeep S. Meel, Moshe Y. Vardi
2019	J	`jnl`	Quantum hype and quantum skepticism. Commun. ACM Moshe Y. Vardi
2019	A*	`conf`	SAT-Based Explicit LTLf Satisfiability Checking. AAAI Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi
2019	J	`jnl`	SAT-based explicit LTL reasoning and its application to satisfiability checking. Formal Methods Syst. Des. Jianwen Li, Shufang Zhu, Geguang Pu, Lijun Zhang, Moshe Y. Vardi
2019	—	`conf`	Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion. CAV (1) Suguman Bansal, Moshe Y. Vardi
2019	—	`conf`	Satisfiability Checking for Mission-Time LTL. CAV (2) Jianwen Li, Moshe Y. Vardi, Kristin Y. Rozier
2019	J	`jnl`	Sequential Relational Decomposition. CoRR Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi
2019	J	`jnl`	Solving Parity Games Using An Automata-Based Algorithm. CoRR Antonio Di Stasio, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
2019	J	`jnl`	The long game of research. Commun. ACM Moshe Y. Vardi
2019	J	`jnl`	The winner-takes-all tech corporation. Commun. ACM Moshe Y. Vardi
2019	J	`jnl`	To serve humanity. Commun. ACM Moshe Y. Vardi
2019	A*	`conf`	Unbounded Orchestrations of Transducers for Manufacturing. AAAI Natasha Alechina, Tomás Brázdil, Giuseppe De Giacomo, Paolo Felli, Brian Logan, Moshe Y. Vardi
2018	J	`jnl`	4th International Workshop on Strategic Reasoning (SR 2016). Inf. Comput. Alessio R. Lomuscio, Moshe Y. Vardi
2018	J	`jnl`	A declaration of the dependence of cyberspace. Commun. ACM Moshe Y. Vardi
2018	J	`jnl`	Accelerating LTL satisfiability checking by SAT solvers. J. Log. Comput. Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y. Vardi, Jifeng He
2018	J	`jnl`	An explicit transition system construction approach to LTL satisfiability checking. Formal Aspects Comput. Jianwen Li, Lijun Zhang, Shufang Zhu, Geguang Pu, Moshe Y. Vardi, Jifeng He
2018	—	`conf`	Automata vs Linear-Programming Discounted-Sum Inclusion. CAV (2) Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi
2018	B	`conf`	Comparator Automata in Quantitative Verification. FoSSaCS Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi
2018	J	`jnl`	Comparator automata in quantitative verification. CoRR Suguman Bansal, Swarat Chaudhuri, Moshe Y. Vardi
2018	J	`jnl`	Computer professionals for social responsibility. Commun. ACM Moshe Y. Vardi
2018	B	`conf`	Functional Synthesis via Input-Output Separation. FMCAD Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi
2018	J	`jnl`	Functional Synthesis via Input-Output Separation. CoRR Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi
2018	J	`jnl`	How the hippies destroyed the internet. Commun. ACM Moshe Y. Vardi
2018	J	`jnl`	How we lost the women in computing. Commun. ACM Moshe Y. Vardi
2018	J	`jnl`	Learning to Solve NP-Complete Problems - A Graph Neural Network for the Decision TSP. CoRR Marcelo O. R. Prates, Pedro H. C. Avelar, Henrique Lemos, Luís C. Lamb, Moshe Y. Vardi
2018	J	`jnl`	Mode-Target Games: Reactive Synthesis for Control Applications. IEEE Trans. Autom. Control. Ayca Balkan, Moshe Y. Vardi, Paulo Tabuada
2018	J	`jnl`	Move fast and break things. Commun. ACM Moshe Y. Vardi
2018	J	`jnl`	Network Reliability Estimation in Theory and Practice. CoRR Roger Paredes, Leonardo Dueñas-Osorio, Kuldeep S. Meel, Moshe Y. Vardi
2018	J	`jnl`	Open access and ACM. Commun. ACM Moshe Y. Vardi
2018	J	`jnl`	SAT-based Explicit LTLf Satisfiability Checking. CoRR Jianwen Li, Kristin Y. Rozier, Geguang Pu, Yueling Zhang, Moshe Y. Vardi
2018	J	`jnl`	Self-reference and section 230. Commun. ACM Moshe Y. Vardi
2018	A*	`conf`	Sequential Relational Decomposition. LICS Dror Fried, Axel Legay, Joël Ouaknine, Moshe Y. Vardi
2018	—	`conf`	SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability. CAV (2) Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Yvonne Rozier, Moshe Y. Vardi
2018	C	`conf`	Solving Parity Games: Explicit vs Symbolic. CIAA Antonio Di Stasio, Aniello Murano, Moshe Y. Vardi
2018	J	`jnl`	Strategy Logic with Imperfect Information. CoRR Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi
2018	A*	`conf`	Synthesis of Orchestrations of Transducers for Manufacturing. AAAI Giuseppe De Giacomo, Moshe Y. Vardi, Paolo Felli, Natasha Alechina, Brian Logan
2018	B	`conf`	The Siren Song of Temporal Synthesis (Invited Talk). CONCUR Moshe Y. Vardi
2017	A*	`conf`	2017 ACM PODS Alberto O. Mendelzon Test-of-Time Award. PODS Leonid Libkin, Moshe Y. Vardi
2017	J	`jnl`	A Symbolic Approach to Safety LTL Synthesis. CoRR Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
2017	—	`conf`	A Symbolic Approach to Safety ltl Synthesis. Haifa Verification Conference Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
2017	J	`jnl`	ACM's open-conference principle and political reality. Commun. ACM Moshe Y. Vardi
2017	J	`jnl`	Alonzo Church Award 2017 - Call for Nominations. Bull. EATCS Natarajan Shankar, Catuscia Palamidessi, Gordon D. Plotkin, Moshe Y. Vardi
2017	J	`jnl`	Combining the k-CNF and XOR Phase-Transitions. CoRR Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi
2017	A*	`conf`	Counting-Based Reliability Estimation for Power-Transmission Grids. AAAI Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, Moshe Y. Vardi
2017	J	`jnl`	Cyber insecurity and cyber libertarianism. Commun. ACM Moshe Y. Vardi
2017	J	`jnl`	Divination by program committee. Commun. ACM Moshe Y. Vardi
2017	B	`conf`	Factored boolean functional synthesis. FMCAD Lucas M. Tabajara, Moshe Y. Vardi
2017	—	`conf`	Flow Games. FSTTCS Orna Kupferman, Gal Vardi, Moshe Y. Vardi
2017	—	`conf`	On Hashing-Based Approaches to Approximate DNF-Counting. FSTTCS Kuldeep S. Meel, Aditya A. Shrotri, Moshe Y. Vardi
2017	J	`jnl`	On Hashing-Based Approaches to Approximate DNF-Counting. CoRR Kuldeep S. Meel, Aditya A. Shrotri, Moshe Y. Vardi
2017	J	`jnl`	Preface to the Special Issue on SR 2014. Inf. Comput. Fabio Mogavero, Aniello Murano, Moshe Y. Vardi
2017	—	`conf`	Random Models for Evaluating Efficient Büchi Universality Checking. ICLA Corey Fisher, Seth Fogarty, Moshe Y. Vardi
2017	A	`conf`	Reactive synthesis for finite tasks under resource constraints. IROS Keliang He, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2017	J	`jnl`	Reasoning about Strategies: on the Satisfiability Problem. Log. Methods Comput. Sci. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
2017	J	`jnl`	Regular Queries on Graph Databases. Theory Comput. Syst. Juan L. Reutter, Miguel Romero, Moshe Y. Vardi
2017	A	`conf`	Safety model checking with complementary approximations. ICCAD Jianwen Li, Shufang Zhu, Yueling Zhang, Geguang Pu, Moshe Y. Vardi
2017	A*	`conf`	Strategy logic with imperfect information. LICS Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, Moshe Y. Vardi
2017	J	`jnl`	Supervisory control and reactive synthesis: a comparative introduction. Discret. Event Dyn. Syst. Rüdiger Ehlers, Stéphane Lafortune, Stavros Tripakis, Moshe Y. Vardi
2017	A*	`conf`	Symbolic LTLf Synthesis. IJCAI Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
2017	J	`jnl`	Symbolic LTLf Synthesis. CoRR Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
2017	J	`jnl`	Technology for the most effective use of mankind. Commun. ACM Moshe Y. Vardi
2017	J	`jnl`	Ten years at the helm of Commun. ACM Moshe Y. Vardi
2017	A*	`conf`	The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas. IJCAI Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi
2017	J	`jnl`	The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas. CoRR Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi
2017	A*	`conf`	The homomorphism problem for regular graph patterns. LICS Miguel Romero, Pablo Barceló, Moshe Y. Vardi
2017	J	`jnl`	Would Turing have won the Turing award? Commun. ACM Moshe Y. Vardi
2016	J	`jnl`	2014 CAV award announcement. Formal Methods Syst. Des. Marta Kwiatkowska, Moshe Y. Vardi, Ahmed Bouajjani, Thomas Ball
2016	A*	`conf`	A Theory of Regular Queries. PODS Moshe Y. Vardi
2016	C	`ed.`	AI, Ethics, and Society, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 13, 2016. AAAI Workshop: AI, Ethics, and Society Blai Bonet, Sven Koenig, Benjamin Kuipers, Illah R. Nourbakhsh, Stuart Russell, Moshe Y. Vardi, Toby Walsh
2016	J	`jnl`	Academic rankings considered harmful! Commun. ACM Moshe Y. Vardi
2016	A*	`conf`	Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls. IJCAI Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2016	J	`jnl`	Alonzo Church Award 2016 - Call for Nominations. Bull. EATCS Moshe Y. Vardi
2016	A*	`conf`	Approximate Probabilistic Inference via Word-Level Counting. AAAI Supratik Chakraborty, Kuldeep S. Meel, Rakesh Mistry, Moshe Y. Vardi
2016	J	`jnl`	Approximate Reachability. CoRR Jianwen Li, Shufang Zhu, Yueling Zhang, Geguang Pu, Moshe Y. Vardi
2016	J	`jnl`	Are we headed toward another global tech bust? Commun. ACM Moshe Y. Vardi
2016	—	`conf`	BDD-Based Boolean Functional Synthesis. CAV (2) Dror Fried, Lucas M. Tabajara, Moshe Y. Vardi
2016	A*	`conf`	Combining the k-CNF and XOR Phase-Transitions. IJCAI Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi
2016	—	`conf`	Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. AAAI Workshop: Beyond NP Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, Sharad Malik
2016	J	`jnl`	Globalization, computing, and their political impact. Commun. ACM Moshe Y. Vardi
2016	J	`jnl`	Iterative Temporal Planning in Uncertain Environments With Partial Satisfaction Guarantees. IEEE Trans. Robotics Morteza Lahijanian, Matthew R. Maly, Dror Fried, Lydia E. Kavraki, Hadas Kress-Gazit, Moshe Y. Vardi
2016	A*	`conf`	LTL IJCAI Giuseppe De Giacomo, Moshe Y. Vardi
2016	J	`jnl`	On computing minimal independent support and its applications to sampling and counting. Constraints An Int. J. Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, Moshe Y. Vardi
2016	—	`ed.`	Proceedings of the 4th International Workshop on Strategic Reasoning, SR 2016, New York City, USA, 10th July 2016. SR Alessio Lomuscio, Moshe Y. Vardi
2016	A*	`conf`	Regular Open APIs. KR Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2016	J	`jnl`	Relentful strategic reasoning in alternating-time temporal logic. J. Log. Comput. Fabio Mogavero, Aniello Murano, Moshe Y. Vardi
2016	J	`jnl`	Semantic Acyclicity on Graph Databases. SIAM J. Comput. Pablo Barceló, Miguel Romero, Moshe Y. Vardi
2016	C	`conf`	Solving Parity Games Using an Automata-Based Algorithm. CIAA Antonio Di Stasio, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
2016	J	`jnl`	Synthesis with rational environments. Ann. Math. Artif. Intell. Orna Kupferman, Giuseppe Perelli, Moshe Y. Vardi
2016	J	`jnl`	The moral hazard of complexity-theoretic assumptions. Commun. ACM Moshe Y. Vardi
2016	J	`jnl`	The moral imperative of artificial intelligence. Commun. ACM Moshe Y. Vardi
2016	J	`jnl`	The ritual of academic-unit review. Commun. ACM Moshe Y. Vardi
2016	J	`jnl`	Viewpoints on "Logic activities in Europe", twenty years later. Bull. EATCS Luca Aceto, Thomas A. Henzinger, Joost-Pieter Katoen, Wolfgang Thomas, Moshe Y. Vardi
2015	J	`jnl`	Approximate Probabilistic Inference via Word-Level Counting. CoRR Supratik Chakraborty, Kuldeep S. Meel, Rakesh Mistry, Moshe Y. Vardi
2015	J	`jnl`	Constrained Sampling and Counting: Universal Hashing Meets SAT Solving. CoRR Kuldeep S. Meel, Moshe Y. Vardi, Supratik Chakraborty, Daniel J. Fremont, Sanjit A. Seshia, Dror Fried, Alexander Ivrii, Sharad Malik
2015	—	`conf`	Controller Synthesis for Mode-Target Games. ADHS Ayca Balkan, Moshe Y. Vardi, Paulo Tabuada
2015	J	`jnl`	Controller Synthesis for Mode-Target Games. CoRR Ayca Balkan, Moshe Y. Vardi, Paulo Tabuada
2015	A*	`conf`	From Weighted to Unweighted Model Counting. IJCAI Supratik Chakraborty, Dror Fried, Kuldeep S. Meel, Moshe Y. Vardi
2015	—	`conf`	Humans, machines, and the future of work. Ada Lovelace Symposium Moshe Y. Vardi
2015	J	`jnl`	Incentivizing quality and impact in computing research. Commun. ACM Moshe Y. Vardi
2015	J	`jnl`	Is information technology destroying the middle class? Commun. ACM Moshe Y. Vardi
2015	J	`jnl`	Node Selection Query Languages for Trees. CoRR Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2015	A	`conf`	On Parallel Scalable Uniform SAT Witness Generation. TACAS Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
2015	J	`jnl`	On lethal autonomous weapons. Commun. ACM Moshe Y. Vardi
2015	J	`jnl`	Profile trees for Büchi word automata, with application to determinization. Inf. Comput. Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, Thomas Wilke
2015	A	`conf`	Regular Queries on Graph Databases. ICDT Juan L. Reutter, Miguel Romero, Moshe Y. Vardi
2015	—	`conf`	SAT-Based Explicit LTL Reasoning. Haifa Verification Conference Jianwen Li, Shufang Zhu, Geguang Pu, Moshe Y. Vardi
2015	J	`jnl`	SAT-based Explicit LTL Reasoning. CoRR Jianwen Li, Shufang Zhu, Geguang Pu, Moshe Y. Vardi
2015	J	`jnl`	Special issue on SR 2013. Inf. Comput. Fabio Mogavero, Aniello Murano, Moshe Y. Vardi
2015	A*	`conf`	Synthesis for LTL and LDL on Finite Traces. IJCAI Giuseppe De Giacomo, Moshe Y. Vardi
2015	—	`conf`	The Complexity of Synthesis from Probabilistic Components. ICALP (2) Krishnendu Chatterjee, Laurent Doyen, Moshe Y. Vardi
2015	J	`jnl`	The Complexity of Synthesis from Probabilistic Components. CoRR Krishnendu Chatterjee, Laurent Doyen, Moshe Y. Vardi
2015	J	`jnl`	The rise and fall of industrial research labs. Commun. ACM Moshe Y. Vardi
2015	J	`jnl`	Theory in practice for system design and verification. ACM SIGLOG News Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi
2015	A*	`conf`	This Time the Robot Settles for a Cost: A Quantitative Approach to Temporal Logic Planning with Partial Satisfaction. AAAI Morteza Lahijanian, Shaull Almagor, Dror Fried, Lydia E. Kavraki, Moshe Y. Vardi
2015	A*	`conf`	Towards manipulation planning with temporal logic specifications. ICRA Keliang He, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2015	J	`jnl`	What can be done about gender diversity in computing?: a lot! Commun. ACM Moshe Y. Vardi
2015	J	`jnl`	What do we do when the jobs are gone, and why we must embrace active learning. Commun. ACM Moshe Y. Vardi, Mark Guzdial
2015	J	`jnl`	Why doesn't ACM have a SIG for theoretical computer science? Commun. ACM Moshe Y. Vardi
2014	A*	`conf`	A sampling-based strategy planner for nondeterministic hybrid systems. ICRA Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi
2014	C	`conf`	Assertion-based flow monitoring of SystemC models. MEMOCODE Sonali Dutta, Moshe Y. Vardi
2014	A*	`conf`	Balancing Scalability and Uniformity in SAT Witness Generator. DAC Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2014	J	`jnl`	Balancing Scalability and Uniformity in SAT Witness Generator. CoRR Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2014	J	`jnl`	Boolean satisfiability: theory and engineering. Commun. ACM Moshe Y. Vardi
2014	—	`conf`	Bridging the Gap between Supervisory Control and Reactive Synthesis: Case of Full Observation and Centralized Control. WODES Rüdiger Ehlers, Stéphane Lafortune, Stavros Tripakis, Moshe Y. Vardi
2014	J	`jnl`	Design and Synthesis from Components (Dagstuhl Seminar 14232). Dagstuhl Reports Jakob Rehof, Moshe Y. Vardi
2014	A*	`conf`	Distribution-Aware Sampling and Weighted Model Counting for SAT. AAAI Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
2014	J	`jnl`	Distribution-Aware Sampling and Weighted Model Counting for SAT. CoRR Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, Moshe Y. Vardi
2014	A*	`conf`	Does query evaluation tractability help query containment? PODS Pablo Barceló, Miguel Romero, Moshe Y. Vardi
2014	J	`jnl`	Fast LTL Satisfiability Checking by SAT Solvers. CoRR Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y. Vardi, Jifeng He
2014	—	`conf`	From Löwenheim to PSL and SVA. Language, Culture, Computation (1) Moshe Y. Vardi
2014	C	`conf`	From visual to logical formalisms for SoC validation. MEMOCODE Ranan Fraer, Doron Keren, Zurab Khasidashvili, Alexander Novakovsky, Avi Puder, Eli Singerman, Eran Talmor, Moshe Y. Vardi, Jin Yang
2014	A	`conf`	LTLf Satisfiability Checking. ECAI Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, Jifeng He
2014	J	`jnl`	LTLf satisfiability checking. CoRR Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, Jifeng He
2014	J	`jnl`	Moore's law and the sand-heap paradox. Commun. ACM Moshe Y. Vardi
2014	J	`jnl`	Openism, IPism, fundamentalism, and pragmatism. Commun. ACM Moshe Y. Vardi
2014	—	`ed.`	Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014. SR Fabio Mogavero, Aniello Murano, Moshe Y. Vardi
2014	J	`jnl`	Reasoning About Strategies: On the Model-Checking Problem. ACM Trans. Comput. Log. Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
2014	J	`jnl`	Scalable conferences. Commun. ACM Moshe Y. Vardi
2014	J	`jnl`	State of Büchi Complementation. Log. Methods Comput. Sci. Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay
2014	J	`jnl`	Synthesis from Probabilistic Components. Log. Methods Comput. Sci. Sumit Nain, Yoad Lustig, Moshe Y. Vardi
2014	C	`conf`	Synthesis with Rational Environments. EUMAS Orna Kupferman, Giuseppe Perelli, Moshe Y. Vardi
2014	J	`jnl`	The Complexity of Integer Bound Propagation. CoRR Lucas Bordeaux, George Katsirelos, Nina Narodytska, Moshe Y. Vardi
2014	B	`conf`	The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies. FoSSaCS Krishnendu Chatterjee, Laurent Doyen, Sumit Nain, Moshe Y. Vardi
2014	J	`jnl`	The Complexity of Partial-observation Stochastic Parity Games With Finite-memory Strategies. CoRR Krishnendu Chatterjee, Laurent Doyen, Sumit Nain, Moshe Y. Vardi
2014	A*	`conf`	Validation of SoC Firmware-Hardware Flows: Challenges and Solution Directions. DAC Yael Abarbanel, Eli Singerman, Moshe Y. Vardi
2014	J	`jnl`	Would Turing have passed the Turing Test? Commun. ACM Moshe Y. Vardi
2013	A	`conf`	A Scalable Approximate Model Counter. CP Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2013	J	`jnl`	A Scalable Approximate Model Counter. CoRR Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2013	J	`jnl`	A Scalable and Nearly Uniform Generator of SAT Witnesses CoRR Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2013	A*	`conf`	A Scalable and Nearly Uniform Generator of SAT Witnesses. CAV Supratik Chakraborty, Kuldeep S. Meel, Moshe Y. Vardi
2013	—	`conf`	A logical revolution (keynote). ESEC/SIGSOFT FSE Moshe Y. Vardi
2013	—	`conf`	A publication culture in software engineering (panel). ESEC/SIGSOFT FSE Steven Fraser, Luciano Baresi, Jane Cleland-Huang, Carlo A. Furia, Georges Gonthier, Paola Inverardi, Moshe Y. Vardi
2013	—	`conf`	CHIMP: A Tool for Assertion-Based Dynamic Verification of SystemC Models. DIFTS@FMCAD Sonali Dutta, Moshe Y. Vardi, Deian Tabakov
2013	J	`jnl`	Falsification of LTL safety properties in hybrid systems. Int. J. Softw. Tools Technol. Transf. Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2013	J	`jnl`	Fricative computing. Commun. ACM Moshe Y. Vardi
2013	J	`jnl`	Has the innovation cup run dry? Commun. ACM Moshe Y. Vardi
2013	—	`conf`	Iterative temporal motion planning for hybrid systems in partially unknown environments. HSCC Matthew R. Maly, Morteza Lahijanian, Lydia E. Kavraki, Hadas Kress-Gazit, Moshe Y. Vardi
2013	C	`conf`	LTL Satisfiability Checking Revisited. TIME Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, Jifeng He
2013	A*	`conf`	Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. IJCAI Giuseppe De Giacomo, Moshe Y. Vardi
2013	J	`jnl`	On simplification of schema mappings. J. Comput. Syst. Sci. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2013	J	`jnl`	Polsat: A Portfolio LTL Satisfiability Solver. CoRR Jianwen Li, Geguang Pu, Lijun Zhang, Yinbo Yao, Moshe Y. Vardi, Jifeng He
2013	—	`ed.`	Proceedings 1st International Workshop on Strategic Reasoning, SR 2013, Rome, Italy, March 16-17, 2013. SR Fabio Mogavero, Aniello Murano, Moshe Y. Vardi
2013	—	`conf`	Profile Trees for Büchi Word Automata, with Application to Determinization. GandALF Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, Thomas Wilke
2013	J	`jnl`	Pushdown module checking with imperfect information. Inf. Comput. Benjamin Aminof, Axel Legay, Aniello Murano, Olivier Serre, Moshe Y. Vardi
2013	A*	`conf`	Regular Real Analysis. LICS Swarat Chaudhuri, Sriram Sankaranarayanan, Moshe Y. Vardi
2013	A*	`conf`	Semantic acyclicity on graph databases. PODS Pablo Barceló Baeza, Miguel Romero, Moshe Y. Vardi
2013	A*	`conf`	Solving Partial-Information Stochastic Parity Games. LICS Sumit Nain, Moshe Y. Vardi
2013	J	`jnl`	Synthesis from Knowledge-Based Specifications. CoRR Ron van der Meyden, Moshe Y. Vardi
2013	J	`jnl`	Synthesis from component libraries. Int. J. Softw. Tools Technol. Transf. Yoad Lustig, Moshe Y. Vardi
2013	J	`jnl`	The end of the American network. Commun. ACM Moshe Y. Vardi
2013	J	`jnl`	The great robotics debate. Commun. ACM Moshe Y. Vardi
2013	J	`jnl`	To boycott or not to boycott. Commun. ACM Moshe Y. Vardi
2013	J	`jnl`	Unifying Büchi Complementation Constructions Log. Methods Comput. Sci. Seth Fogarty, Orna Kupferman, Thomas Wilke, Moshe Y. Vardi
2013	J	`jnl`	What is a flagship publication? Commun. ACM Moshe Y. Vardi, Victor Vianu
2013	J	`jnl`	Who begat computing? Commun. ACM Moshe Y. Vardi
2012	J	`jnl`	2010 CAV award announcement. Formal Methods Syst. Des. Orna Grumberg, Moshe Y. Vardi, Joseph Sifakis, Rajeev Alur
2012	J	`jnl`	2011 CAV award announcement. Formal Methods Syst. Des. Moshe Y. Vardi, Thomas A. Henzinger, Rajeev Alur, Marta Z. Kwiatkowska
2012	J	`jnl`	A Decidable Fragment of Strategy Logic CoRR Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
2012	J	`jnl`	Artificial intelligence: past and future. Commun. ACM Moshe Y. Vardi
2012	—	`conf`	Automatic aspectization of systemC. MISS@AOSD Deian Tabakov, Moshe Y. Vardi
2012	A*	`conf`	Bma: Visual Tool for Modeling and Analyzing Biological Networks. CAV David Benqué, Sam Bourton, Caitlin Cockerton, Byron Cook, Jasmin Fisher, Samin Ishtiaq, Nir Piterman, Alex S. Taylor, Moshe Y. Vardi
2012	J	`jnl`	Büchi Complementation and Size-Change Termination Log. Methods Comput. Sci. Seth Fogarty, Moshe Y. Vardi
2012	—	`conf`	Compositional Temporal Synthesis. QEST Moshe Y. Vardi
2012	—	`conf`	Deterministic Compilation of Temporal Safety Properties in Explicit State Model Checking. Haifa Verification Conference Kristin Yvonne Rozier, Moshe Y. Vardi
2012	J	`jnl`	Fair access. Commun. ACM Moshe Y. Vardi
2012	J	`jnl`	Once and for all. J. Comput. Syst. Sci. Orna Kupferman, Amir Pnueli, Moshe Y. Vardi
2012	J	`jnl`	Optimized temporal monitors for SystemC. Formal Methods Syst. Des. Deian Tabakov, Kristin Y. Rozier, Moshe Y. Vardi
2012	J	`jnl`	Predatory scholarly publishing. Commun. ACM Moshe Y. Vardi
2012	J	`jnl`	Publication Culture in Computing Research (Dagstuhl Perspectives Workshop 12452). Dagstuhl Reports Kurt Mehlhorn, Moshe Y. Vardi, Marc Herbstritt
2012	J	`jnl`	Query Processing under GLAV Mappings for Relational and Graph Databases. Proc. VLDB Endow. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2012	B	`conf`	Synthesizing Probabilistic Composers. FoSSaCS Sumit Nain, Moshe Y. Vardi
2012	J	`jnl`	Temporal property verification as a program analysis task - Extended Version. Formal Methods Syst. Des. Byron Cook, Eric Koskinen, Moshe Y. Vardi
2012	B	`conf`	What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic. CONCUR Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
2012	J	`jnl`	What is an algorithm? Commun. ACM Moshe Y. Vardi
2012	J	`jnl`	Why ACM? Commun. ACM Moshe Y. Vardi
2012	J	`jnl`	Will MOOCs destroy academia? Commun. ACM Moshe Y. Vardi
2011	B	`conf`	A Multi-encoding Approach for LTL Symbolic Satisfiability Checking. FM Kristin Y. Rozier, Moshe Y. Vardi
2011	J	`jnl`	Are you talking to me? Commun. ACM Moshe Y. Vardi
2011	B	`conf`	Branching vs. Linear Time: Semantical Perspective. CSL Moshe Y. Vardi
2011	J	`jnl`	Computing for humans. Commun. ACM Moshe Y. Vardi
2011	—	`conf`	Constraints, Graphs, Algebra, Logic, and Complexity (Invited Talk). FSTTCS Moshe Y. Vardi
2011	B	`conf`	Dynamic Reactive Modules. CONCUR Jasmin Fisher, Thomas A. Henzinger, Dejan Nickovic, Nir Piterman, Anmol V. Singh, Moshe Y. Vardi
2011	J	`jnl`	Fumbling the future. Commun. ACM Moshe Y. Vardi
2011	J	`jnl`	Is Moore's Party over? Commun. ACM Moshe Y. Vardi
2011	J	`jnl`	Modeling, Analysis, and Verification - The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482). Dagstuhl Manifestos Jörg Kreiker, Andrzej Tarlecki, Moshe Y. Vardi, Reinhard Wilhelm
2011	J	`jnl`	Motion Planning with Complex Goals. IEEE Robotics Autom. Mag. Amit Bhatia, Matthew R. Maly, Lydia E. Kavraki, Moshe Y. Vardi
2011	J	`jnl`	Reasoning About Strategies: On the Model-Checking Problem CoRR Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
2011	A	`conf`	Simplifying schema mappings. ICDT Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2011	J	`jnl`	Solving the unsolvable. Commun. ACM Moshe Y. Vardi
2011	J	`jnl`	Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. Int. J. Softw. Tools Technol. Transf. Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
2011	B	`conf`	Synthesis from Probabilistic Components. CSL Yoad Lustig, Sumit Nain, Moshe Y. Vardi
2011	—	`conf`	Synthesis from Recursive-Components Libraries GandALF Yoad Lustig, Moshe Y. Vardi
2011	J	`jnl`	Technology has social consequences. Commun. ACM Moshe Y. Vardi
2011	A*	`conf`	Temporal Property Verification as a Program Analysis Task. CAV Byron Cook, Eric Koskinen, Moshe Y. Vardi
2011	A	`conf`	Temporal Synthesis for Bounded Systems and Environments. STACS Orna Kupferman, Yoad Lustig, Moshe Y. Vardi, Mihalis Yannakakis
2011	J	`jnl`	The Complexity of Integer Bound Propagation. J. Artif. Intell. Res. Lucas Bordeaux, George Katsirelos, Nina Narodytska, Moshe Y. Vardi
2011	B	`conf`	The Only Way Is Up. FM Jasmin Fisher, Nir Piterman, Moshe Y. Vardi
2011	J	`jnl`	The Planning Spectrum - One, Two, Three, Infinity CoRR Marco Pistore, Moshe Y. Vardi
2011	B	`conf`	Unifying Büchi Complementation Constructions. CSL Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, Thomas Wilke
2011	J	`jnl`	Where have all the workshops gone? Commun. ACM Moshe Y. Vardi
2010	J	`jnl`	2009 CAV award announcement. Formal Methods Syst. Des. Randal E. Bryant, Orna Grumberg, Joseph Sifakis, Moshe Y. Vardi
2010	—	`conf`	An Automata-Theoretic Approach to Infinite-State Systems. Essays in Memory of Amir Pnueli Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2010	A	`conf`	Constraints, Graphs, Algebra, Logic, and Complexity. CP Moshe Y. Vardi
2010	A	`conf`	Efficient Büchi Universality Checking. TACAS Seth Fogarty, Moshe Y. Vardi
2010	A*	`conf`	From Automated Verification to Automated Design. ICAPS Moshe Y. Vardi
2010	J	`jnl`	Hypercriticality. Commun. ACM Moshe Y. Vardi
2010	J	`jnl`	LTL satisfiability checking. Int. J. Softw. Tools Technol. Transf. Kristin Y. Rozier, Moshe Y. Vardi
2010	C	`conf`	Monitoring temporal SystemC properties. MEMOCODE Deian Tabakov, Moshe Y. Vardi
2010	J	`jnl`	More debate, please! Commun. ACM Moshe Y. Vardi
2010	J	`jnl`	Motion Planning With Dynamics by a Synergistic Combination of Layers of Planning. IEEE Trans. Robotics Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2010	—	`conf`	Motion planning with hybrid dynamics and temporal goals. CDC Amit Bhatia, Lydia E. Kavraki, Moshe Y. Vardi
2010	A*	`conf`	Node Selection Query Languages for Trees. AAAI Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2010	J	`jnl`	On P, NP, and computational complexity. Commun. ACM Moshe Y. Vardi
2010	B	`conf`	Optimized temporal monitors for SystemC. RV Deian Tabakov, Moshe Y. Vardi
2010	—	`conf`	Reasoning About Strategies. FSTTCS Fabio Mogavero, Aniello Murano, Moshe Y. Vardi
2010	—	`conf`	Relentful Strategic Reasoning in Alternating-Time Temporal Logic. LPAR (Dakar) Fabio Mogavero, Aniello Murano, Moshe Y. Vardi
2010	J	`jnl`	Revisiting the publication culture in computing research. Commun. ACM Moshe Y. Vardi
2010	A*	`conf`	Sampling-based motion planning with temporal goals. ICRA Amit Bhatia, Lydia E. Kavraki, Moshe Y. Vardi
2010	J	`jnl`	Science has only two legs. Commun. ACM Moshe Y. Vardi
2010	C	`conf`	State of Büchi Complementation. CIAA Ming-Hsien Tsai, Seth Fogarty, Moshe Y. Vardi, Yih-Kuen Tsay
2010	—	`conf`	Synthesis of Trigger Properties. LPAR (Dakar) Orna Kupferman, Moshe Y. Vardi
2010	J	`jnl`	View Synthesis from Schema Mappings CoRR Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2009	J	`jnl`	"Yes, it can be done". Commun. ACM Moshe Y. Vardi
2009	—	`conf`	An Automata-Theoretic Approach to Regular XPath. DBPL Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2009	A	`conf`	Büchi Complementation and Size-Change Termination. TACAS Seth Fogarty, Moshe Y. Vardi
2009	J	`jnl`	Conferences vs. journals in computing research. Commun. ACM Moshe Y. Vardi
2009	C	`conf`	Constraints, Graphs, Algebra, Logic, and Complexity. TAMC Moshe Y. Vardi
2009	A	`conf`	Falsification of LTL Safety Properties in Hybrid Systems. TACAS Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2009	—	`conf`	From Philosophical to Industrial Logics. ICLA Moshe Y. Vardi
2009	J	`jnl`	From liveness to promptness. Formal Methods Syst. Des. Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2009	J	`jnl`	How are we doing? Commun. ACM Moshe Y. Vardi
2009	J	`jnl`	Hybrid systems: from verification to falsification by combining motion planning and discrete search. Formal Methods Syst. Des. Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2009	J	`jnl`	Intelligate: An Algorithm for Learning Boolean Functions for Dynamic Power Reduction. J. Low Power Electron. Roni Wiener, Gila Kamhi, Moshe Y. Vardi
2009	J	`jnl`	Is the image crisis over? Commun. ACM Moshe Y. Vardi
2009	—	`conf`	Model Checking as A Reachability Problem. RP Moshe Y. Vardi
2009	J	`jnl`	Open, closed, or clopen access? Commun. ACM Moshe Y. Vardi
2009	A	`conf`	Symbolic Techniques in Propositional Satisfiability Solving. SAT Moshe Y. Vardi
2009	B	`conf`	Synthesis from Component Libraries. FoSSaCS Yoad Lustig, Moshe Y. Vardi
2009	J	`jnl`	The 2008 CAV Award citation. Formal Methods Syst. Des. Randal E. Bryant, Orna Grumberg, Thomas A. Henzinger, Moshe Y. Vardi
2009	J	`jnl`	The financial meltdown and computing. Commun. ACM Moshe Y. Vardi
2009	A*	`conf`	Trace Semantics is Fully Abstract. LICS Sumit Nain, Moshe Y. Vardi
2008	J	`jnl`	"Where do you come from? and where are you going?". Commun. ACM Moshe Y. Vardi
2008	—	`conf`	A Framework for Inherent Vacuity. Haifa Verification Conference Dana Fisman, Orna Kupferman, Sarai Sheinvald-Faragy, Moshe Y. Vardi
2008	—	`conf`	A Logical Approach to Constraint Satisfaction. Complexity of Constraints Phokion G. Kolaitis, Moshe Y. Vardi
2008	B	`conf`	A Temporal Language for SystemC. FMCAD Deian Tabakov, Gila Kamhi, Moshe Y. Vardi, Eli Singerman
2008	—	`ed.`	Algorithmic-Logical Theory of Infinite Structures, 28.10. - 02.11.2007 Algorithmic-Logical Theory of Infinite Structures Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, Moshe Y. Vardi
2008	—	`conf`	Automata-Theoretic Model Checking Revisited. Haifa Verification Conference Moshe Y. Vardi
2008	—	`conf`	Automata: from logics to algorithms. Logic and Automata Moshe Y. Vardi, Thomas Wilke
2008	J	`jnl`	CACM: past, present, and future. Commun. ACM Moshe Y. Vardi
2008	—	`conf`	From Church and Prior to PSL. 25 Years of Model Checking Moshe Y. Vardi
2008	—	`conf`	From Monadic Logic to PSL. Pillars of Computer Science Moshe Y. Vardi
2008	—	`conf`	From Verification to Synthesis. VSTTE Moshe Y. Vardi
2008	A*	`conf`	Impact of workspace decompositions on discrete search leading continuous exploration (DSLX) motion planning. ICRA Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2008	—	`conf`	Intelligate: Scalable Dynamic Invariant Learning for Power Reduction. PATMOS Roni Wiener, Gila Kamhi, Moshe Y. Vardi
2008	J	`jnl`	Let us---together---make CACM exciting. Commun. ACM Moshe Y. Vardi
2008	J	`jnl`	Multi-Objective Model Checking of Markov Decision Processes CoRR Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis
2008	J	`jnl`	Multi-Objective Model Checking of Markov Decision Processes. Log. Methods Comput. Sci. Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis
2008	—	`conf`	Open Implication. ICALP (2) Karin Greimel, Roderick Bloem, Barbara Jobstmann, Moshe Y. Vardi
2008	J	`jnl`	The Complexity of Enriched Mu-Calculi CoRR Piero A. Bonatti, Carsten Lutz, Aniello Murano, Moshe Y. Vardi
2008	J	`jnl`	The Complexity of Enriched Mu-Calculi. Log. Methods Comput. Sci. Piero A. Bonatti, Carsten Lutz, Aniello Murano, Moshe Y. Vardi
2007	—	`conf`	07441 Abstracts Collection -- Algorithmic-Logical Theory of Infinite Structures. Algorithmic-Logical Theory of Infinite Structures Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, Moshe Y. Vardi
2007	—	`conf`	07441 Summary -- Algorithmic-Logical Theory of Infinite Structures. Algorithmic-Logical Theory of Infinite Structures Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, Moshe Y. Vardi
2007	A*	`conf`	A Motion Planner for a Hybrid Robotic System with Kinodynamic Constraints. ICRA Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2007	J	`jnl`	A continuous-discontinuous second-order transition in the satisfiability of random Horn-SAT formulas. Random Struct. Algorithms Cristopher Moore, Gabriel Istrate, Demetrios D. Demopoulos, Moshe Y. Vardi
2007	A	`conf`	An Analysis of Slow Convergence in Interval Propagation. CP Lucas Bordeaux, Youssef Hamadi, Moshe Y. Vardi
2007	B	`conf`	Automata-Theoretic Model Checking Revisited. VMCAI Moshe Y. Vardi
2007	—	`ch.`	Automata-theoretic techniques for temporal reasoning. Handbook of Modal Logic Moshe Y. Vardi
2007	B	`conf`	Branching vs. Linear Time: Semantical Perspective. ATVA Sumit Nain, Moshe Y. Vardi
2007	—	`conf`	Deeper Bound in BMC by Combining Constant Propagation and Abstraction. ASP-DAC Roy Armoni, Limor Fix, Ranan Fraer, Tamir Heyman, Moshe Y. Vardi, Yakir Vizel, Yael Zbar
2007	—	`conf`	Discrete Search Leading Continuous Exploration for Kinodynamic Motion Planning. Robotics: Science and Systems Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2007	—	`book`	Finite Model Theory and Its Applications Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, Scott Weinstein
2007	A*	`conf`	Formal Techniques for SystemC Verification; Position Paper. DAC Moshe Y. Vardi
2007	A*	`conf`	From Liveness to Promptness. CAV Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2007	J	`jnl`	GSTE is partitioned model checking. Formal Methods Syst. Des. Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi
2007	A*	`conf`	Hybrid Systems: From Verification to Falsification. CAV Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi
2007	A	`conf`	Interactive presentation: PowerQuest: trace driven data mining for power optimization. DATE Pietro Babighian, Gila Kamhi, Moshe Y. Vardi
2007	—	`conf`	LTL Satisfiability Checking. SPIN Kristin Y. Rozier, Moshe Y. Vardi
2007	C	`conf`	Linear-Time Model Checking: Automata Theory in Practice. CIAA Moshe Y. Vardi
2007	C	`conf`	Model Checking Buechi Specifications. LATA Deian Tabakov, Moshe Y. Vardi
2007	A	`conf`	Multi-objective Model Checking of Markov Decision Processes. TACAS Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis
2007	A	`conf`	Property-Driven Partitioning for Abstraction Refinement. TACAS Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
2007	A*	`conf`	Proving that programs eventually do something good. POPL Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, Moshe Y. Vardi
2007	B	`conf`	Pushdown Module Checking with Imperfect Information. CONCUR Benjamin Aminof, Aniello Murano, Moshe Y. Vardi
2007	A	`conf`	The Büchi Complementation Saga. STACS Moshe Y. Vardi
2007	J	`jnl`	The Planning Spectrum - One, Two, Three, Infinity. J. Artif. Intell. Res. Marco Pistore, Moshe Y. Vardi
2007	J	`jnl`	View-based query processing: On the relationship between rewriting, answering and losslessness. Theor. Comput. Sci. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2006	J	`jnl`	Aggregating disparate estimates of chance. Games Econ. Behav. Daniel N. Osherson, Moshe Y. Vardi
2006	A	`conf`	Automata theory: its relevance to computer science students and course contents. SIGCSE Michal Armoni, Susan H. Rodger, Moshe Y. Vardi, Rakesh M. Verma
2006	J	`jnl`	BDD-based decision procedures for the modal logic K. J. Appl. Non Class. Logics Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi
2006	J	`jnl`	Büchi Complementation Made Tighter. Int. J. Found. Comput. Sci. Ehud Friedgut, Orna Kupferman, Moshe Y. Vardi
2006	J	`jnl`	Coverage metrics for formal verification. Int. J. Softw. Tools Technol. Transf. Hana Chockler, Orna Kupferman, Moshe Y. Vardi
2006	J	`jnl`	Coverage metrics for temporal logic model checking Formal Methods Syst. Des. Hana Chockler, Orna Kupferman, Moshe Y. Vardi
2006	—	`conf`	Deterministic Dynamic Monitors for Linear-Time Assertions. FATES/RV Roy Armoni, Dmitry Korchemny, Andreas Tiemeyer, Moshe Y. Vardi, Yael Zbar
2006	A*	`conf`	Fixed-Parameter Hierarchies inside PSPACE. LICS Guoqiang Pan, Moshe Y. Vardi
2006	A*	`conf`	Memoryful Branching-Time Logic. LICS Orna Kupferman, Moshe Y. Vardi
2006	B	`conf`	On Locally Checkable Properties. LPAR Orna Kupferman, Yoad Lustig, Moshe Y. Vardi
2006	J	`jnl`	Relating word and tree automata. Ann. Pure Appl. Log. Orna Kupferman, Shmuel Safra, Moshe Y. Vardi
2006	A*	`conf`	Safraless Compositional Synthesis. CAV Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2006	—	`ed.`	Synthesis and Planning, 12.-17. June 2005 Synthesis and Planning Henry A. Kautz, Wolfgang Thomas, Moshe Y. Vardi
2006	—	`conf`	The Complexity of Enriched ICALP (2) Piero A. Bonatti, Carsten Lutz, Aniello Murano, Moshe Y. Vardi
2006	—	`ch.`	The Phase Transition in the Random HornSAT Problem. Computational Complexity and Statistical Physics Demetrios D. Demopoulos, Moshe Y. Vardi
2006	A	`conf`	educational response to offshore outsourcing. SIGCSE William Aspray, A. Frank Mayadas, Moshe Y. Vardi, Stuart H. Zweben
2005	—	`conf`	05241 Abstracts Collection - Synthesis and Planning. Synthesis and Planning Henry A. Kautz, Wolfgang Thomas, Moshe Y. Vardi
2005	—	`conf`	05241 Executive Summary - Synthesis and Planning. Synthesis and Planning Henry A. Kautz, Wolfgang Thomas, Moshe Y. Vardi
2005	—	`conf`	A Continuous-Discontinuous Second-Order Transition in the Satisfiability of Random Horn-SAT Formulas. APPROX-RANDOM Cristopher Moore, Gabriel Istrate, Demetrios D. Demopoulos, Moshe Y. Vardi
2005	A	`conf`	Complementation Constructions for Nondeterministic Automata on Infinite Words. TACAS Orna Kupferman, Moshe Y. Vardi
2005	J	`jnl`	Decidable containment of recursive queries. Theor. Comput. Sci. Diego Calvanese, Giuseppe De Giacomo, Moshe Y. Vardi
2005	A	`conf`	Efficient LTL compilation for SAT-based model checking. ICCAD Roy Armoni, Sergey Egorov, Ranan Fraer, Dmitry Korchemny, Moshe Y. Vardi
2005	B	`conf`	Experimental Evaluation of Classical Automata Constructions. LPAR Deian Tabakov, Moshe Y. Vardi
2005	A*	`conf`	Formal Verification of Backward Compatibility of Microcode. CAV Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Lenore D. Zuck
2005	J	`jnl`	From complementation to certification. Theor. Comput. Sci. Orna Kupferman, Moshe Y. Vardi
2005	J	`jnl`	From linear time to branching time. ACM Trans. Comput. Log. Orna Kupferman, Moshe Y. Vardi
2005	J	`jnl`	In memory of Seymour Ginsburg 1928 - 2004. SIGMOD Rec. Serge Abiteboul, Richard Hull, Victor Vianu, Sheila A. Greibach, Michael A. Harrison, Ellis Horowitz, Daniel J. Rosenkrantz, Jeffrey D. Ullman, Moshe Y. Vardi
2005	A	`conf`	Model Checking for Database Theoreticians. ICDT Moshe Y. Vardi
2005	—	`conf`	Regular Vacuity. CHARME Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi
2005	A*	`conf`	Safraless Decision Procedures. FOCS Orna Kupferman, Moshe Y. Vardi
2005	A*	`conf`	Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. CAV Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi
2005	J	`jnl`	Symbolic Techniques in Satisfiability Solving. J. Autom. Reason. Guoqiang Pan, Moshe Y. Vardi
2005	B	`conf`	Treewidth in Verification: Local vs. Global. LPAR Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi
2005	A	`conf`	View-Based Query Processing: On the Relationship Between Rewriting, Answering and Losslessness. ICDT Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2004	A	`conf`	A Measured Collapse of the Modal µ-Calculus Alternation Hierarchy. STACS Doron Bustan, Orna Kupferman, Moshe Y. Vardi
2004	B	`conf`	Büchi Complementation Made Tighter. ATVA Ehud Friedgut, Orna Kupferman, Moshe Y. Vardi
2004	J	`jnl`	Complete Axiomatizations for Reasoning about Knowledge and Time. SIAM J. Comput. Joseph Y. Halpern, Ron van der Meyden, Moshe Y. Vardi
2004	A	`conf`	Constraint Propagation as a Proof System. CP Albert Atserias, Phokion G. Kolaitis, Moshe Y. Vardi
2004	A	`conf`	From Complementation to Certification. TACAS Orna Kupferman, Moshe Y. Vardi
2004	A*	`conf`	GSTE Is Partitioned Model Checking. CAV Roberto Sebastiani, Eli Singerman, Stefano Tonetta, Moshe Y. Vardi
2004	A*	`conf`	Global Model-Checking of Infinite-State Systems. CAV Nir Piterman, Moshe Y. Vardi
2004	—	`conf`	Pattern search in hierarchical high-level designs. ICECS Zvi Terem, Gila Kamhi, Moshe Y. Vardi, Amitai Irron
2004	B	`conf`	Projection Pushing Revisited. EDBT Benjamin J. McMahan, Guoqiang Pan, Patrick Porter, Moshe Y. Vardi
2004	—	`conf`	SAT-based Induction for Temporal Safety Properties. BMC@CAV Roy Armoni, Limor Fix, Ranan Fraer, Scott Huddleston, Nir Piterman, Moshe Y. Vardi
2004	A	`conf`	Search vs. Symbolic Techniques in Satisfiability Solving. SAT Guoqiang Pan, Moshe Y. Vardi
2004	—	`conf`	Search vs. Symbolic Techniques in Satisfiability Solving. SAT (Selected Papers Guoqiang Pan, Moshe Y. Vardi
2004	A	`conf`	Symbolic Decision Procedures for QBF. CP Guoqiang Pan, Moshe Y. Vardi
2004	A*	`conf`	Verifying omega-Regular Properties of Markov Chains. CAV Doron Bustan, Sasha Rubin, Moshe Y. Vardi
2003	—	`conf`	A Call to Regularity. PCK50 Moshe Y. Vardi
2003	A*	`conf`	Automated Verification: Graphs, Logic, and Automata. IJCAI Moshe Y. Vardi
2003	—	`conf`	Coverage Metrics for Formal Verification. CHARME Hana Chockler, Orna Kupferman, Moshe Y. Vardi
2003	A	`conf`	Decidable Containment of Recursive Queries. ICDT Diego Calvanese, Giuseppe De Giacomo, Moshe Y. Vardi
2003	A*	`conf`	Enhanced Vacuity Detection in Linear Temporal Logic. CAV Roy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi
2003	—	`conf`	Fair Equivalence Relations. Verification: Theory and Practice Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2003	J	`jnl`	From bidirectionality to alternation. Theor. Comput. Sci. Nir Piterman, Moshe Y. Vardi
2003	A*	`conf`	Homomorphism Closed vs. Existential Positive. LICS Tomás Feder, Moshe Y. Vardi
2003	—	`conf`	In Memoriam: Paris C. Kanellakis. PCK50 Serge Abiteboul, Gabriel M. Kuper, Alexander A. Shvartsman, Moshe Y. Vardi
2003	A*	`conf`	Logic and Automata: A Match Made in Heaven. ICALP Moshe Y. Vardi
2003	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 10th International Conference, LPAR 2003, Almaty, Kazakhstan, September 22-26, 2003, Proceedings LPAR Moshe Y. Vardi, Andrei Voronkov
2003	A*	`conf`	Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems. LICS Nir Piterman, Moshe Y. Vardi
2003	A	`conf`	Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. TACAS Marcelo Glusman, Gila Kamhi, Sela Mador-Haim, Ranan Fraer, Moshe Y. Vardi
2003	—	`conf`	On Complementing Nondeterministic Büchi Automata. CHARME Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, Moshe Y. Vardi
2003	A	`conf`	Optimizing a BDD-Based Modal Solver. CADE Guoqiang Pan, Moshe Y. Vardi
2003	—	`conf`	Query Containment Using Views. SEBD Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2003	J	`jnl`	Random 3-SAT: The Plot Thickens. Constraints An Int. J. Cristian Coarfa, Demetrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika Subramanian, Moshe Y. Vardi
2003	J	`jnl`	Reasoning on regular path queries. SIGMOD Rec. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2003	A	`conf`	Resets vs. Aborts in Linear Temporal Logic. TACAS Roy Armoni, Doron Bustan, Orna Kupferman, Moshe Y. Vardi
2003	A*	`conf`	The Planning Spectrum - One, Two, Three, Infinity. LICS Marco Pistore, Moshe Y. Vardi
2003	J	`jnl`	Vacuity detection in temporal model checking. Int. J. Softw. Tools Technol. Transf. Orna Kupferman, Moshe Y. Vardi
2003	A*	`conf`	View-based query containment. PODS Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2003	A*	`conf`	Π ICALP Orna Kupferman, Moshe Y. Vardi
2002	J	`jnl`	A Rice University perspective on software engineering licensing. Commun. ACM Ken Kennedy, Moshe Y. Vardi
2002	B	`conf`	Alternation. JELIA Moshe Y. Vardi
2002	A	`conf`	BDD-Based Decision Procedures for K. CADE Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi
2002	J	`jnl`	Bisimulation Minimization and Symbolic Model Checking. Formal Methods Syst. Des. Kathi Fisler, Moshe Y. Vardi
2002	J	`jnl`	Black Box Checking. J. Autom. Lang. Comb. Doron A. Peled, Moshe Y. Vardi, Mihalis Yannakakis
2002	J	`jnl`	Complete Axiomatizations for Reasoning About Knowledge and Time CoRR Joseph Y. Halpern, Ron van der Meyden, Moshe Y. Vardi
2002	A	`conf`	Constraint Satisfaction, Bounded Treewidth, and Finite-Variable Logics. CP Víctor Dalmau, Phokion G. Kolaitis, Moshe Y. Vardi
2002	A*	`conf`	Eliminating Incoherence from Subjective Estimates of Chance. KR Randy Batsell, Lyle Brenner, Daniel N. Osherson, Spyros Tsavachidis, Moshe Y. Vardi
2002	J	`jnl`	First-Order Logic with Two Variables and Unary Temporal Logic. Inf. Comput. Kousha Etessami, Moshe Y. Vardi, Thomas Wilke
2002	C	`ed.`	Formal Techniques for Networked and Distributed Systems - FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11-14, 2002, Proceedings FORTE Doron A. Peled, Moshe Y. Vardi
2002	A*	`conf`	Lossless Regular Views. PODS Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2002	A*	`conf`	Model Checking Linear Properties of Prefix-Recognizable Systems. CAV Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2002	—	`conf`	Model Checking: A Complexity-Theoretic Perspective (invited talk). PDMC@CONCUR Moshe Y. Vardi
2002	J	`jnl`	On the Complexity of Verifying Concurrent Transition Systems. Inf. Comput. David Harel, Orna Kupferman, Moshe Y. Vardi
2002	B	`conf`	Pushdown Specifications. LPAR Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2002	A*	`conf`	Reasoning about Actions and Planning in LTL Action Theories. KR Diego Calvanese, Giuseppe De Giacomo, Moshe Y. Vardi
2002	J	`jnl`	Rewriting of Regular Expressions and Regular Path Queries. J. Comput. Syst. Sci. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2002	A	`conf`	The Complexity of the Graded µ-Calculus. CADE Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi
2002	A	`conf`	The ForSpec Temporal Logic: A New Temporal Property-Specification Language. TACAS Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Yael Zbar
2001	J	`jnl`	A New Heuristic for Bad Cycle Detection Using BDDs. Formal Methods Syst. Des. Ronald H. Hardin, Robert P. Kurshan, Sandeep K. Shukla, Moshe Y. Vardi
2001	A*	`conf`	A Practical Approach to Coverage in Model Checking. CAV Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi
2001	A*	`conf`	Benefits of Bounded Model Checking at an Industrial Setting. CAV Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi
2001	A	`conf`	Branching vs. Linear Time: Final Showdown. TACAS Moshe Y. Vardi
2001	A	`conf`	Coverage Metrics for Temporal Logic Model Checking. TACAS Hana Chockler, Orna Kupferman, Moshe Y. Vardi
2001	B	`conf`	Extended Temporal Logic Revisited. CONCUR Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2001	B	`conf`	From Bidirectionality to Alternation. MFCS Nir Piterman, Moshe Y. Vardi
2001	A	`conf`	Is There a Best Symbolic Cycle-Detection Algorithm? TACAS Kathi Fisler, Ranan Fraer, Gila Kamhi, Moshe Y. Vardi, Zijiang Yang
2001	J	`jnl`	Model Checking of Safety Properties. Formal Methods Syst. Des. Orna Kupferman, Moshe Y. Vardi
2001	J	`jnl`	Module Checking. Inf. Comput. Orna Kupferman, Moshe Y. Vardi, Pierre Wolper
2001	B	`conf`	On Bounded Specifications. LPAR Orna Kupferman, Moshe Y. Vardi
2001	B	`conf`	On the Complexity of Parity Word Automata. FoSSaCS Valerie King, Orna Kupferman, Moshe Y. Vardi
2001	J	`jnl`	On the unusual effectiveness of logic in computer science. Bull. Symb. Log. Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, Victor Vianu
2001	A	`conf`	Random 3-SAT and BDDs: The Plot Thickens Further. CP Alfonso San Miguel Aguirre, Moshe Y. Vardi
2001	A*	`conf`	Synthesizing Distributed Systems. LICS Orna Kupferman, Moshe Y. Vardi
2001	A	`conf`	The Hybrid µ-Calculus. IJCAR Ulrike Sattler, Moshe Y. Vardi
2001	J	`jnl`	Towards an Efficient Library for SAT: a Manifesto. Electron. Notes Discret. Math. Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella, Moshe Y. Vardi
2001	J	`jnl`	Verification by Augmented Abstraction: The Automata-Theoretic View. J. Comput. Syst. Sci. Yonit Kesten, Amir Pnueli, Moshe Y. Vardi
2001	—	`conf`	View-Based Query Answering and Query Containment over Semistructured Data. DBPL Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2001	J	`jnl`	Weak alternating automata are not that weak. ACM Trans. Comput. Log. Orna Kupferman, Moshe Y. Vardi
2000	B	`conf`	0-1 Laws for Fragments of Existential Second-Order Logic: A Survey. MFCS Phokion G. Kolaitis, Moshe Y. Vardi
2000	—	`conf`	A Game-Theoretic Approach to Constraint Satisfaction. AAAI/IAAI Phokion G. Kolaitis, Moshe Y. Vardi
2000	A*	`conf`	An Automata-Theoretic Approach to Reasoning about Infinite-State Systems. CAV Orna Kupferman, Moshe Y. Vardi
2000	J	`jnl`	An automata-theoretic approach to branching-time model checking. J. ACM Orna Kupferman, Moshe Y. Vardi, Pierre Wolper
2000	J	`jnl`	An automata-theortetic approach to modular model checking. ACM Trans. Program. Lang. Syst. Orna Kupferman, Moshe Y. Vardi
2000	A*	`conf`	Answering Regular Path Queries Using Views. ICDE Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2000	B	`conf`	Automated Verification = Graphs, Automata, and Logic. CSL Moshe Y. Vardi
2000	J	`jnl`	Conjunctive-Query Containment and Constraint Satisfaction. J. Comput. Syst. Sci. Phokion G. Kolaitis, Moshe Y. Vardi
2000	A*	`conf`	Constraint Satisfaction and Database Theory: a Tutorial. PODS Moshe Y. Vardi
2000	A*	`conf`	Containment of Conjunctive Regular Path Queries with Inverse. KR Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2000	—	`conf`	Fair Equivalence Relations. FSTTCS Orna Kupferman, Nir Piterman, Moshe Y. Vardi
2000	B	`conf`	Open Systems in Reactive Environments: Control and Synthesis. CONCUR Orna Kupferman, P. Madhusudan, P. S. Thiagarajan, Moshe Y. Vardi
2000	A*	`conf`	Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. CAV Ranan Fraer, Gila Kamhi, Barukh Ziv, Moshe Y. Vardi, Limor Fix
2000	A	`conf`	Random 3-SAT: The Plot Thickens. CP Cristian Coarfa, Demetrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika Subramanian, Moshe Y. Vardi
2000	A*	`conf`	View-Based Query Processing and Constraint Satisfaction. LICS Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2000	A*	`conf`	View-Based Query Processing for Regular Path Queries with Inverse. PODS Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2000	—	`conf`	What is Query Rewriting? CIA Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2000	—	`conf`	What is View-Based Query Rewriting? KRDB Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
2000	B	`conf`	µ-Calculus Synthesis. MFCS Orna Kupferman, Moshe Y. Vardi
1999	—	`conf`	Automata-Theoretic Approach to Planning for Temporally Extended Goals. ECP Giuseppe De Giacomo, Moshe Y. Vardi
1999	—	`conf`	Bisimulation and Model Checking. CHARME Kathi Fisler, Moshe Y. Vardi
1999	C	`conf`	Black Box Checking. FORTE Doron A. Peled, Moshe Y. Vardi, Mihalis Yannakakis
1999	J	`jnl`	Church's problem revisited. Bull. Symb. Log. Orna Kupferman, Moshe Y. Vardi
1999	J	`jnl`	Common Knowledge Revisited. Ann. Pure Appl. Log. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1999	—	`conf`	Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting. SMC@FLoC Ranan Fraer, Gila Kamhi, Limor Fix, Moshe Y. Vardi
1999	A*	`conf`	Improved Automata Generation for Linear Temporal Logic. CAV Marco Daniele, Fausto Giunchiglia, Moshe Y. Vardi
1999	A*	`conf`	Model Checking of Safety Properties. CAV Orna Kupferman, Moshe Y. Vardi
1999	—	`conf`	Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach. ARTS Moshe Y. Vardi
1999	—	`conf`	Query Answering Using Views for Data Integration over the Web. WebDB (Informal Proceedings) Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
1999	J	`jnl`	Reminiscences on Influential Papers. SIGMOD Rec. Kenneth A. Ross, Surajit Chaudhuri, Gösta Grahne, H. V. Jagadish, Jan Van den Bussche, Moshe Y. Vardi
1999	A*	`conf`	Rewriting of Regular Expressions and Regular Path Queries. PODS Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
1999	—	`conf`	Rewriting of Regular Path Queries. SEBD Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Moshe Y. Vardi
1999	B	`conf`	Robust Satisfaction. CONCUR Orna Kupferman, Moshe Y. Vardi
1999	—	`conf`	Strong Cyclic Planning Revisited. ECP Marco Daniele, Paolo Traverso, Moshe Y. Vardi
1999	J	`jnl`	The Complexity of Problems on Graphs Represented as OBDDs. Chic. J. Theor. Comput. Sci. Joan Feigenbaum, Sampath Kannan, Moshe Y. Vardi, Mahesh Viswanathan
1999	A	`conf`	The Weakness of Self-Complementation. STACS Orna Kupferman, Moshe Y. Vardi
1999	J	`jnl`	The hierarchical approach to modeling knowledge and common knowledge. Int. J. Game Theory Ronald Fagin, John Geanakoplos, Joseph Y. Halpern, Moshe Y. Vardi
1999	—	`conf`	Vacuity Detection in Temporal Model Checking. CHARME Orna Kupferman, Moshe Y. Vardi
1998	B	`conf`	Alternating Refinement Relations. CONCUR Rajeev Alur, Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi
1998	B	`conf`	Bisimulation Minimization in an Automata-Theoretic Verification Framework. FMCAD Kathi Fisler, Moshe Y. Vardi
1998	J	`jnl`	Common knowledge revisited CoRR Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1998	A	`conf`	Complexity of Problems on Graphs Represented as OBDDs (Extended Abstract). STACS Joan Feigenbaum, Sampath Kannan, Moshe Y. Vardi, Mahesh Viswanathan
1998	J	`jnl`	Computational Model Theory: An Overview. Log. J. IGPL Moshe Y. Vardi
1998	A*	`ed.`	Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings CAV Alan J. Hu, Moshe Y. Vardi
1998	A*	`conf`	Conjunctive-Query Containment and Constraint Satisfaction. PODS Phokion G. Kolaitis, Moshe Y. Vardi
1998	A*	`conf`	Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time. LICS Orna Kupferman, Moshe Y. Vardi
1998	A*	`conf`	Linear vs. Branching Time: A Complexity-Theoretic Perspective. LICS Moshe Y. Vardi
1998	A	`conf`	Panel: logic in the computer science curriculum. SIGCSE Kim B. Bruce, Phokion G. Kolaitis, Daniel Leivant, Moshe Y. Vardi
1998	A*	`conf`	Reasoning about The Past with Two-Way Automata. ICALP Moshe Y. Vardi
1998	—	`conf`	Relating linear and branching model checking. PROCOMET Orna Kupferman, Moshe Y. Vardi
1998	B	`conf`	Sometimes and Not Never Re-revisited: On Branching Versus Linear Time. CONCUR Moshe Y. Vardi
1998	B	`conf`	Synthesis from Knowledge-Based Specifications (Extended Abstract). CONCUR Ron van der Meyden, Moshe Y. Vardi
1998	J	`jnl`	The Computational Structure of Monotone Monadic SNP and Constraint Satisfaction: A Study through Datalog and Group Theory. SIAM J. Comput. Tomás Feder, Moshe Y. Vardi
1998	J	`jnl`	Verification of Fair Transition Systems. Chic. J. Theor. Comput. Sci. Orna Kupferman, Moshe Y. Vardi
1998	A*	`conf`	Weak Alternating Automata and Tree Automata Emptiness. STOC Orna Kupferman, Moshe Y. Vardi
1997	A	`conf`	Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. CADE Moshe Y. Vardi
1997	A*	`conf`	First-Order Logic with Two Variables and Unary Temporal Logic. LICS Kousha Etessami, Moshe Y. Vardi, Thomas Wilke
1997	J	`jnl`	Fixpoint logics, relational machines, and computational complexity. J. ACM Serge Abiteboul, Moshe Y. Vardi, Victor Vianu
1997	J	`jnl`	Knowledge-Based Programs. Distributed Comput. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1997	A*	`conf`	Model Checking and Transitive-Closure Logic. CAV Neil Immerman, Moshe Y. Vardi
1997	—	`conf`	Modular Model Checking. COMPOS Orna Kupferman, Moshe Y. Vardi
1997	A*	`conf`	Module Checking Revisited. CAV Orna Kupferman, Moshe Y. Vardi
1997	B	`conf`	On the Complexity of Verifying Concurrent Transition Systems. CONCUR David Harel, Orna Kupferman, Moshe Y. Vardi
1997	J	`jnl`	On the Equivalence of Recursive and Nonrecursive Datalog Programs. J. Comput. Syst. Sci. Surajit Chaudhuri, Moshe Y. Vardi
1997	J	`jnl`	On the decision problem for two-variable first-order logic. Bull. Symb. Log. Erich Grädel, Phokion G. Kolaitis, Moshe Y. Vardi
1997	J	`jnl`	Reasoning about Knowledge: A Response by the Authors. Minds Mach. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1997	J	`jnl`	Special Selection in Logic in Computer Science. J. Symb. Log. Moshe Y. Vardi
1997	—	`conf`	Verification of Open Systems. FSTTCS Moshe Y. Vardi
1997	—	`conf`	Weak Alternating Automata Are Not That Weak. ISTCS Orna Kupferman, Moshe Y. Vardi
1996	B	`conf`	A Space-Efficient On-the-fly Algorithm for Real-Time Model Checking. CONCUR Thomas A. Henzinger, Orna Kupferman, Moshe Y. Vardi
1996	B	`conf`	Common Knowledge Revisited. TARK Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1996	A*	`conf`	Database Research: Lead, Follow, or Get Out of the Way? - Panel Abstract. ICDE Surajit Chaudhuri, Ashok K. Chandra, Umeshwar Dayal, Jim Gray, Michael Stonebraker, Gio Wiederhold, Moshe Y. Vardi
1996	B	`conf`	Implementing Knowledge-Based Programs. TARK Moshe Y. Vardi
1996	J	`jnl`	In Memoriam Paris C. Kanellakis. ACM Comput. Surv. Serge Abiteboul, Gabriel M. Kuper, Harry G. Mairson, Alexander A. Shvartsman, Moshe Y. Vardi
1996	J	`jnl`	In Memoriam: Paris C. Kanellakis (1953-1995). Inf. Comput. Moshe Y. Vardi
1996	A*	`conf`	In Memoriam: Paris C. Kanellakis. PODS Serge Abiteboul, Gabriel M. Kuper, Christos H. Papadimitriou, Moshe Y. Vardi
1996	A*	`conf`	Module Checking. CAV Orna Kupferman, Moshe Y. Vardi
1996	A*	`conf`	On the Expressive Power of Variable-Confined Logics. LICS Phokion G. Kolaitis, Moshe Y. Vardi
1996	J	`jnl`	Rank Predicates vs. Progress Measures in Concurrent-Program Verification. Chic. J. Theor. Comput. Sci. Moshe Y. Vardi
1996	A*	`conf`	Relating Word and Tree Automata. LICS Orna Kupferman, Shmuel Safra, Moshe Y. Vardi
1996	A*	`conf`	Verification of Fair Transisiton Systems. CAV Orna Kupferman, Moshe Y. Vardi
1996	—	`conf`	Why is Modal Logic So Robustly Decidable? Descriptive Complexity and Finite Models Moshe Y. Vardi
1995	J	`jnl`	A Nonstandard Approach to the Logical Omniscience Problem. Artif. Intell. Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1995	—	`ch.`	Alternating Automata and Program Verification. Computer Science Today Moshe Y. Vardi
1995	A*	`conf`	An Automata-Theoretic Approach to Fair Realizability and Synthesis. CAV Moshe Y. Vardi
1995	—	`conf`	An Automata-Theoretic Approach to Linear Temporal Logic. Banff Higher Order Workshop Moshe Y. Vardi
1995	J	`jnl`	Computing with Infinitary Logic. Theor. Comput. Sci. Serge Abiteboul, Moshe Y. Vardi, Victor Vianu
1995	A	`ed.`	Database Theory - ICDT'95, 5th International Conference, Prague, Czech Republic, January 11-13, 1995, Proceedings ICDT Georg Gottlob, Moshe Y. Vardi
1995	A*	`conf`	Knowledge-Based Programs. PODC Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1995	J	`jnl`	On Monadic NP vs. Monadic co-NP Inf. Comput. Ronald Fagin, Larry J. Stockmeyer, Moshe Y. Vardi
1995	A*	`conf`	On the Complexity of Bounded-Variable Queries. PODS Moshe Y. Vardi
1995	B	`conf`	On the Complexity of Branching Modular Model Checking (Extended Abstract). CONCUR Orna Kupferman, Moshe Y. Vardi
1995	A*	`conf`	On the Complexity of Modular Model Checking LICS Moshe Y. Vardi
1995	J	`jnl`	On the Expressive Power of Datalog: Tools and a Case Study. J. Comput. Syst. Sci. Phokion G. Kolaitis, Moshe Y. Vardi
1995	—	`book`	Reasoning About Knowledge. Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1995	—	`conf`	Simple on-the-fly automatic verification of linear temporal logic. PSTV Rob Gerth, Doron A. Peled, Moshe Y. Vardi, Pierre Wolper
1995	J	`jnl`	Undecidable Boundedness Problems for Datalog Programs. J. Log. Program. Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson, Moshe Y. Vardi
1994	B	`conf`	Algorithmic Knowledge. TARK Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1994	A*	`conf`	An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract). CAV Orna Bernholtz, Moshe Y. Vardi, Pierre Wolper
1994	A*	`conf`	An Operational Semantics for Knowledge Bases. AAAI Ronald Fagin, Joseph Y. Halpern, Yoram Moses, Moshe Y. Vardi
1994	—	`conf`	Nontraditional Applications of Automata Theory. TACS Moshe Y. Vardi
1994	A*	`conf`	On the Complexity of Equivalence between Recursive and Nonrecursive Datalog Programs. PODS Surajit Chaudhuri, Moshe Y. Vardi
1994	J	`jnl`	Reasoning About Infinite Computations Inf. Comput. Moshe Y. Vardi, Pierre Wolper
1993	J	`jnl`	Logical Query Optimization by Proff-Tree Transformation. J. Comput. Syst. Sci. Raghu Ramakrishnan, Yehoshua Sagiv, Jeffrey D. Ullman, Moshe Y. Vardi
1993	A*	`conf`	Monotone monadic SNP and constraint satisfaction. STOC Tomás Feder, Moshe Y. Vardi
1993	—	`conf`	On Monadic NP vs. Monadic co-NP (Extended Abstract). SCT Ronald Fagin, Larry J. Stockmeyer, Moshe Y. Vardi
1993	J	`jnl`	On the Complexity of Queries in the Logical Data Model. Theor. Comput. Sci. Gabriel M. Kuper, Moshe Y. Vardi
1993	A*	`conf`	Optimization of PODS Surajit Chaudhuri, Moshe Y. Vardi
1993	A*	`conf`	Parametric real-time reasoning. STOC Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi
1993	B	`conf`	The Complexity of Set Constraints. CSL Alexander Aiken, Dexter Kozen, Moshe Y. Vardi, Edward L. Wimmers
1993	J	`jnl`	The Logical Data Model. ACM Trans. Database Syst. Gabriel M. Kuper, Moshe Y. Vardi
1993	J	`jnl`	Undecidable Optimization Problems for Database Logic Programs. J. ACM Haim Gaifman, Harry G. Mairson, Yehoshua Sagiv, Moshe Y. Vardi
1992	—	`conf`	Automata Theory for Database Theoreticans. Theoretical Studies in Computer Science Moshe Y. Vardi
1992	A	`conf`	Computing with Infinitary Logic. ICDT Serge Abiteboul, Moshe Y. Vardi, Victor Vianu
1992	A*	`conf`	Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory LICS Phokion G. Kolaitis, Moshe Y. Vardi
1992	—	`conf`	Fixpoint Logics, Relational Machines, and Computational Complexity. SCT Serge Abiteboul, Moshe Y. Vardi, Victor Vianu
1992	A*	`conf`	Infinitary Logic for Computer Science. ICALP Phokion G. Kolaitis, Moshe Y. Vardi
1992	J	`jnl`	Infinitary Logics and 0-1 Laws Inf. Comput. Phokion G. Kolaitis, Moshe Y. Vardi
1992	J	`jnl`	Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods Syst. Des. Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis
1992	A*	`conf`	On the Equivalence of Recursive and Nonrecursive Datalog Programs. PODS Surajit Chaudhuri, Moshe Y. Vardi
1992	A*	`ed.`	Proceedings of the Eleventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June 2-4, 1992, San Diego, California, USA Moshe Y. Vardi, Paris C. Kanellakis
1992	B	`conf`	The Expressive Power of the Kierarchical Approach to Modeling Knowledge and Common Knowledge. TARK Ronald Fagin, John Geanakoplos, Joseph Y. Halpern, Moshe Y. Vardi
1992	J	`jnl`	What Can Machines Know? On the Properties of Knowledge in Distributed Systems. J. ACM Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1992	J	`jnl`	What Is an Inference Rule? J. Symb. Log. Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1991	J	`jnl`	A Model-Theoretic Analysis of Knowledge. J. ACM Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1991	J	`jnl`	Database Logic Programming. J. Log. Program. Moshe Y. Vardi
1991	A*	`conf`	Logic Programs as Types for Logic Programs LICS Thom W. Frühwirth, Ehud Shapiro, Moshe Y. Vardi, Eyal Yardeni
1991	—	`conf`	Model Checking vs. Theorem Proving: A Manifesto. Artificial and Mathematical Theory of Computation Joseph Y. Halpern, Moshe Y. Vardi
1991	A*	`conf`	Model Checking vs. Theorem Proving: A Manifesto. KR Joseph Y. Halpern, Moshe Y. Vardi
1991	A*	`conf`	Tools for Datalog Boundedness. PODS Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson, Moshe Y. Vardi
1991	J	`jnl`	Verification of Concurrent Programs: The Automata-Theoretic Framework. Ann. Pure Appl. Log. Moshe Y. Vardi
1990	J	`jnl`	0-1 Laws and Decision Problems for Fragments of Second-Order Logic Inf. Comput. Phokion G. Kolaitis, Moshe Y. Vardi
1990	A*	`conf`	0-1 Laws for Infinitary Logics (Preliminary Report) LICS Phokion G. Kolaitis, Moshe Y. Vardi
1990	B	`conf`	A Nonstandard Approach to the Logical Omniscience Problem. TARK Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1990	J	`jnl`	Endmarkers can Make a Difference. Inf. Process. Lett. Moshe Y. Vardi
1990	B	`conf`	Global Optimization Problems for Database Logic Programs. ICLP Moshe Y. Vardi
1990	A*	`conf`	Memory Efficient Algorithms for the Verification of Temporal Properties. CAV Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis
1990	—	`conf`	Memory Efficient Algorithms for the Verification of Temporal Properties. CAV (DIMACS/AMS volume) Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper, Mihalis Yannakakis
1990	A*	`conf`	On the Expressive Power of Datalog: Tools and a Case Study. PODS Phokion G. Kolaitis, Moshe Y. Vardi
1990	A*	`conf`	On the Power of Bounded Concurrency~III: Reasoning About Programs (Preliminary Report) LICS David Harel, Roni Rosner, Moshe Y. Vardi
1990	J	`jnl`	Polynomial-Time Implication Problems for Unary Inclusion Dependencies J. ACM Stavros S. Cosmadakis, Paris C. Kanellakis, Moshe Y. Vardi
1990	—	`conf`	What is an inference rule? Jerusalem Conference on Information Technology Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1989	J	`jnl`	A Note on the Reduction of Two-Way Automata to One-Way Automata. Inf. Process. Lett. Moshe Y. Vardi
1989	A*	`conf`	Automata Theory for Database Theoreticans. PODS Moshe Y. Vardi
1989	A*	`conf`	On omega-Automata and Temporal Logic (Preliminary Report) STOC Shmuel Safra, Moshe Y. Vardi
1989	A*	`conf`	On the Complexity of Epistemic Reasoning LICS Moshe Y. Vardi
1989	A*	`conf`	Proof-Tree Transformation Theorems and Their Applications. PODS Raghu Ramakrishnan, Yehoshua Sagiv, Jeffrey D. Ullman, Moshe Y. Vardi
1989	A*	`conf`	Safety of Datalog Queries over Infinite Databases. PODS Yehoshua Sagiv, Moshe Y. Vardi
1989	J	`jnl`	The Complexity of Reasoning about Knowledge and Time. I. Lower Bounds. J. Comput. Syst. Sci. Joseph Y. Halpern, Moshe Y. Vardi
1988	A*	`conf`	0-1 Laws and Decision Problems for Fragments of Second-Order Logic LICS Phokion G. Kolaitis, Moshe Y. Vardi
1988	A*	`conf`	A Temporal Fixpoint Calculus. POPL Moshe Y. Vardi
1988	—	`conf`	An Automata-Theoretic Approach to Protocol Verification (Abstract). Concurrency Moshe Y. Vardi
1988	—	`conf`	Database Logic Programming, Deductive Databases, and Expert Database Systems. SIGMOD Conference Moshe Y. Vardi
1988	A*	`conf`	Decidability and Undecidability Results for Boundedness of Linear Recursive Queries. PODS Moshe Y. Vardi
1988	A*	`conf`	Decidable Optimization Problems for Database Logic Programs (Preliminary Report) STOC Stavros S. Cosmadakis, Haim Gaifman, Paris C. Kanellakis, Moshe Y. Vardi
1988	A	`conf`	On the Complexity of Queries in the Logical Data Model (Extended Abstract). ICDT Gabriel M. Kuper, Moshe Y. Vardi
1988	B	`ed.`	Proceedings of the 2nd Conference on Theoretical Aspects of Reasoning about Knowledge, Pacific Grove, CA, USA, March 1988 TARK Moshe Y. Vardi
1988	A*	`conf`	Reasoning about Knowledge and Time in Asynchronous Systems STOC Joseph Y. Halpern, Moshe Y. Vardi
1988	J	`jnl`	Response to a Letter to the Editor. IEEE Softw. Moshe Y. Vardi
1988	A*	`conf`	The Complexity of Ordering Subgoals. PODS Jeffrey D. Ullman, Moshe Y. Vardi
1988	J	`jnl`	The Universal-Relation Data Model for Logical Independence. IEEE Softw. Moshe Y. Vardi
1987	A*	`ed.`	Proceedings of the Sixth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, March 23-25, 1987, San Diego, California, USA Moshe Y. Vardi
1987	J	`jnl`	The Complementation Problem for Büchi Automata with Appplications to Temporal Logic. Theor. Comput. Sci. A. Prasad Sistla, Moshe Y. Vardi, Pierre Wolper
1987	A*	`conf`	The Decision Problem for the Probabilities of Higher-Order Properties STOC Phokion G. Kolaitis, Moshe Y. Vardi
1987	A*	`conf`	Undecidable Optimization Problems for Database Logic Programs LICS Haim Gaifman, Harry G. Mairson, Yehoshua Sagiv, Moshe Y. Vardi
1987	—	`conf`	Unified Verification Theory. Temporal Logic in Specification Moshe Y. Vardi
1987	A*	`conf`	Verification of Concurrent Programs: The Automata-Theoretic Framework LICS Moshe Y. Vardi
1986	A*	`conf`	An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) LICS Moshe Y. Vardi, Pierre Wolper
1986	J	`jnl`	Automata-Theoretic Techniques for Modal Logics of Programs. J. Comput. Syst. Sci. Moshe Y. Vardi, Pierre Wolper
1986	B	`conf`	Knowledge and Implicit Knowledge in a Distributed Environment: Preliminary Report. TARK Ronald Fagin, Moshe Y. Vardi
1986	J	`jnl`	Notions of dependency satisfaction. J. ACM Marc H. Graham, Alberto O. Mendelzon, Moshe Y. Vardi
1986	B	`conf`	On Epistemic Logic and Logical Omniscience. TARK Moshe Y. Vardi
1986	J	`jnl`	On the Expressive Power of Data Dependencies. Acta Informatica Johann A. Makowsky, Moshe Y. Vardi
1986	A*	`conf`	On the Integrity of Databases with Incomplete Information. PODS Moshe Y. Vardi
1986	J	`jnl`	Querying Logical Databases. J. Comput. Syst. Sci. Moshe Y. Vardi
1986	A*	`conf`	Reasoning about Fair Concurrent Programs STOC Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper
1986	A*	`conf`	The Complexity of Reasoning about Knowledge and Time: Extended Abstract STOC Joseph Y. Halpern, Moshe Y. Vardi
1986	J	`jnl`	Updating Logical Databases. Adv. Comput. Res. Ronald Fagin, Gabriel M. Kuper, Jeffrey D. Ullman, Moshe Y. Vardi
1986	A*	`conf`	What Can Machines Know? On the Epistemic Properties of Machines. AAAI Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1985	A*	`conf`	A Model-Theoretic Analysis of Monotonic Knowledge. IJCAI Moshe Y. Vardi
1985	J	`jnl`	A responce to "A complete axiomatisation for full join dependencies in relations". Bull. EATCS Moshe Y. Vardi
1985	J	`jnl`	A simple proof that connectivity of finite graphs is not first-order definable. Bull. EATCS Haim Gaifman, Moshe Y. Vardi
1985	A*	`conf`	An Internal Semantics for Modal Logic: Preliminary Report STOC Ronald Fagin, Moshe Y. Vardi
1985	A*	`conf`	Automatic Verification of Probabilistic Concurrent Finite-State Programs FOCS Moshe Y. Vardi
1985	J	`jnl`	Formal Systems for Join Dependencies. Theor. Comput. Sci. Catriel Beeri, Moshe Y. Vardi
1985	A*	`conf`	Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report STOC Moshe Y. Vardi, Larry J. Stockmeyer
1985	—	`conf`	On the Expressive Power of the Logical Data Model (Preliminary Report). SIGMOD Conference Gabriel M. Kuper, Moshe Y. Vardi
1985	A*	`conf`	Querying Logical Databases. PODS Moshe Y. Vardi
1985	A*	`conf`	The Complementation Problem for Büchi Automata with Applications to Temporal Logic (Extended Abstract). ICALP A. Prasad Sistla, Moshe Y. Vardi, Pierre Wolper
1985	J	`jnl`	The Implication Problem for Functional and Inclusion Dependencies is Undecidable. SIAM J. Comput. Ashok K. Chandra, Moshe Y. Vardi
1985	—	`conf`	The Taming of Converse: Reasoning about Two-way Computations. Logic of Programs Moshe Y. Vardi
1984	A*	`conf`	A Model-Theoretic Analysis of Knowledge: Preliminary Report FOCS Ronald Fagin, Joseph Y. Halpern, Moshe Y. Vardi
1984	A*	`conf`	A New Approach to Database Logic. PODS Gabriel M. Kuper, Moshe Y. Vardi
1984	J	`jnl`	A Note on Lossless Database Decompositions. Inf. Process. Lett. Moshe Y. Vardi
1984	J	`jnl`	A Proof Procedure for Data Dependencies. J. ACM Catriel Beeri, Moshe Y. Vardi
1984	A*	`conf`	Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract) STOC Moshe Y. Vardi, Pierre Wolper
1984	J	`jnl`	Formal Systems for Tuple and Equality Generating Dependencies. SIAM J. Comput. Catriel Beeri, Moshe Y. Vardi
1984	J	`jnl`	On Acyclic Database Decompositions Inf. Control. Catriel Beeri, Moshe Y. Vardi
1984	A*	`conf`	On the Complexity and Axiomatizability of Consistent Database States. PODS Marc H. Graham, Moshe Y. Vardi
1984	A*	`conf`	On the Equivalence of Logical Databases. PODS Gabriel M. Kuper, Jeffrey D. Ullman, Moshe Y. Vardi
1984	J	`jnl`	On the Foundations of the Universal Relation Model. ACM Trans. Database Syst. David Maier, Jeffrey D. Ullman, Moshe Y. Vardi
1984	J	`jnl`	The Implication and Finite Implication Problems for Typed Template Dependencies. J. Comput. Syst. Sci. Moshe Y. Vardi
1984	A*	`conf`	The Theory of Data Dependencies - An Overview. ICALP Ronald Fagin, Moshe Y. Vardi
1983	J	`jnl`	Armstrong Databases for Functional and Inclusion Dependencies. Inf. Process. Lett. Ronald Fagin, Moshe Y. Vardi
1983	J	`jnl`	Inferring Multivalued Dependencies From Functional and Join Dependencies. Acta Informatica Moshe Y. Vardi
1983	A*	`conf`	On the Semantics of Updates in Databases. PODS Ronald Fagin, Jeffrey D. Ullman, Moshe Y. Vardi
1983	A*	`conf`	Reasoning about Infinite Computation Paths (Extended Abstract) FOCS Pierre Wolper, Moshe Y. Vardi, A. Prasad Sistla
1983	—	`conf`	Second-Order Dependency Theory. XP4.5 Workshop on Database Theory Moshe Y. Vardi
1983	A*	`conf`	The Revenge of the JD. PODS David Maier, Jeffrey D. Ullman, Moshe Y. Vardi
1983	A*	`conf`	Unary Inclusion Dependencies have Polynomial Time Inference Problems (Extended Abstract) STOC Paris C. Kanellakis, Stavros S. Cosmadakis, Moshe Y. Vardi
1983	—	`conf`	Yet Another Process Logic (Preliminary Version). Logic of Programs Moshe Y. Vardi, Pierre Wolper
1982	A*	`conf`	On Decomposition of Relational Databases FOCS Moshe Y. Vardi
1982	A*	`conf`	The Complexity of Relational Query Languages (Extended Abstract) STOC Moshe Y. Vardi
1982	A*	`conf`	The Implication and Finite Implication Problems for Typed Template Dependencies. PODS Moshe Y. Vardi
1981	J	`jnl`	A Note on Decompositions of Relational Databases. SIGMOD Rec. Catriel Beeri, Moshe Y. Vardi
1981	A*	`conf`	Global Decision Problems for Relational Databases FOCS Moshe Y. Vardi
1981	J	`jnl`	The Decision Problem for Database Dependencies. Inf. Process. Lett. Moshe Y. Vardi
1981	A*	`conf`	The Implication Problem for Data Dependencies. ICALP Catriel Beeri, Moshe Y. Vardi
1981	—	`—`	בעיית הגרירה לתלויות בין נתונים במסדי נתונים יחסיים (The implication problem for data dependencies in relational databases.). Moshe Y. Vardi
1980	—	`conf`	Decision Problems for Data Dependencies. XP1 Workshop on Database Theory Catriel Beeri, Moshe Y. Vardi
1979	—	`conf`	On the Properties of Join Dependencies. Advances in Data Base Theory Catriel Beeri, Moshe Y. Vardi