Sistla Web>Publications (revision 10)~~EditAttach~~

Publications

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, pp 244-263, Apr 1986.
Complexity of Propositional Linear Temporal Logics (with E.M.Clarke), Journal of the Association for Computing Machinery, Vol. 32, No. 3, pp 733-749, Jul 1985.
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, pp 88-112, Oct/Nov 1984.
Deciding Full Branching Time Logic (with E.A.Emerson), Information and Control, Vol. 61, No. 3, pp 175-201, Jun 1984.
A Multiprocess Network Logic with Temporal and Spatial Modalities (with J. Reif), Journal of Computer and System Sciences, Vol. 30, No. 1, pp 41-53, Feb 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, pp 217-237, 1987.
On Verifying That A Concurrent Program Satisfies A Nondeterministic Specification, Information Processing Letters 32, pp 17-23, 1989.
Reasoning About Systems With Many Processes (with S.M.German), Journal of the ACM, Vol. 39, No. 3, pp 675-735, Jul 1992.
Reasoning in a Restricted Temporal Logic (with Lenore Zuck), Information and Computation, Vol. 102, No. 2, pp 675-735, Feb 1993.
Proving Correctness with respect to Nondeterministic Safety Specifications, Information Processing Letters 39, pp 45-49, 1991.
Quantitative Temporal Reasoning (With E.A. Emerson, Al Mok and Jai Srinivasan), Journal of Real-Time Systems, 4, pp 331-352, 1992.
Safety, Liveness and Fairness in Temporal Logic, Formal Aspects in Computing, vol. 6, pp 495-511, 1994.
Temporal Triggers in Active Databases (with Ouri Wolfson), IEEE Transactions on Knowledge and Data Engineering, Vol. 7, No. 3, pp 471-486, Jun 1995.
Symmetry and Modelchecking (with E. A. Emerson), Formal Methods in System Design, 9(1/2), pp 105-130, 1996.
Hybrid and Incremental Modelchecking Techniques, ACM Computing Surveys, Vol. 28, No. 4es, Dec 1996.
Utilizing 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, pp 637-638, Jul 1997.
Minimization of Communication Cost Through Caching in Mobile Environments (with Ouri Wolfson), IEEE Transactions on Parallel and Distributed Systems, Vol 9, Number 4, pp 378-390, Apr 1998.
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), pp 411-452, Dec 1998.
Automatic Temporal Verification of Communicating Processes (with L. Zuck), to appear in the journal Science of Computer Programming.
On-the-fly Modelchecking under Fairness that Exploits Symmetry (with V. Gyuris), Formal Methods in System Design, Vol 15, Issue 3, pp 217-238, Nov 1999.
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.
A New Incremental Algorithm for Real-time systems with A. Sahay and J. Tsai), Journal of Software Engineering and Knowledge Engineering, Vol. 9, No. 2, 1999.
On Model-checking for mu-calculus and its fragments (with E. A. Emerson and C. Jutla), Theoretical Computer Sciecne 258(1-2), pp 491-522, 2001.
Reasoning about Qualitative Spatial Relationships (with C. Y. Yu), Journal of Automated Reasoning, Vol. 25, no. 4, pp 291-328, Nov 2000.
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, pp 133-166, Apr 2000.
Symmetry and Reduced Symmetry in Model Checking(with P. Godefroid), ACM Transactions on Programming Languages, Volume 26, Issue 4, pp 702-734, Jul 2004.
Employing Symmetry Reductions in Model Checking, Computer Languages, Systems and Structures 30, pp 99-137, invited paper, 2004.
Language Based Policy Analysis SPKI Trust Management Systems (with A. Eamani), Journal of Computer Security Volume 4, Number 4, pp 327-357, 2006.
Analysis of Dynamic Policies (with M. Zhou), Information and Computation, Vol 206/2-4, pp 185-212.
Checking Extended CTL Properties with Guarded Structures (with X. wand and M. Zhou), Formal Methods in System Design, Vol. 31, Issue 3, pp 197-219, Dec 2007.
On the Expressiveness and Complexity of Finite State Probabilistic Monitors (with R. Chadha and M. Viswanathan), Journal of the ACM, Vol. 56, Issue 5, Article 26, Aug 2009.

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, Jan 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., Apr-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, Jul 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, Aug 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, Oct, 1983.
Triple Exponential Decision Procedure for the Logic CTL* (with E. A. Emerson), Workshop on Logics of Programs, Carnegie-Mellon University, Pittsburgh, Pennsylvania, Jun 1983.
Distributed Algorithms to Ensure Fair Interprocess Communications, Proceedings ACM SIGACT/SIGOPS Symposium on Principles of Distributed Computing, Vancouver, Canada, Aug 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, Aug 1985.
Reasoning with Many Processes (with S. M. German), Proceedings of the second IEEE Symposium On Logic in Computer Science, Cornell University, Ithaca, Jun 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, Jun 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, Oct 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, Aug 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, Jun 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 Jun 28 - Jul 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 Jun 28- Jul 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, Jun 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, Santiago, Chile, Sep 12-15, 1994.
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, Jun 1995, Skovde, Sweden.
Similarity based Retrieval of Pictures Using Indices on Spatial Relationships (with C. Yu et al.), Proceedings of the 21st VLDB Conference, Sep 1995, Zurich, Switzerland.
Utilizing Symmetry when Modelchecking Under Fairness Assumptions, (with E. A. Emerson), International Conference on Computer Aided Verification, Leize, Belgium, Jul 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, Apr 1997, Birmingham, U.K.
Similarity based Retrieval of Videos (with C. Yu and R. Venkatasubramanian), IEEE International Conference on Data Engineering, Apr 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.
Similarity based Retrieval of Videos (with C. Yu and R. Venkatasubramanian), IEEE International Conference on Data Engineering, Apr 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, Jun 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, Jun 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, Jun 1997; Springer-Verlag Lecture Notes in Computer Science 1254.
Incremental Verification of Software Architecture, (with A. Sahay and J. Tsai), ACM SIGSOFT Notices, Oct 1997, pp 80-83.
Query Processing in Video Retrieval Systems (with K. Liu, C. Yu and Rishie), 14th Intnl Conference on Data Engineering, Orlando, Florida, Mar 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, Jun 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), Jun 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, Jul 1999.
Symmetry and Reduced Symmetry in Modelchecking (with P. Godefroid), International Conference on Computer Aided Verification, Jul 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), Jun 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, Sep 2004.
Model Checking Systems employing Commutative Functions (with Xiaodong Wang, Min Zhou), Proceedings of the Fourth the International Conference on Verification, Model checking and Abstract Interpretation, Paris, Jan 2005, Spinger-Verlag Lecture Notes in Computer Science LNCS 3385.
Combining Static Analysis and Model Checking for Systems Employing commutative Functions, FORTE 2005, Appeared in the Springer-Verlag Lecture
Notes in Computer Science, Oct 2005.
Language based Policy Analysis in SPKI Trust Management Systems (with Arun Eamani) Fourth Annual PKI Annual R\&D Workshop: Multuple Paths to Trust, NIST Gaithersburg, Maryland, Apr 2005.
Opportunistic Data Dissemination in Mobile Peer-to-Peer Networks, (with Bo Xu and Ouri Wolfson) 9th International Symposium on Spatial and Temporal Databases, Aug 2005.
Taming Interface Specifications (with T. Margaria, B. Steffan and L. D. Zuck), revised version of the paper that appeared in CONCUR 2005 conference, Sep 2005.
Merging Source Query Interfaces on Web Databases (with E, Dragut, W. Wu, C. Yu, W. Meng), 22nd International Conference on Data Engineering (ICDE'06), Atlanta, Georgia, Apr 2006.
Monitoring off-the-shelf Components, (with Min Zhou, Lenore Zuck), Proceedings of the seventh International Conference on Verification, Model checking and Abstract Interpretation, Jan, 2006 (VMCAI 2006), Springer-Verlag Lecture Notes in Computer Science, LNCS 3855.
Analysis of Dynamic Policies (with M. Zhou), Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol
Analysis, Seattle, Aug 15-16, 2006.
Verification of Object-Relational Maps, (with K. Mehra, S. Rajamani and S. Jha), Fifth IEEE Symposium on Software Engineering and
Formal Methods, London, Sep, 2007.PATENT
Monitoring Temporal Properties of Stochastic Systems (with A. Srinivas), Proceedings of the 9th International Conference
on Verification, Model checking and Abstract Interpretation, Jan, 2008 (VMCAI 2008), Springer-Verlag Lecture Notes in Computer Science.
CMV: Automatic Verification of Complete Mediation for Java Virtual Machines (with V. N. Venkatakrishnan, M. Zhou, H. Branske),
ACM Symposium on Information, Computer and Communication Security (ASIACCS'08), Tokyo 18-20 Mar 2008.
On the Expressiveness and Complexity of Randomization in Finite State Monitors (with R. Chadha, M. Viswanathan),
IEEE Symposium on Logic in Computer Science (LICS'08), Pittsburgh, Jun, 2008.
Preventing Information Leaks Through Shadow executions (with R. Capizzi, A. Longo and V. N. Venkatakrishnan), Annual Computer Security
Applications Conference (ACSAC 2008), Annaheim, California, Dec 2008.
Monitoring the Full range of Omega-regular properties of Stochastic Systems (with Kalpana Gondi and Yogesh Patel),
Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI2009), Savannah, Georgia, 2009.
A Query Processor for Prediction based Monitoring of Data Streams (with Sergio Illari, Ouri Wolfson, Eduardo Mena and Arantza Illarramendi) 12th International Conference on Extended Databased Technology (EDBT 2009), Mar 2009, St Petersburg, Russia.
A Data Model and Query Language for Urban Transport Systems (with Joel Booth, Ouri Wolfson and Isabel Cruz), 12th International Conference on Extended Databased Technology (EDBT 2009), Mar 2009, St Petersburg, Russia.
Power of Randomization in Automata on Infinite Strings (with R. Chadha and M. Viswanathan), 20th International Conference on
Concurrency Theory, Bolgna, Italy, Sep 2009 (CONCUR 2009).
Stop Word and Related Problems in Web Interface Integration (with Eduardo Draghut, Fang Fang, Clement Yu and Weiyi Meng), 35th International Conference on Very Large Database Systems, Lyon, France, Aug 2009 (VLDB 2009).
Automatically Preparing Safe SQL Queries (with Prithvi Bisht and V.N. Venkatakrishnan), to appear in 14th Financial Cryptography and Data Security Conference, Canary Islands, Spain, Jan 25-28, 2010.
TAPS: Automatically Preparing Safe SQL Queries (with Prithvi Bisht and V.N. Venkatakr- ishnan), ACM Conference on Computer and Communication Security 2010: 645-747, October, Chicago, Illinois (Demo paper).
Construction of a Sentimental Word Dictionary (with Eduardo Draghut, Weiyi Meng and Clement Yu), 19th ACM International Conference on Information and Knowledge Management (CIKM 2010), Toronto, Canada, October 26-30, 2010.
Model Checking Concurrent Programs with Nondeterminism and Randomization (with Rohit Chadha and Mahesh Viswanathan), 30th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS2010), Chennai, India, December 15-18, 2010.
Probabilistic Buchi Automata with Non-extremal Thresholds (with Rohit Chadha and Mahesh Viswanathan), 12th International Conference on Verification, Model checking abd Abstract Interpretation, Austin, Texas, January 23-25, 2011.
Monitorability in Dynalic Stochastic Systems (with M. Zefran and Yao Feng), 23rd In- ternational Conference on Computer Aided Verifications, July 14-20, Cliff Lodge, Utah, 2011.
Answer-Pairs and Processing of Continuous Nearest-Neighbor Queries (with Ouri Wolf- son and Bo Xu),The Seventh ACM SIGACT/SIGMOBILE International Workshop on Foundations of Mobile Computing (FOMC2011), June 2011.
Runtime Monitoring of Stochastic Cyber-Physical Systems with Hybrid State (with Milos Zefran and Yao Feng), 2nd International Conference on Runtime Verification (RV 2011), September 27 - September 30, 2011 San Francisco, California.
Polarity Consistency Checking for Sentiment Dictionaries (with Eduard Dragut, Hong Wang, Clement Yu, Weiyi Meng), ACL 2012 : The 50th Annual Meeting of the Associa- tion for Computational Linguistics, July 8-Jul 12, 2012, Jeju, Korea.

Publications

Journal Publications

Conference Publications

Other Articles