BibSLEIGH — Moshe_Y

Travelled to:

1 × Australia
1 × Austria
1 × Cyprus
1 × Czech Republic
1 × Estonia
1 × Greece
1 × Iceland
1 × Ireland
1 × Japan
1 × Norway
1 × Portugal
1 × Spain
2 × Belgium
2 × Germany
2 × Poland
2 × Russia
2 × The Netherlands
3 × Denmark
3 × Israel
5 × Italy
6 × Canada
60 × USA
7 × France
8 × United Kingdom

Collaborated with:

∅ O.Kupferman P.G.Kolaitis N.Piterman G.Pan P.Wolper S.Nain D.Calvanese G.D.Giacomo M.Lenzerini J.D.Ullman G.M.Kuper S.Fogarty S.Chaudhuri J.Y.Halpern R.Fagin U.Sattler G.Kamhi T.Feder Y.Sagiv R.Sebastiani S.Tonetta S.Chakraborty K.S.Meel Y.Lustig K.Y.Rozier S.Safra P.C.Kanellakis S.Bansal E.Singerman R.Fraer R.Armoni L.Fix M.Romero S.Chaudhuri E.Plaku L.E.Kavraki B.Cook K.Chatterjee L.Doyen T.Wilke K.Etessami D.Bustan H.Chockler C.Courcoubetis S.S.Cosmadakis J.Li A.Tiemeyer D.Tabakov M.Yannakakis M.Pistore N.Immerman H.G.Mairson H.Gaifman L.J.Stockmeyer M.H.Graham C.Beeri J.Fisher E.Giunchiglia A.Tacchella S.Mador-Haim Y.Abarbanel P.Barceló S.Sankaranarayanan P.B.Baeza E.Koskinen P.Babighian S.Rubin V.King M.Daniele F.Giunchiglia O.Bernholtz R.Alur T.A.Henzinger D.Harel R.Rosner A.P.Sistla D.Maier D.Fried L.M.Tabajara Y.Zbar M.Tsai Y.Tsay K.Greimel R.Bloem B.Jobstmann M.Z.Kwiatkowska P.A.Bonatti C.Lutz A.Murano R.P.Kurshan M.Narizzano S.Abiteboul C.H.Papadimitriou A.Aiken D.Kozen E.L.Wimmers T.W.Frühwirth E.Y.Shapiro E.Yardeni G.G.Hillebrand R.Ramakrishnan A.Flaisher D.J.Fremont S.A.Seshia A.Gotsman A.Podelski A.Rybalchenko D.Korchemny M.Glusman R.Batsell L.Brenner D.N.Osherson S.Tsavachidis K.Fisler Z.Yang B.Ziv R.Dureja G.Pu K.Y.Rozier O.Grumberg F.Copty D.Benque S.Bourton C.Cockerton S.Ishtiaq A.S.Taylor T.Arons E.Elster M.Mishaeli J.Shalev L.D.Zuck R.Gerth B.Ginsburg T.Kanza A.Landver

Talks about:

logic (34) automata (23) check (22) model (19) program (17) databas (17) queri (16) complex (15) time (14) tempor (13)

Person: Moshe Y. Vardi

DBLP: Vardi:Moshe_Y=

Facilitated 3 volumes:

Contributed to:

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1991

1990

1989

1988

1987

1986

1985

1984

1983

1982

1981

2016

2018

2019

Wrote 162 papers:

