|
[1]
|
M. Y. Vardi and P. Wolper, An automata-theoretic approach to automatic program
verification, in Proc. 1st Symp. on
Logic in Computer Science, (Cambridge), pp. 332-344, June 1986.
[ List ]
@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 = JUN,
ADDRESS = {Cambridge},
URL = {http://www.cs.rice.edu/~vardi/papers/lics86.pdf.gz}
}
|
|
[2]
|
M. Y. Vardi, Verification of concurrent programs - the automata-theoretic
framework, Annals of Pure and Applied
Logic, vol. 51, pp. 79-98, 1991.
[ List ]
@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}
}
|
|
[3]
|
M. Y. Vardi, Probabilistic linear-time model checking: An overview of the
automata-theoretic approach, in 5th
Int'l Workshop on Formal Methods for Real-Time and Probabilistic Systems
(J. P. Katoen, ed.), Lecture Notes in Computer Science 1601, pp. 265-276,
Springer-Verlag, 1999.
[ List ]
@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}
}
|
|
[4]
|
C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis, Memory efficient algorithms for the verification of temporal
properties, Formal Methods in System
Design, vol. 1, pp. 275-288, 1992.
[ List ]
@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}
}
|
|
[5]
|
M. Y. Vardi and P. Wolper, Reasoning about infinite computations,
Information and Computation, vol. 115, pp. 1-37, Nov. 1994.
[ List ]
@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 = NOV,
PAGES = {1--37},
URL = {http://www.cs.rice.edu/~vardi/papers/focs83rj.ps.gz}
}
|
|
[6]
|
M. Y. Vardi, An automata-theoretic approach to linear temporal
logic, in Logics for Concurrency:
Structure versus Automata (F. Moller and G. Birtwistle, eds.), vol. 1043 of
Lecture Notes in Computer Science, pp. 238-266, Springer-Verlag,
Berlin, 1996.
[ List ]
@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}
}
|
|
[7]
|
M. Y. Vardi, Alternating automata and program
verification, in Computer Science
Today -Recent Trends and Developments, vol. 1000 of Lecture Notes in
Computer Science, pp. 471-485, Springer-Verlag, Berlin, 1995.
[ List ]
@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}
}
|
|
[8]
|
R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, Simple on-the-fly automatic verification of linear temporal
logic, in Protocol Specification,
Testing, and Verification (P. Dembiski and M. Sredniawa, eds.), pp. 3-18,
Chapman & Hall, Aug. 1995.
[ List ]
@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 = AUG,
YEAR = {1995},
URL = {http://www.cs.rice.edu/~vardi/papers/pstv95rj.ps.gz}
}
|
|
[9]
|
N. Daniele, F. Guinchiglia, and M. Y. Vardi, Improved automata generation for linear temporal
logic, in Computer Aided Verification,
Proc. 11th International Conference, vol. 1633 of Lecture Notes in
Computer Science, pp. 249-260, Springer-Verlag, 1999.
[ List ]
@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}
}
|
|
[10]
|
O. Kupferman and M. Y. Vardi, Model checking of safety properties,
Formal methods in System Design, vol. 19, pp. 291-314, Nov. 2001.
[ List ]
@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 = NOV,
PAGES = {291--314},
YEAR = {2001},
URL = {http://www.cs.rice.edu/~vardi/papers/cav991.ps.gz}
}
|
|
[11]
|
O. Kupferman and M. Y. Vardi, Weak alternating automata are not that
weak, ACM Trans. on Computational
Logic, vol. 2001, pp. 408-429, July 2001.
[ List ]
@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 = JUL,
YEAR = {2001},
PAGES = {408--429},
URL = {http://www.cs.rice.edu/~vardi/papers/istcs97rj.ps.gz}
}
|
