JOURNAL PUBLICATIONS
- Automatic Verification of Finite-State Concurrent Systems Using
Temporal Logic Specifications (with E.M.Clarke and E.A.Emerson),
ACM Transactions On Programming Languages And Systems, Vol.\ 8,No. 2,
April 1986, Pages 244-263.
- Complexity of Propositional Linear Temporal Logics
(with E.M.Clarke),
Journal of the Association for Computing Machinery,
Vol. 32,No. 3,July 1985, pp 733-749.
- Can Message Buffers be Axiomatized in Linear Temporal Logic(with
E.M.Clarke, N.Francez and A.R.Meyer), Information and Control, Vol. 63,
Nos. 1/2, October/November 1984.
- Deciding Full Branching Time Logic (with E.A.Emerson),
Information and Control, Vol. 61, No. 3, June 1984.
- A Multiprocess Network Logic with Temporal and Spatial Modalities (with
J. Reif),
Journal of Computer and System Sciences, Vol. 30, No. 1,
February 1985.
- The Complementation Problem for Buchi Automata and Applications to
Temporal Logic (with M. Vardi and P. Wolper),
Theoretical Computer Science, 49,
No 2,3 1987, pp 217-237.
- On Verifying That A Concurrent Program Satisfies A Nondeterministic
Specification, Information Processing Letters 32 (1989).
- Reasoning About Systems With Many Processes (with S.M.German),
Journal of the ACM, July 1992, Volume 39, Number 3, pp 675-735.
- Reasoning in a Restricted Temporal Logic (with Lenore Zuck),
Information and Computation, Vol 102, No 2, February 1993.
- Proving Correctness with respect to Nondeterministic Safety
Specifications, Information Processing Letters 39(1991)45-49.
- Quantitative Temporal Reasoning (With E.A. Emerson, Al Mok and Jai
Srinivasan), Journal of Real-Time Systems, 4, 331-352 (1992).
- Safety, Liveness and Fairness in Temporal
Logic,
Formal Aspects in Computing, 1994, vol. 6, pp 495-511.
- Temporal Triggers in Active Databases (with Ouri Wolfson), IEEE
Transactions on Knowledge and Data Engineering, Vol 7, No 3, June 1995.
- Symmetry and Modelchecking (with E. A. Emerson),
Formal Methods in System Design, 9(1/2), 1996, pp 105-130.
- Using Symmetry When Modelchecking under Fairness Assumptions: An
Automata Theoretic Approach (with E. A. Emerson), ACM
Transactions on Programming Languages and Systems, Vol. 19, No. 4, JUly 1997.
- Minimization of Communication Cost Through Caching in Mobile
Environments (with Ouri Wolfson), IEEE Transactions on Parallel
and Distributed Systems, Vol 9, Number 4, April 1998, pp 378-390.
- Incremental Verification of Architecture Specification Language for
Real-time Systems (with Jeff Tsai, Avinash Sahay and Ray Paul), To appear
in the Journal of Software Engineering and Knowledge Engineering.
- Towards a Theory of Cost Management for Digital Libraries (with
Wolfson, Yesha and Sloan), ACM Transactions on Database Systems, Vol. 23(4),
Dec. 1998, pp 411-452.
- On-the-fly Modelchecking under Fairness that Exploits Symmetry
(with V. Gyuris), Formal Methods in System Design, Vol 15, Issue 3, Nov 1999,
pp 217-238.
- Updating and Querying Databases that Track Mobile Units
(with O. Wolfson, S. Chamberlin, Y. Yesha), Distrbuted and Parallel Databases,
7(3), 1999.
- Parametrized Verification of Linear Networks using automata as
invariants (with V. Gyuris), Formal Aspects of Computing, Vol. 11,
pp 402-425, 1999.
- On Model-checking for Fragments of mu-calculus (with E. A. Emerson
and C. Jutla), Theoretical Computer Sciecne 258(1-2)(2001)pp 491-522.
- Reasoning about Qualitative Spatial Relationships (with C. Y. Yu),
Journal of Automated Reasoning, Vol. 25, no. 4, November 2000, pp 291-328.
- SMC: A Symmetry based Model Checker for safety and liveness properties
(with V. Gyuris and E. A. Emerson), ACM Transactions on
Software Engineering Methodologies, Vol. 9, No. 2, April 2000, pp 133-166.
- Symmetry and Reduced Symmetry in Model Checking(with P. Godefroid),
ACM Transactions on Programming Languages, Volume 26, Issue 4, July 2004,
Pages 702-734.
- Employing Symmetry Reductions in Model Checking,
Computer Languages, Systems and Structures 30 (2004) pp 99-137 (invited paper).
CONFERENCE PUBLICATIONS
- Automatic Verification of Finite-State Concurrent Systems Using
Temporal Logic Specifications (with E.M.Clarke and E.A.Emerson),
Proceedings Of The 10th Acm Symposium On Principles Of Programming Languages,
Austin, Texas, January 1983.
- Complexity of Propositional Linear Temporal Logics
(with E.M.Clarke),
Proceedings Of The 14th Annual Acm Symposium On Theory Of Computing,
Sanfransisco, May 1982.
- Deciding Full Branching Time Logic(with E.A.Emerson),
Proceedings Of The
16th Annual ACM Symposium On Theory Of Computing, Washington D.C.,
April-May 1984.
- A Multiprocess Network Logic with Temporal and Spatial Modalities(with
J. Reif),
Proceedings Of The 10th International Colloquium On
Automata, Languages And Programming, July 1983, Barcelona, Spain.
- The Complementation Problem for Buchi Automata and Applications to
Temporal Logic (with M. Vardi and P. Wolper),
Proceedings Of The 12th International
Colloquium On Automata, Languages And Programming, Greece, August 1985.
- Can Message Buffers be Characterized in Linear Temporal Logic(with
E.M.Clarke, N.Francez and Y.Gurevich), Proceedings of ACM SIGACT/SIGOPS Symposium
on Principles of Distributed Computing, Ottawa, Canada, 1982.
- Reasoning about Infinite Computations(with M.Vardi, P.Wolper),
Proceedings
of IEEE Symposium on Foundations of Computer Science, Tucson,Arizona, October,
1983.
- Triple Exponential Decision Procedure for the Logic CTL*
(with E. A. Emerson),
Workshop on Logics of Programs, Carnegie-Mellon University, Pittsburgh,
Pennsylvania, June 1983.
- Distributed Algorithms to Ensure Fair Interprocess Communications,
Proceedings ACM SIGACT/SIGOPS Symposium on Principles of Distributed Computing,
Vancouver,Canada, August 1984.
- On Characterization of Safety and Liveness Properties in Temporal
Logic,
Proceedings of the 4th ACM SIGACT/SIGOPS Symposium on Principles of Distributed
Computing, Minaki,Canada, August 1985.
- Reasoning with Many Processes (with S. M. German),
Proceedings of the second IEEE Symposium On Logic in Computer Science, Cornell
University, Ithaca, June 1987.
- On the Eventuality Operator in Temporal Logic (with Lenore Zuck),
Proceedings of the second IEEE Symposium On Logic in Computer Science, Cornell
University, Ithaca, June 1987.
- Using Temporal Logic for Automatic Verification of Finite State
Systems
(with M.Browne, E.M.Clarke and E.A.Emerson), Proceedings of the Advanced Course
"Logics and Models for Verifications and Specifications of Concurrent Systems", Colle-sur-Loup, France, October 1984, Also Appeared in Springer-verlag
Lecture Notes in Computer Science.
- Efficient Distributed Recovery Using Message Logging (With
Jennifer Welch),
Proceedings Of The 8th Acm Symposium On Principles Of Distributed
Computing, August 1989, Edmonton, Canada.
- Quantitative Temporal Reasoning (With E.A. Emerson, Al Mok and Jai
Srinivasan), Proceedings Of The Workshop On Automatic Verification Methods
For Finite State Systems, June 1989, Grenoble, France.
- Automatic Temporal Verification of Buffer Systems
(with Lenore Zuck), Proceedings of the Workshop on Computer Aided Verification,
Denmark, June 1991.
- Symmetry and Modelchecking (with E. A. Emerson),
Presented at the Fifth International Conference on Computer Aided Verification, Elounda,
Crete, Greece June 28- July 1, 1993;
Appeared in Lecture Notes in Computer Science 697, Springer-Verlag.
- Modelchecking for fragments of $\mu$-calculus (with E. A. Emerson and C. S. Jutla),
Presented at the Fifth International Conference on Computer Aided Verification, Elounda,
Crete, Greece June 28- July 1, 1993;
Appeared in Lecture Notes in Computer Science 697, Springer-Verlag.
- Verification of a Real-life Protocol Using Symbolic Modelchecking (with
V. G. Naik), 6th International Conference on Computer Aided Verification,
Stanford, California, June 1994; Also appeared in Springer-Verlag Lecture Notes
in Computer Science.
- Data Replication for Mobile Computers (with Y. Huang and O. Wolfson),
Proceedings of the ACM-SIGMOD 1994 International Conference on Management of Data,
Minneapolis, Minnesotta, May 1994.
- Reasoning about Spatial Relationships in Picture Retrieval Systems
(with C. Yu and R. Haddad), Proceedings of the 20th VLDB Conference, Sept 12-15
1994, Santiago, Chile.
- Temporal Conditions and Integrity Constraints (with O. Wolfson),
Proceedings of the ACM-SIGMOD 1995 International Conference on Management of Data,
San Jose, California, May 1995.
- Temporal Condition Evaluation and Retroactive/Proactive Updates
in ACtive Database Systems, International Workshop on Active
and Realtime Database Systems, June 1995, Skovde, Sweden.
- Similarity based Retrieval of Pictures Using Indices on
Spatial Relationships
(with C. Yu et al.), Proceedings of the 21st VLDB Conference, Sept 1995, Zurich, Switzerland.
- Utilizing Symmetry when Modelchecking Under Fairness Assumptions,
(with E. A. Emerson), International Conference on Computer Aided Verification,
Leize, Belgium, July 1995.
- G-tree: Performance evaluation and application in
Fuzzy databases (with C. Yu et al),
International Conference on Information and
Knowlege Management 1996 ( accepted for presentation).
- Modeling and Querying Moving Objects (with Ouri Wolfson et al),IEEE International Conference on Data Engineering, April 1997, Birmingham, U.K.
- Similarity based Retrieval of Videos (with C. Yu and R. Venkatasubramanian),
IEEE International Conference on Data Engineering, April 1997,
Birmingham, U.K.
- An Architecture for Consumer-Oriented Online Database Services
(with Ouri Wolfson et al), Research Issues in Data Engineering
Workshop 1996 (RIDE'96), NewOrleans, Louisiana.
- Modeling and Querying Moving Objects (with Ouri Wolfson et al),
IEEE International Conference on Data Engineering, April 1997, Birmingham, U.K.
- Similarity based Retrieval of Videos (with C. Yu and
R. Venkatasubramanian),
IEEE International Conference on Data Engineering, April 1997, Birmingham, U.K.
- On-the-fly Modelchecking under Fairness that Exploits Symmetry
(with V. Gyuris), 9th International Conference on
Computer Aided Verification, Haifa, Israel, June 1997;
Springer-Verlag Lecture Notes in Computer Science 1254.
- Parametrized Verification of Linear Networks using
Automata as Invariants,
9th International Conference on
Computer Aided Verification, Haifa, Israel, June 1997;
Springer-Verlag Lecture Notes in Computer Science 1254.
- SMC: A Symmetry based ModelChecker for Verification
of Liveness Properties, Preliminary version presented in
9th International Conference on
Computer Aided Verification, Haifa, Israel, June 1997;
Springer-Verlag Lecture Notes in Computer Science 1254.
- Query Processing in Video Retrieval Systems
(with K. Liu, C. Yu and Rishie), 14th Intnl Conference on Data Engineering,
Orlando, Florida, March 1998.
- View Maintenance in Mobile Computing (with O. Wolfson, S. Dao,
K. Narayanan, R. Raj), SIGMOD RECORD, Association
of Computing Machinery Press, Dec. 1995.
- Symmetry Reductions in Model Checking (with Clarke, Emerson and Jha),
10th International Conference on Computer Aided Verification,
Vancouver, Canada, June 1998.
- Databases for Tracking Mobile Units in Real Time (with O. Wolfson et al),
Proceedings of the Seventh International
Conference on Database Theory (ICDT), Jerusalem, Israel,
Jan. 10-12, 1999, also to appear in the Springer-Verlag Lecture Notes in
Computer Science.
- DOMINO : Database for Moving Object Tracking (with O. Wolfson
et al), ACM Symposium on
Modification of Data (demo paper), June 1999, Philadelphia, Pennsylvania.
- Tracking Objects using Database TechnologY: DOMINO,
(with O. Wolfson, et al), The fourth workshop on Next Generation Information
Technologies and Systems (NGITS '99), Israel, July 1999.
- Symmetry and Reduced Symmetry in Modelchecking (with P. Godefroid),
International Conference on Computer Aided Verification, July 2001, Paris, France.
- Similarity based Retrieval from Sequence Databases using Automata as Queries
(with Tao Hu and Vikas Choudhry),
Eleventh International Conference on Knowledge and Information Management, Nov 4-9, 2002, McLean, VA.
- Formal Languages and Algorithms for Similarity based Retrieval from Sequence Databases,
12th International Conference on Foundations of Software Technology and Theoretical Computer Science,
Dec 12-14, 2002, Indian Institute of Technology, Kanpur; Also to in Springer-Verlag Lecture Notes in Computer Science.
- An Economic Model for Resource Exchange in Mobile Peer to Peer Networks
(with O. Wolfson and B. Xu),
16th International Conference on Scientific and Statistical Database Management (SSDBM),
June 2004, Santorini Island, Greece.
- Applications of a Transportation Information Architecture,
(with J. Dillenbrug, Nelson et al),
Proc. of the IEEE International conference on networking,
Sensing, and Control (ICNSC 2004), Taipei, Taiwan, Mar. 2004.
- Checking Extended CTL properties using Guarded Quotient Structures
(with Xiaodong Wang, Min Zhou), Proceedings of IEEE Sysmposium on
Software Engineering and Formal Methods, Beijing, Septmeber 2004.
- Model checking of Systems employing Commutative Functions
(with Xiaodong Wang, Min Zhou), To be presented at the International Conference
on Verification, Model checking and Abstract Interpretation, Paris,
January, 2005.
- Language based Policy Analysis in SPKI Trust Management Systems
(with Arun Eamani) To be presented at the Fourth Annual PKI Annual R\&D
Workshop: Multuple Paths to Trust, NIST Gaithersburg, Maryland, April 2005.
- Taming Interface Specifications
(with T. Margaria, B. Steffan and L. D. Zuck), revised version of the paper
that appeared in CONCUR 2005 conference, Sept 2005.
OTHER REFEREED ARTICLES
OTHER ARTICLES
- Triggers on Database Histories (with Ouri Wolfson), Bulletin of the Technical Committee
on Data Engineering, December 1992, Vol 15, No 1-4, IEEE Compute Society.
- Scholarly Review on Concurrency appeared in IEEE Computing Reviews; also published in
SIGACT NEWS.
- A Graph Model for Wong and Youseffi's Decomposition - A Strategy
for Query
Processing, Tech Report TR-06-81, Aiken Computational Laboratory, Harvard
University 1981.