ICALP-v2-2015-Chatterjee0V #complexity #component #probability #synthesis: The Complexity of Synthesis from Probabilistic Components (KC, LD, MYV), pp. 108–120.
TACAS-2015-ChakrabortyFMSV #generative #on the #parallel #satisfiability #scalability: On Parallel Scalable Uniform SAT Witness Generation (SC, DJF, KSM, SAS, MYV), pp. 304–319.
DAC-2014-AbarbanelSV #challenge #validation: Validation of SoC Firmware-Hardware Flows: Challenges and Solution Directions (YA, ES, MYV), p. 4.
DAC-2014-ChakrabortyMV #generative #satisfiability #scalability: Balancing Scalability and Uniformity in SAT Witness Generator (SC, KSM, MYV), p. 6.
FoSSaCS-2014-Chatterjee0NV #complexity #game studies #probability: The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies (KC, LD, SN, MYV), pp. 242–257.
PODS-2014-Barcelo0V #evaluation #query #question: Does query evaluation tractability help query containment? (PB, MR, MYV), pp. 188–199.
CAV-2013-ChakrabortyMV #generative #satisfiability #scalability: A Scalable and Nearly Uniform Generator of SAT Witnesses (SC, KSM, MYV), pp. 608–623.
ESEC-FSE-2013-Vardi #logic: A logical revolution (MYV), p. 1.
LICS-2013-ChaudhuriSV #analysis: Regular Real Analysis (SC, SS, MYV), pp. 509–518.
LICS-2013-NainV #game studies #probability: Solving Partial-Information Stochastic Parity Games (SN, MYV), pp. 341–348.
PODS-2013-BaezaRV #database #graph #semantics: Semantic acyclicity on graph databases (PBB, MR, MYV), pp. 237–248.
VLDB-2013-CalvaneseGLV12 #database #graph #query #relational: Query Processing under GLAV Mappings for Relational and Graph Databases (DC, GDG, ML, MYV), pp. 61–72.
CAV-2012-BenqueBCCFIPTV #biology #modelling #named #network #visual notation: Bma: Visual Tool for Modeling and Analyzing Biological Networks (DB, SB, CC, BC, JF, SI, NP, AST, MYV), pp. 686–692.
FoSSaCS-2012-NainV #probability: Synthesizing Probabilistic Composers (SN, MYV), pp. 421–436.
CAV-2011-CookKV #program analysis #verification: Temporal Property Verification as a Program Analysis Task (BC, EK, MYV), pp. 333–348.
CSL-2011-FogartyKVW #automaton: Unifying Büchi Complementation Constructions (SF, OK, MYV, TW), pp. 248–263.
CSL-2011-LustigNV #component #probability #synthesis: Synthesis from Probabilistic Components (YL, SN, MYV), pp. 412–427.
CSL-2011-Vardi #branch #linear #perspective #semantics: Branching vs. Linear Time: Semantical Perspective (MYV), p. 3.
FM-2011-FisherPV: The Only Way Is Up (JF, NP, MYV), pp. 3–11.
FM-2011-RozierV #approach #encoding #ltl #multi #satisfiability: A Multi-encoding Approach for LTL Symbolic Satisfiability Checking (KYR, MYV), pp. 417–431.
CIAA-2010-TsaiFVT #automaton: State of Büchi Complementation (MHT, SF, MYV, YKT), pp. 261–271.
TACAS-2010-FogartyV #automaton #performance: Efficient Büchi Universality Checking (SF, MYV), pp. 205–220.
FoSSaCS-2009-LustigV #component #library #synthesis: Synthesis from Component Libraries (YL, MYV), pp. 395–409.
LICS-2009-NainV #semantics: Trace Semantics is Fully Abstract (SN, MYV), pp. 59–68.
SAT-2009-Vardi #satisfiability: Symbolic Techniques in Propositional Satisfiability Solving (MYV), pp. 2–3.
TACAS-2009-FogartyV #automaton #termination: Büchi Complementation and Size-Change Termination (SF, MYV), pp. 16–30.
TACAS-2009-PlakuKV #hybrid #ltl #safety: Falsification of LTL Safety Properties in Hybrid Systems (EP, LEK, MYV), pp. 368–382.
ICALP-B-2008-GreimelBJV: Open Implication (KG, RB, BJ, MYV), pp. 361–372.
CAV-2007-KupfermanPV #liveness: From Liveness to Promptness (OK, NP, MYV), pp. 406–419.
CAV-2007-PlakuKV #hybrid #verification: Hybrid Systems: From Verification to Falsification (EP, LEK, MYV), pp. 463–476.
CIAA-2007-Vardi #automaton #linear #model checking: Linear-Time Model Checking: Automata Theory in Practice (MYV), pp. 5–10.
DAC-2007-Vardi #verification: Formal Techniques for SystemC Verification; Position Paper (MYV), pp. 188–192.
DATE-2007-BabighianKV #data mining #interactive #mining #optimisation: Interactive presentation: PowerQuest: trace driven data mining for power optimization (PB, GK, MYV), pp. 1078–1083.
LATA-2007-TabakovV #model checking #specification: Model Checking Buechi Specifications (DT, MYV), pp. 565–576.
POPL-2007-CookGPRV #proving #source code: Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.
TACAS-2007-EtessamiKVY #markov #model checking #multi #process: Multi-objective Model Checking of Markov Decision Processes (KE, MZK, MYV, MY), pp. 50–65.
TACAS-2007-SebastianiTV #abstraction #clustering #refinement: Property-Driven Partitioning for Abstraction Refinement (RS, ST, MYV), pp. 389–404.
VMCAI-2007-Vardi #formal method #model checking #revisited: Automata-Theoretic Model Checking Revisited (MYV), pp. 137–150.
CAV-2006-KupfermanPV #composition #synthesis: Safraless Compositional Synthesis (OK, NP, MYV), pp. 31–44.
FATES-RV-2006-ArmoniKTVZ #linear #monitoring: Deterministic Dynamic Monitors for Linear-Time Assertions (RA, DK, AT, MYV, YZ), pp. 163–177.
ICALP-v2-2006-BonattiLMV #calculus #complexity #μ-calculus: The Complexity of Enriched μ-Calculi (PAB, CL, AM, MYV), pp. 540–551.
LICS-2006-KupfermanV #logic: Memoryful Branching-Time Logic (OK, MYV), pp. 265–274.
LICS-2006-PanV #parametricity: Fixed-Parameter Hierarchies inside PSPACE (GP, MYV), pp. 27–36.
CAV-2005-AronsEFMMSSTVZ #verification: Formal Verification of Backward Compatibility of Microcode (TA, EE, LF, SMH, MM, JS, ES, AT, MYV, LDZ), pp. 185–198.
CAV-2005-SebastianiTV #hybrid #ltl #model checking: Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking (RS, ST, MYV), pp. 350–363.
TACAS-2005-KupfermanV #automaton #infinity #nondeterminism #word: Complementation Constructions for Nondeterministic Automata on Infinite Words (OK, MYV), pp. 206–221.
CAV-2004-BustanRV #markov #verification: Verifying ω-Regular Properties of Markov Chains (DB, SR, MYV), pp. 189–201.
CAV-2004-PitermanV #infinity #model checking: Global Model-Checking of Infinite-State Systems (NP, MYV), pp. 387–400.
CAV-2004-SebastianiSTV #model checking: GSTE Is Partitioned Model Checking (RS, ES, ST, MYV), pp. 229–241.
SAT-2004-PanV #satisfiability: Search vs. Symbolic Techniques in Satisfiability Solving (GP, MYV), pp. 137–146.
SAT-J-2004-PanV05 #satisfiability: Search vs. Symbolic Techniques in Satisfiability Solving (GP, MYV), pp. 235–250.
TACAS-2004-KupfermanV #certification: From Complementation to Certification (OK, MYV), pp. 591–606.
CADE-2003-PanV #optimisation: Optimizing a BDD-Based Modal Solver (GP, MYV), pp. 75–89.
CAV-2003-ArmoniFFGPTV #detection #linear #logic: Enhanced Vacuity Detection in Linear Temporal Logic (RA, LF, AF, OG, NP, AT, MYV), pp. 368–380.
ICALP-2003-KupfermanV: Π₂ ∩ Σ₂ ≡ AFMC (OK, MYV), pp. 697–713.
ICALP-2003-Vardi #automaton #logic: Logic and Automata: A Match Made in Heaven (MYV), pp. 64–65.
LICS-2003-FederV #morphism: Homomorphism Closed vs. Existential Positive (TF, MYV), pp. 311–320.
LICS-2003-PistoreV #infinity: The Planning Spectrum — One, Two, Three, Infinity (MP, MYV), pp. 234–243.
LICS-2003-PitermanV #decidability #future of #stack: Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems (NP, MYV), p. 381–?.
PODS-2003-CalvaneseGLV #query: View-based query containment (DC, GDG, ML, MYV), pp. 56–67.
TACAS-2003-ArmoniBKV #linear #logic: Resets vs. Aborts in Linear Temporal Logic (RA, DB, OK, MYV), pp. 65–80.
TACAS-2003-GlusmanKMFV #abstraction #evaluation #industrial #multi #refinement: Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation (MG, GK, SMH, RF, MYV), pp. 176–191.
CADE-2002-KupfermanSV #calculus #complexity: The Complexity of the Graded µ-Calculus (OK, US, MYV), pp. 423–437.
CADE-2002-PanSV: BDD-Based Decision Procedures for K (GP, US, MYV), pp. 16–30.
CAV-2002-KupfermanPV #linear #model checking: Model Checking Linear Properties of Prefix-Recognizable Systems (OK, NP, MYV), pp. 371–385.
KR-2002-BatsellBOTV: Eliminating Incoherence from Subjective Estimates of Chance (RB, LB, DNO, ST, MYV), pp. 353–364.
KR-2002-CalvaneseGV #ltl #reasoning: Reasoning about Actions and Planning in LTL Action Theories (DC, GDG, MYV), pp. 593–602.
PODS-2002-CalvaneseGLV: Lossless Regular Views (DC, GDG, ML, MYV), pp. 247–258.
TACAS-2002-ArmoniFFGGKLMSTVZ #logic: The ForSpec Temporal Logic: A New Temporal Property-Specification Language (RA, LF, AF, RG, BG, TK, AL, SMH, ES, AT, MYV, YZ), pp. 296–211.
CAV-2001-ChocklerKKV #approach #model checking: A Practical Approach to Coverage in Model Checking (HC, OK, RPK, MYV), pp. 66–78.
CAV-2001-CoptyFFGKTV #bound #industrial #model checking: Benefits of Bounded Model Checking at an Industrial Setting (FC, LF, RF, EG, GK, AT, MYV), pp. 436–453.
FoSSaCS-2001-KingKV #automaton #complexity #on the #word: On the Complexity of Parity Word Automata (VK, OK, MYV), pp. 276–286.
IJCAR-2001-SattlerV #calculus #hybrid: The Hybrid µ-Calculus (US, MYV), pp. 76–91.
LICS-2001-KupfermanV #distributed: Synthesizing Distributed Systems (OK, MYV), pp. 389–398.
SAT-2001-GiunchigliaNTV #library #performance #satisfiability #towards: Towards an Efficient Library for SAT: a Manifesto (EG, MN, AT, MYV), pp. 290–310.
TACAS-2001-ChocklerKV #logic #metric #model checking: Coverage Metrics for Temporal Logic Model Checking (HC, OK, MYV), pp. 528–542.
TACAS-2001-FislerFVY #algorithm #detection #question: Is There a Best Symbolic Cycle-Detection Algorithm? (KF, RF, GK, MYV, ZY), pp. 420–434.
TACAS-2001-Vardi #branch #linear: Branching vs. Linear Time: Final Showdown (MYV), pp. 1–22.
CAV-2000-FraerKZVF #analysis #performance #reachability #traversal #verification: Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification (RF, GK, BZ, MYV, LF), pp. 389–402.
CAV-2000-KupfermanV #approach #infinity #reasoning: An Automata-Theoretic Approach to Reasoning about Infinite-State Systems (OK, MYV), pp. 36–52.
CSL-2000-Vardi #automation #automaton #graph #logic #verification: Automated Verification = Graphs, Automata, and Logic (MYV), p. 139.
KR-2000-CalvaneseGLV #query: Containment of Conjunctive Regular Path Queries with Inverse (DC, GDG, ML, MYV), pp. 176–185.
LICS-2000-CalvaneseGLV #constraints #query: View-Based Query Processing and Constraint Satisfaction (DC, GDG, ML, MYV), pp. 361–371.
PODS-2000-CalvaneseGLV #query: View-Based Query Processing for Regular Path Queries with Inverse (DC, GDG, ML, MYV), pp. 58–66.
PODS-2000-Vardi #constraints #database #tutorial: Constraint Satisfaction and Database Theory: a Tutorial (MYV), pp. 76–85.
CAV-1999-DanieleGV #automaton #generative #linear #logic: Improved Automata Generation for Linear Temporal Logic (MD, FG, MYV), pp. 249–260.
CAV-1999-KupfermanV #model checking #safety: Model Checking of Safety Properties (OK, MYV), pp. 172–183.
PODS-1999-CalvaneseGLV #query #regular expression: Rewriting of Regular Expressions and Regular Path Queries (DC, GDG, ML, MYV), pp. 194–204.
ICALP-1998-Vardi #automaton #reasoning: Reasoning about The Past with Two-Way Automata (MYV), pp. 628–641.
LICS-1998-KupfermanV #linear: Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time (OK, MYV), pp. 81–92.
LICS-1998-Vardi #branch #linear #perspective: Linear vs. Branching Time: A Complexity-Theoretic Perspective (MYV), pp. 394–405.
PODS-1998-KolaitisV #constraints: Conjunctive-Query Containment and Constraint Satisfaction (PGK, MYV), pp. 205–213.
STOC-1998-KupfermanV #automaton: Weak Alternating Automata and Tree Automata Emptiness (OK, MYV), pp. 224–233.
CADE-1997-Vardi #automaton #logic: Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics (MYV), pp. 191–206.
CAV-1997-ImmermanV #logic #model checking #transitive: Model Checking and Transitive-Closure Logic (NI, MYV), pp. 291–302.
CAV-1997-KupfermanV #revisited: Module Checking Revisited (OK, MYV), pp. 36–47.
LICS-1997-EtessamiVW #first-order #logic: First-Order Logic with Two Variables and Unary Temporal Logic (KE, MYV, TW), pp. 228–235.
CAV-1996-KupfermanV: Module Checking (OK, MYV), pp. 75–86.
CAV-1996-KupfermanV96a #verification: Verification of Fair Transisiton Systems (OK, MYV), pp. 372–382.
LICS-1996-KolaitisV #logic #on the #power of: On the Expressive Power of Variable-Confined Logics (PGK, MYV), pp. 348–359.
LICS-1996-KupfermanSV #automaton #word: Relating Word and Tree Automata (OK, SS, MYV), pp. 322–332.
PODS-1996-AbiteboulKPV: In Memoriam: Paris C. Kanellakis (SA, GMK, CHP, MYV), p. 79.
CAV-1995-Vardi #approach #synthesis: An Automata-Theoretic Approach to Fair Realizability and Synthesis (MYV), pp. 267–278.
LICS-1995-Vardi #complexity #composition #model checking #on the: On the Complexity of Modular Model Checking (MYV), pp. 101–111.
PODS-1995-Vardi #bound #complexity #on the #query: On the Complexity of Bounded-Variable Queries (MYV), pp. 266–276.
CAV-1994-BernholtzVW #approach #model checking: An Automata-Theoretic Approach to Branching-Time Model Checking (OB, MYV, PW), pp. 142–155.
PODS-1994-ChaudhuriV #complexity #datalog #equivalence #on the #recursion #source code: On the Complexity of Equivalence between Recursive and Nonrecursive Datalog Programs (SC, MYV), pp. 107–116.
CSL-1993-AikenKVW #complexity #constraints #set: The Complexity of Set Constraints (AA, DK, MYV, ELW), pp. 1–17.
PODS-1993-ChaudhuriV #optimisation #query: Optimization of Real Conjunctive Queries (SC, MYV), pp. 59–70.
STOC-1993-AlurHV #parametricity #realtime #reasoning: Parametric real-time reasoning (RA, TAH, MYV), pp. 592–601.
STOC-1993-FederV #constraints #monad: Monotone monadic SNP and constraint satisfaction (TF, MYV), pp. 612–622.
ICALP-1992-KolaitisV #logic: Infinitary Logic for Computer Science (PGK, MYV), pp. 450–473.
LICS-1992-KolaitisV #fixpoint #logic: Fixpoint Logic vs. Infinitary Logic in Finite-Model Theory (PGK, MYV), pp. 46–57.
PODS-1992-ChaudhuriV #datalog #equivalence #on the #recursion #source code: On the Equivalence of Recursive and Nonrecursive Datalog Programs (SC, MYV), pp. 55–66.
KR-1991-HalpernV #model checking #proving #theorem proving: Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
LICS-1991-FruhwirthSVY #logic programming #source code: Logic Programs as Types for Logic Programs (TWF, EYS, MYV, EY), pp. 300–309.
PODS-1991-HillebrandKMV #bound #datalog #tool support: Tools for Datalog Boundedness (GGH, PCK, HGM, MYV), pp. 1–12.
CAV-1990-CourcoubetisVWY #algorithm #memory management #performance #verification: Memory Efficient Algorithms for the Verification of Temporal Properties (CC, MYV, PW, MY), pp. 233–242.
CLP-1990-Vardi90 #database #logic programming #optimisation #problem #source code: Global Optimization Problems for Database Logic Programs (MYV), pp. 767–771.
LICS-1990-HarelRV #bound #concurrent #on the #power of #reasoning #source code: On the Power of Bounded Concurrency~III: Reasoning About Programs (DH, RR, MYV), pp. 478–488.
LICS-1990-KolaitisV #logic: 0-1 Laws for Infinitary Logics (PGK, MYV), pp. 156–167.
PODS-1990-KolaitisV #case study #datalog #on the #power of #tool support: On the Expressive Power of Datalog: Tools and a Case Study (PGK, MYV), pp. 61–71.
LICS-1989-Vardi #complexity #on the #reasoning: On the Complexity of Epistemic Reasoning (MYV), pp. 243–252.
PODS-1989-RamakrishnanSUV #program transformation #theorem: Proof-Tree Transformation Theorems and Their Applications (RR, YS, JDU, MYV), pp. 172–181.
PODS-1989-SagivV #database #datalog #infinity #query #safety: Safety of Datalog Queries over Infinite Databases (YS, MYV), pp. 160–171.
PODS-1989-Vardi #automaton #database: Automata Theory for Database Theoreticans (MYV), pp. 83–92.
STOC-1989-SafraV #automaton #logic #on the: On ω-Automata and Temporal Logic (SS, MYV), pp. 127–137.
LICS-1988-KolaitisV #higher-order #logic #problem: 0-1 Laws and Decision Problems for Fragments of Second-Order Logic (PGK, MYV), pp. 2–11.
PODS-1988-UllmanV #complexity: The Complexity of Ordering Subgoals (JDU, MYV), pp. 74–81.
PODS-1988-Vardi #bound #decidability #linear #query #recursion: Decidability and Undecidability Results for Boundedness of Linear Recursive Queries (MYV), pp. 341–351.
POPL-1988-Vardi #calculus #fixpoint: A Temporal Fixpoint Calculus (MYV), pp. 250–259.
SIGMOD-1988-Vardi #database #deduction #logic programming: Database Logic Programming, Deductive Databases, and Expert Database Systems (MYV), p. 7.
STOC-1988-CosmadakisGKV #database #decidability #logic programming #optimisation #problem #source code: Decidable Optimization Problems for Database Logic Programs (SSC, HG, PCK, MYV), pp. 477–490.
STOC-1988-HalpernV #reasoning: Reasoning about Knowledge and Time in Asynchronous Systems (JYH, MYV), pp. 53–65.
LICS-1987-GaifmanMSV #database #decidability #logic programming #optimisation #problem #source code: Undecidable Optimization Problems for Database Logic Programs (HG, HGM, YS, MYV), pp. 106–115.
LICS-1987-Vardi #concurrent #framework #source code #verification: Verification of Concurrent Programs: The Automata-Theoretic Framework (MYV), pp. 167–176.
STOC-1987-KolaitisV #higher-order #problem: The Decision Problem for the Probabilities of Higher-Order Properties (PGK, MYV), pp. 425–435.
LICS-1986-VardiW #approach #automation #verification: An Automata-Theoretic Approach to Automatic Program Verification (MYV, PW), pp. 332–344.
PODS-1986-Vardi #database #on the: On the Integrity of Databases with Incomplete Information (MYV), pp. 252–266.
STOC-1986-CourcoubetisVW #concurrent #reasoning #source code: Reasoning about Fair Concurrent Programs (CC, MYV, PW), pp. 283–294.
STOC-1986-HalpernV #complexity #reasoning: The Complexity of Reasoning about Knowledge and Time: Extended Abstract (JYH, MYV), pp. 304–315.
ICALP-1985-SistlaVW #automaton #logic #problem: The Complementation Problem for Büchi Automata with Applications to Temporal Logic (APS, MYV, PW), pp. 465–474.
PODS-1985-Vardi #database #logic #query: Querying Logical Databases (MYV), pp. 57–65.
SIGMOD-1985-KuperV #logic #on the #power of: On the Expressive Power of the Logical Data Model (GMK, MYV), pp. 180–187.
STOC-1985-FaginV #logic #semantics: An Internal Semantics for Modal Logic: Preliminary Report (RF, MYV), pp. 305–315.
STOC-1985-VardiS #bound #logic #source code: Improved Upper and Lower Bounds for Modal Logics of Programs: Preliminary Report (MYV, LJS), pp. 240–251.
ICALP-1984-FaginV #dependence #formal method #overview #perspective: The Theory of Data Dependencies — An Overview (RF, MYV), pp. 1–22.
PODS-1984-GrahamV #axiom #complexity #consistency #database #on the: On the Complexity and Axiomatizability of Consistent Database States (MHG, MYV), pp. 281–289.
PODS-1984-KuperUV #database #equivalence #logic #on the: On the Equivalence of Logical Databases (GMK, JDU, MYV), pp. 221–228.
PODS-1984-KuperV #approach #database #logic: A New Approach to Database Logic (GMK, MYV), pp. 86–96.
STOC-1984-VardiW #automaton #logic #source code: Automata Theoretic Techniques for Modal Logics of Programs (MYV, PW), pp. 446–456.
PODS-1983-FaginUV #database #on the #semantics: On the Semantics of Updates in Databases (RF, JDU, MYV), pp. 352–365.
PODS-1983-MaierUV: The Revenge of the JD (DM, JDU, MYV), pp. 279–287.
STOC-1983-KanellakisCV #dependence #polynomial #problem: Unary Inclusion Dependencies have Polynomial Time Inference Problems (PCK, SSC, MYV), pp. 264–277.
PODS-1982-Vardi #dependence #finite #problem: The Implication and Finite Implication Problems for Typed Template Dependencies (MYV), pp. 230–238.
STOC-1982-Vardi #complexity #query #relational: The Complexity of Relational Query Languages (MYV), pp. 137–146.
ICALP-1981-BeeriV #dependence #problem: The Implication Problem for Data Dependencies (CB, MYV), pp. 73–85.
CAV-2016-FriedTV #functional #synthesis: BDD-Based Boolean Functional Synthesis (DF, LMT, MYV), pp. 402–421.
CAV-2018-BansalCV #automaton: Automata vs Linear-Programming Discounted-Sum Inclusion (SB, SC, MYV), pp. 99–116.
CAV-2018-LiDPRV #approximate #named #performance #reachability: SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate Reachability (JL, RD, GP, KYR, MYV), pp. 37–44.
CAV-2019-BansalV #automaton #safety: Safety and Co-safety Comparator Automata for Discounted-Sum Inclusion (SB, MYV), pp. 60–78.
CAV-2019-LiVR #ltl #satisfiability: Satisfiability Checking for Mission-Time LTL (JL, MYV, KYR), pp. 3–22.