@inproceedings{VW86b,
        author      =   "M.Y. Vardi and P. Wolper",
        title       =   "An Automata-Theoretic Approach to
                         Automatic Program Verification",
        booktitle   =   "Proc. 1st Symp. on Logic
                         in Computer Science",
        pages       =   "332--344",
        year        =   "1986",
        month       =   "June",
        address     =   "Cambridge",
        url         =   "http://www.cs.rice.edu/~vardi/papers/lics86.pdf.gz"
}     

@article{Var91,
    author = "M.Y. Vardi",
    title = "Verification of concurrent programs --
             the automata-theoretic framework",
    journal = "Annals of Pure and Applied Logic",
    volume = "51",
    pages = "79--98",
    year = "1991",
    url = "http://www.cs.rice.edu/~vardi/papers/lics87r2.ps.gz"
}                

@inproceedings{Var99,
    author = "M.Y. Vardi",
    title = "Probabilistic Linear-Time Model Checking: An Overview of
             the Automata-Theoretic Approach",
    booktitle = "5th Int'l Workshop on Formal Methods for Real-Time and
                 Probabilistic Systems",
    series = "Lecture Notes in Computer Science 1601",
    editor = "J.P. Katoen",
    publisher = "Springer-Verlag",
    pages = "265--276",
    year = "1999",
    url = "http://www.cs.rice.edu/~vardi/papers/arts99.ps.gz"
}            

@article{CVWY92,
        author =        "C. Courcoubetis and M.Y. Vardi and P. Wolper
                         and M. Yannakakis",
        title =         "Memory Efficient Algorithms for the
                         Verification of Temporal Properties",
        journal =       "Formal Methods in System Design",
        pages           = "275--288",
        volume          = 1,
         year            = 1992,
        url = "http://www.cs.rice.edu/~vardi/papers/cav90rj.ps.gz"
}       


@article{VW94,
        author      =   "M.Y. Vardi and P. Wolper",
        title       =   "Reasoning about Infinite Computations",
        journal     =   "Information and Computation",
        volume      =   "115",
        number      =   "1",
        year        =   "1994",
        month       =   "November",
        pages       =   "1-37",
        url = "http://www.cs.rice.edu/~vardi/papers/focs83rj.ps.gz"
}       

@inproceedings{Var96,
        author      =   "M.Y. Vardi",
        title       =   "An automata-theoretic approach to
                         linear temporal logic",
        editor     =   "F. Moller and G. Birtwistle",
        booktitle   =   "Logics for Concurrency: Structure versus
                         Automata",
        series          = "Lecture Notes in Computer Science",
        publisher       = "Springer-Verlag, Berlin",
        volume      =   "1043",
        pages       =   "238--266",
        year        =   "1996",
        url = "http://www.cs.rice.edu/~vardi/papers/banff94rj.ps.gz"
}


@inproceedings{Var95d,
        author =        "M.Y. Vardi",
        title =         "Alternating automata and program verification",
       booktitle =     "Computer Science Today --Recent Trends and
                         Developments",
        series          = "Lecture Notes in Computer Science",
        volume =         1000,
        year =          "1995",
        publisher   =   "Springer-Verlag, Berlin",
        pages       =   "471-485",
        url = "http://www.cs.rice.edu/~vardi/papers/vol1000.ps.gz"
}    

@inproceedings{GPVW95,
        author      =   "R. Gerth and D. Peled and M.Y. Vardi and P.
Wolper",
        editor     =   "P. Dembiski and M. Sredniawa",
        publisher   =   "Chapman \& Hall",
        title       =   "Simple on-the-fly automatic verification
                         of linear temporal logic",
        booktitle   =   "Protocol Specification, Testing, and Verification",
        pages       =   "3--18",
        month       =   "August",
        year        =   "1995",
        url = "http://www.cs.rice.edu/~vardi/papers/pstv95rj.ps.gz"
}                 


@inproceedings{DGV99,
        author      =   "N. Daniele and F. Guinchiglia and M.Y. Vardi",
        title       =   "Improved automata generation for linear
                  temporal logic",
        booktitle   =   "Computer Aided Verification, Proc. 11th International
                         Conference",
        pages       =   "249-260",
        series      =   "Lecture Notes in Computer Science",
        volume      =   "1633",
        publisher   =   "Springer-Verlag",
        year        =   "1999",
        url = "http://www.cs.rice.edu/~vardi/papers/cav992rj.ps.gz"
}    
   
@article{KV01d,
        author      =   "O. Kupferman and M.Y. Vardi",
        title       =   "Model checking of safety properties",
        journal    =    "Formal methods in System Design",
        volume     =    19,
        number     =    3,
        month      =    "November",
        pages      =    "291-314",
        year       =    "2001",
        url = "http://www.cs.rice.edu/~vardi/papers/cav991.ps.gz"
}    
    
@article{KV01c,
        author      =   "O. Kupferman and M.Y. Vardi",
        title       =   "Weak alternating automata are not that weak",
        journal     =   "ACM Trans. on Computational Logic",
        volume      =   2001,
        number      =   2,
        month       =   "July",
        year        =   2001,
        pages       =   "408--429",
        url = "http://www.cs.rice.edu/~vardi/papers/istcs97rj.ps.gz"
}