BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Vardi:Moshe_Y=

Facilitated 3 volumes:

CAV 1998Ed
PODS 1992Ed
PODS 1987Ed

Contributed to:

ICALP (2) 20152015
TACAS 20152015
DAC 20142014
FoSSaCS 20142014
PODS 20142014
CAV 20132013
ESEC/FSE 20132013
LICS 20132013
PODS 20132013
VLDB 20132012
CAV 20122012
FOSSACS 20122012
CAV 20112011
CSL 20112011
FM 20112011
CIAA 20102010
TACAS 20102010
FOSSACS 20092009
LICS 20092009
SAT 20092009
TACAS 20092009
ICALP (2) 20082008
CAV 20072007
CIAA 20072007
DAC 20072007
DATE 20072007
LATA 20072007
POPL 20072007
TACAS 20072007
VMCAI 20072007
CAV 20062006
FATES/RV 20062006
ICALP (2) 20062006
LICS 20062006
CAV 20052005
TACAS 20052005
CAV 20042004
SAT 20042004
SAT 20042005
TACAS 20042004
CADE 20032003
CAV 20032003
ICALP 20032003
LICS 20032003
PODS 20032003
TACAS 20032003
CADE 20022002
CAV 20022002
KR 20022002
PODS 20022002
TACAS 20022002
CAV 20012001
FoSSaCS 20012001
IJCAR 20012001
LICS 20012001
SAT 20012001
TACAS 20012001
CAV 20002000
CSL 20002000
KR 20002000
LICS 20002000
PODS 20002000
CAV 19991999
PODS 19991999
ICALP 19981998
LICS 19981998
PODS 19981998
STOC 19981998
CADE 19971997
CAV 19971997
LICS 19971997
CAV 19961996
LICS 19961996
PODS 19961996
CAV 19951995
LICS 19951995
PODS 19951995
CAV 19941994
PODS 19941994
CSL 19931993
PODS 19931993
STOC 19931993
ICALP 19921992
LICS 19921992
PODS 19921992
KR 19911991
LICS 19911991
PODS 19911991
CAV 19901990
ICLP 19901990
LICS 19901990
PODS 19901990
LICS 19891989
PODS 19891989
STOC 19891989
LICS 19881988
PODS 19881988
POPL 19881988
SIGMOD 19881988
STOC 19881988
LICS 19871987
STOC 19871987
LICS 19861986
PODS 19861986
STOC 19861986
ICALP 19851985
PODS 19851985
SIGMOD 19851985
STOC 19851985
ICALP 19841984
PODS 19841984
STOC 19841984
PODS 19831983
STOC 19831983
PODS 19821982
STOC 19821982
ICALP 19811981
CAV (2) 20162016
CAV (2) 20182018
CAV (1) 20192019
CAV (2) 20192019

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.