Papers and Reports: 1998-1999

Security Protocols Analysis

• Patrick Lincoln, John Mitchell, Mark Mitchell, and Andre Scedrov: "Probabilistic polynomial-time equivalence and security protocols", in the proceedings of the World Congress On Formal Methods in the Development of Computing Systems - FM'99, Toulouse, France, September 1999.
• Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov: "Undecidability of bounded security protocols", in the Proceedings of the Workshop on Formal Methods and Security Protocols - FMSP'99 (N. Heintze and E. Clarke, editors), Trento, Italy, July 1999. Revised version.
• Iliano Cervesato, Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov: "A Meta-Notation for Protocol Analysis", in the Proceedings of the Twelfth IEEE Computer Security Foundations Workshop - CSFW'99s (R. Gorrieri editor), pp. 55-69, IEEE Computer Society Press, Mordano, Italy, 28-30 June 1999.

• Cynthia Dwork and Amit Sahai: "Concurrent Zero Knowledge: Reducing the Need for Timing Constraints", in the Proceedings of the 18th Annual IACR Crypto Conference - CRYPTO'98, Santa Barbara, CA, August 1998.
• Cynthia Dwork, Moni Naor, and Amit Sahai: "Concurrent Zero Knowledge", in the Proceedings of the 30th Annual ACM Symposium on the Theory of Computing - STOC'98, Dallas, TX, May 1998.

Real-Time Systems

• Hanêne Ben-Abdallah, Insup Lee, and Oleg Sokolsky: "Specification and Analysis of Real-Time Systems with PARAGON", to appear in the Annals of Software Engineering, Baltzer Science Publishers, 1999.
• Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, and Mahesh Viswanathan: "Runtime Assurance Based On Formal Specifications", in the proceedings of the 1999 International Conference on Parallel and Distributed Processing Techniques and Applications - PDPTA'99 (H. Arabnia et al., editors), CSREA Press, Las Vegas, NV, 28 June - 1 July 1999.
• Moonjoo Kim, Mahesh Viswanathan, Hanêne Ben-Abdallah, Sampath Kannan, Insup Lee, and Oleg Sokolsky: "Formally Specified Monitoring of Temporal Properties", in the Proceedings of the European Conference on Real-Time Systems - ECRTS'99, pp. 114-121, York, UK, 9-11 June 1999.
• Moonjoo Kim, Mahesh Viswanathan, Hanêne Ben-Abdallah, Sampath Kannan, Insup Lee, and Oleg Sokolsky: "MaC: A Framework for Run-time Correctness Assurance of Real-Time Systems", Technical Report MS-CIS-98-37, Department of Computer and Information Sciences, University of Pennsylvania, December 1998.
• Hanêne Ben-Abdallah and Insup Lee: "A Graphical Language with Formal Semantics for the Specification and Analysis of Real-Time Systems", Special Issue of Integrated Computer-Aided Engineering on Real-time Engineering Systems, Vol. 5, No. 4, IOS Press, 1998.
• Hee-Hwan Kwak, Insup Lee, and Oleg Sokolsky: "Parametric Approach to the Specification and Analysis of Real-time System Designs based on ACSR-VP", in the proceedings of the 1998 ARO/ONR/NSF/DARPA Monterey Workshop on Engineering Automation for Computer Based Systems, Carmel, CA, 27-29 October 1998.
• Hee-Hwang Kwak, Jin-Young Choi, Insup Lee, and Anna Philippou: "Symbolic Weak Bisimulation for Value-Passing Calculi", Technical report MS-CIS-98-22, Department of Computer and Information Science, University of Pennsylvania, May 1998.

Result Checking

• Tugkan Batu, Ronitt Rubinfeld, and Patrick White: "Fast Approximate PCPs for Multidimensional Bin-Packing Problems", in the Proceedings of the Third International Workshop on Randomization and Approximation Techniques in Computer Science - APPROX-RANDOM'99 (D. Hochbaum, K. Jansen, J.P.D. Rolim, and A. Sinclair editors), pp. 245-256, Springer-Verlag LNCS 1671, Berkeley, CA, August 1999.
• Tugkan Batu, Ronitt Rubinfeld, and Patrick White: "Runtime Verification of Remotely Executed Code using Probabilistically Checkable Proof Systems", in the Proceedings of the Workshop on Run-Time Result Verification - RTRV'99, Trento, Italy, July 1999.
• Funda Ergün, S. Ravi Kumar, and Ronitt Rubinfeld: "Fast approximate PCPs", in the Proceedings of the 31st ACM Symposium on Theory of Computing - STOC'99, pp. 41-50, ACM Press, Atlanta, GA, 1-4 May 1999.
• Funda Ergün, Sampath Kannan, S. Ravi Kumar, Ronitt Rubinfeld, and Mahesh Viswanathan: "Spot-Checkers", to appear in the Journal of Computer and System Sciences, special issue on STOC'98.
• S. Ravi Kumar and Ronitt Rubinfeld: "Property Testing of Abelian Group Operations", manuscript.
• Joan Feigenbaum, Sampath Kannan, Martin Strauss, and Mahesh Viswanathan: "Streaming Algorithms for Distributed, Massive Data Sets", manuscript.

Complexity

• John Mitchell, Mark Mitchell, and Andre Scedrov: "A Linguistic Characterization of Bounded Oracle Computation and Probabilistic Polynomial Time", in the Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science - FOCS'98, pp. 725-733, IEEE Computer Society Press, Palo Alto, CA, November 1998.
• Patrick Lincoln, John Mitchell, Mark Mitchell, and Andre Scedrov: "A Probabilistic PolyTime Framework", in the Proceedings of the 5th ACM Conference on Computer and Communication Security - CCS-5, pp. 112-121, ACM Press, San Francisco, CA, November 1998.
• Iliano Cervesato, Massimo Francheschet, and Angelo Montanari: "The Complexity of Model Checking in Modal Event Calculi with Quantifiers", Electronic Transactions in Artificial Intelligence, vol. 2(1-2), January-June 1998, pp. 1-24.
• Joan Feigenbaum, Sampath Kannan, Moshe Y. Vardi, and Mahesh Viswanathan: "Complexity of Problems on Graphs Represented as OBDDs", in the Proceedings of the 15th Symposium on Theoretical Aspects of Computer Science - STACS'98, Paris, France, February 1998.
• Patrick Lincoln, John Mitchell, and Andre Scedrov: "Optimization Complexity of Linear Logic Proof Games", accepted for publication in Theoretical Computer Science.

Logic and Programming Languages

• Stephen Freund and John Mitchell: "A Type System for Object Initialization in the Java Bytecode Language", to appear in the ACM Transactions on Programming Languages and Systems (TOPLAS), ACM Press.
• Stephen Freund and John Mitchell: "A Formal Framework for the Java Bytecode Language and Verifier", to appear in the Proceedings of the 1999 ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA'99, Denver, CO, November 1999.
• Iliano Cervesato: "Logical Framework Design: Why not just classical logic?", accepted for publication in Information in Formation: Proceedings of the Seventh CSLI Workshop on Logic, Language and Computation (M. Faller, S. Kaufmann, M. Pauly editors), CSLI Publications, 1999.
• Stephen N. Freund and John C. Mitchell: "Specification and Verification of Java Bytecode Subroutines and Exceptions (summary)", Technical Note CS-TN-99-91, Computer Science Department, Stanford University, August 1999.
• Iliano Cervesato, Valeria de Paiva and Eike Ritter: "Explicit Substitutions for Linear Logical Frameworks: Preliminary Results", in the Proceedings of the Workshop on Logical Frameworks and Meta-languages - LFM'99, (A. Felty, editor), Paris, France, 28 September 1999.
• Stephen N. Freund: "The Costs and Benefits of Java Bytecode Subroutines", in the Proceedings of the Formal Underpinnings of Java Workshop at OOPSLA, Vancouver, Canada, October 1998.

Applications

• William Spears and Diana Gordon: "Using Artificial Physics to Control Agents", to appear in the Proceedings of the IEEE International Conference on Information, Intelligence, and Systems - ICIIS'99, Washington, DC, 1-3 November 1999.
• Diana Gordon, William Spears, Oleg Sokolsky, and Insup Lee: "Distributed Spatial Control and Global Monitoring of Mobile Agents", to appear in the Proceedings of the IEEE International Conference on Information, Intelligence, and Systems - ICIIS'99, Washington, DC, 1-3 November 1999.