Publications (by topic)

Crowdsourcing, Reputation Systems, Collaboration

• L. de Alfaro, B. Adler. Content-Driven Reputation for Collaborative Systems. In Proceedings of Trustworthy Global Computing 2013. Lecture Notes in Computer Science, Springer, 2013. PDF
• L. de Alfaro, M. Shavlovsky. CrowdGrader: Crowdsourcing the Evaluation of Homework Assignments. Technical report UCSC-SOE-13-11, August 2013. Abstract, PDF
• L. de Alfaro, M. Shavlovsky. Attributing Authorship of Revisioned Content. Proceedings of WWW 2013: 22nd International Conference on the World Wide Web, 2013. PDF
• V. Polychronopoulos, L. de Alfaro, J. Davis, H. Garcia-Molina, N. Polyzotis. Human-Powered Top-k Lists. InProceedings of the 16th International Workshop of the Web and Databases (WebDB), 2013. PDF
• A. Adabi and L. de Alfaro. Towards a Social Graph Recommendation Algorithm: Do We Trust Our Friends in Movie Recommendations? In Proceedings of On the Move to Meaningful Internet Systems: OTM 2012 Workshops. Lecture notes in Computer Science 7567, pages 637-647, Springer Verlag, 2012. PDF
  • L. de Alfaro, A. Kulshreshtha, I. Pye, B.T. Adler. Reputation Systems for Open Collaboration. Communications of the ACM, Volume 54, Issue 8, August 2011. PDF (author's version)
  • B.T. Adler, L. de Alfaro, S.M. Mola-Velasco, P. Rosso, A.G. West. Wikipedia Vandalism Detection: Combining Natural Language, Metadata, and Reputation Features. In CICLING 2011: Proceedings of the 12th International Conference on Intelligent Text Processing and Computational Linguistics, LNCS 6609, pages 277-288, Springer Verlag, 2011. PDF
  • B.T. Adler, L. de Alfaro, I. Pye. Detecting Wikipedia Vandalism Using WikiTrust. PAN lab report, CLEF (Conference on Multilingual and Multimodal Information Access Evaluation), 2010. PDF
  • K. Chatterjee, L. de Alfaro, I. Pye. Robust Content-Driven Reputation. In Proceedings of AISec 08: First ACM Workshop of AISec, ACM Press, 2008. Abstract PDF
  • B.T. Adler, K. Chatterjee, L. de Alfaro, M. Faella, I. Pye, V. Raman. Assigning Trust to Wikipedia Content. In WikiSym 2008: International Symposium on Wikis. Abstract PDF
  • B.T. Adler, L. de Alfaro, I. Pye, V. Raman. Measuring Author Contributions to the Wikipedia. In WikiSym 2008:International Symposium on Wikis. Abstract PDF
  • K. Chatterjee, L. de Alfaro, I. Pye. Robust Content-Driven Reputation. Technical Report UCSC-SOE-08-09, School of Engineering, University of California, Santa Cruz, CA, USA. May 2008. Abstract PDF
  • B.T. Adler, L. de Alfaro, I. Pye, V. Raman. Measuring Author Contributions to the Wikipedia. Technical Report UCSC-SOE-08-08, School of Engineering, University of California, Santa Cruz, CA, USA. May 2008. Abstract PDF
  • B.T. Adler, K. Chatterjee, L. de Alfaro, M. Faella, I. Pye, V. Raman. Assigning Trust to Wikipedia Content. Technical Report UCSC-SOE-08-07, School of Engineering, University of California, Santa Cruz, CA, USA. May 2008. This report supersedes the Technical Report UCSC-CRL-07-09, School of Engineering, University of California, Santa Cruz, CA, USA. Abstract PDF
  • B.T. Adler, J. Benterou, K. Chatterjee, L. de Alfaro, I. Pye, V. Raman. Assigning Trust To Wikipedia Content.Technical Report UCSC-CRL-07-09, School of Engineering, University of California, Santa Cruz, CA, USA. November 2007. Abstract PDF
  • B.T. Adler, L. de Alfaro. A Content-Driven Reputation System for the Wikipedia. In WWW 2007, Proceedings of the 16th International World Wide Web Conference, ACM Press, 2007. Abstract Postscript PDF
  • B.T. Adler, L. de Alfaro. A Content-Driven Reputation System for the Wikipedia. Technical report ucsc-crl-06-18, School of Engineering, University of California, Santa Cruz, November 2006. Abstract Postscript PDF Errata Corrige:Postscript PDF
  • A revised version of this paper has been accepted at WWW 2007.
  • L. de Alfaro. Model Checking the World Wide Web. In CAV 01: 13th Conference on Computer Aided Verification,Lecture Notes in Computer Science 2102, pages 337-349, Springer-Verlag, 2001. Postscript PDF
  • L. de Alfaro, T.A. Henzinger, and F.Y.C. Mang. MCWEB: A Model-Checking Tool for Web Site Debugging. Poster presented at the 10th World Wide Web Conference, Hong Kong, 2001. Postscript PDF

Game Theory

• K. Chatterjee, L. de Alfaro, R. Majumdar, V. Raman. Algorithms for Game Metrics. Logical Methods in Computer Science, Volume 6 (3:13), pages 1-27, 2010. PDF
• L. de Alfaro, P. Roy. Solving Games via Three-Valued Abstraction Refinement. Information and Computation, volume 208, issue 6, pages 666-676, June 2010. PDF
• K. Chatterjee, L. de Alfaro, T.A. Henzinger. Termination Criteria for Solving Concurrent Safety and Reachability Games. In Proceedings of SODA 09: ACM-SIAM Symposium on Discrete Algorithms, ACM Press, 2009. Abstract PDF
• L. de Alfaro, R. Majumdar, V. Raman, M. Stoelinga. Game Refinement Relations and Metrics. Logical Methods in Computer Science, volume 4, issue 3, 2008. Abstract PDF
• K. Chatterjee, L. de Alfaro, T.A. Henzinger. Strategy Improvement for Concurrent Safety Games. Technical Report UCSC-SOE-08-04, School of Engineering, University of California, Santa Cruz, CA, USA. April 2008. Abstract PDF
• K. Chatterjee, L. de Alfaro, T.A. Henzinger. Qualitative Concurrent Parity Games. Technical Report UCSC-CRL-08-02, School of Engineering, University of California, Santa Cruz, CA, USA. April 2008. Abstract PDF
• L. de Alfaro, M. Faella. Accelerated Algorithms for 3-Color Parity Games with an Application to Timed Games.In CAV 2007: Proceedings of the 19th International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Springer-Verlag, 2007. Abstract Postscript PDF
• L. de Alfaro, T.A. Henzinger, O. Kupferman. Concurrent Reachability Games. In Theoretical Computer Science 386 (3), 188-217. Elsevier, 2007. Abstract PDF
• L. de Alfaro, P. Roy. Solving Games via Three-Valued Abstraction Refinement. In CONCUR 2007: Proceedings of the 18th International Conference on Concurrency Theory, Lecture Notes in Computer Science, Springer-Verlag, 2007.Abstract Postscript PDF
• L. de Alfaro, R. Majumdar, V. Raman, M. Stoelinga. Game Relations and Metrics. In LICS 2007: Proceedings of the 22nd IEEE Symposium on Logic in Computer Science, 2007. Abstract Postscript PDF
• L. de Alfaro, M. Faella. Accelerated Algorithms for 3-Color Parity Games with an Application to Timed Games.In CAV 2007: Proceedings of the 19th International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Springer-Verlag, 2007. Abstract Postscript PDF
• K. Chatterjee, L. de Alfaro, T.A. Henzinger. Strategy Improvement for Concurrent Reachability Games. In QEST 06: International Conference on Quantitative Evaluation of Systems, pages 291-300, IEEE Computer Society Press, 2006. Abstract Postscript PDF
• K. Chatterjee, L. de Alfaro, T.A. Henzinger. The Complexity of Quantitative Concurrent Parity Games. In SODA 06: ACM-SIAM Symposium on Discrete Algorithms, pages 678-687, ACM Press, 2006. Postscript PDF
• B.T. Adler, L. de Alfaro, M. Faella. Average Reward Timed Games. In FORMATS 05: International Conference on Formal Modelling and Analysis of Timed Systems, Lecture Notes in Computer Science 3829, pages 65-80, Springer-Verlag, 2005. Postscript PDF
• K. Chatterjee, L. de Alfaro, T.A. Henzinger. The Complexity of Stochastic Rabin and Streett Games. In ICALP 05: 31st International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 3580, pages 878-890, Springer-Verlag, 2005. Postscript PDF
• K. Chatterjee, L. de Alfaro, and T.A. Henzinger. Trading Memory for Randomness. In QEST 04: 1st International Conference on the Quantitative Evaluation of Systems, pages 206-217, IEEE Computer Society Press, 2004. PostscriptPDF
• L. de Alfaro, P. Godefroid, and R. Jagadeesan. Three-Valued Abstractions of Games: Uncertainty, but with Precision. In LICS 04: Proceedings of 19th IEEE Symposium on Logic in Computer Science, pages 170-179, 2004.Postscript PDF
• L. de Alfaro and R. Majumdar. Quantitative Solution of Omega-Regular Games. In Journal of Computer and System Sciences 68, pages 374-397, 2004. Postscript PDF
• A preliminary version of this paper appeared in STOC 01: 33rd Annual ACM Symposium on Theory of Computing,2001.
• L. de Alfaro and M. Faella. Information Flow in Concurrent Games. In ICALP 03: 30th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 2719, pages 1038-1053, Springer-Verlag, 2003. Postscript PDF
• L. de Alfaro. Quantitative Verification and Control via the Mu-Calculus. In CONCUR 03: Concurrency Theory, 14th International Conference, Lecture Notes in Computer Science 2761, pages 103-127, Springer-Verlag, 2003. PostscriptPDF
• L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, and M. Stoelinga. The Element of Surprise in Timed Games.In CONCUR 03: Concurrency Theory, 14th International Conference, Lecture Notes in Computer Science 2761, pages 144-158, Springer-Verlag, 2003. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and R. Majumdar. Discounting the Future in Systems Theory. In ICALP 03: 30th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 2719, pages 1022-1037, Springer-Verlag, 2003. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and M. Stoelinga. Timed Interfaces. In EMSOFT 02: Proceedings of the Second International Workshop on Embedded Software, Lecture Notes in Computer Science 2491, pages 108-122, Springer-Verlag, 2002. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and R. Majumdar. Symbolic Algorithms for Infinite-State Games. In CONCUR 01: Concurrency Theory, 12th International Conference, Lecture Notes in Computer Science 2154, pages 536-550, Springer-Verlag, 2001. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and R. Majumdar. From Verification to Control: Dynamic Programs for Omega-Regular Objectives. In LICS 01: 16th International IEEE Symposium on Logic in Computer Science, pages 279-290, IEEE press, 2001. Postscript PDF
• L. de Alfaro and R. Majumdar. Quantitative Solution of Omega-Regular Games. In STOC 01: 33rd Annual ACM Symposium on Theory of Computing, 2001. Postscript PDF
• An extended version of this paper appeared in Journal of Computer and System Sciences 68, pages 374-397, 2004.
• L. de Alfaro and T.A. Henzinger. Concurrent Omega-Regular Games. In LICS 2000: 15th International IEEE Symposium on Logic in Computer Science, pages 141-154, IEEE press, 2000. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and O. Kupferman. Concurrent Reachability Games. In FOCS 98: 39th Annual IEEE Symposium on Foundations of Computer Science, pages 564-575, IEEE Press, 1998. Postscript PDF
• An extended version is available as Technical report UCB/ERL M98/33, University of California at Berkeley, 1998.Postscript PDF

Theory of Components

• L. de Alfaro, M. Faella, A. Legay. An Introduction to the Tool Ticc. Technical report ucsc-crl-06-14, School of Engineering, University of California, Santa Cruz, 2006. Also to appear in Proc. of Trustworthy Workshop Software, Saarbrücken, August 2006, to be published in Dagstuhl online proceedings. Postscript PDF
• B.T. Adler, L. de Alfaro, L. Dias Da Silva, M. Faella, A. Legay, V. Raman, P. Roy. Ticc: A Tool for Interface Compatibility and Composition. In CAV 06: Computer-Aided Verification, Lecture Notes in Computer Science 4144, pages 59-62, Springer-Verlag, 2006. Postscript PDF
• An extended version of this paper has been published as the Technical Report ucsc-crl-06-01, School of Engineering, University of California, Santa Cruz, 2006. Postscript PDF
• L. de Alfaro, M. Faella, R. Majumdar, V. Raman. Code Aware Resource Management. In EMSOFT 05: Fifth ACM International Conference on Embedded Software, pages 191-202, ACM Press, 2005. Postscript PDF
• L. de Alfaro, T.A. Henzinger. Interface-based Design. In Engineering Theories of Software-intensive Systems (M. Broy, J. Gruenbauer, D. Harel, and C.A.R. Hoare, eds.), NATO Science Series: Mathematics, Physics, and Chemistry, Vol. 195, Springer, 2005, pp. 83-104. Abstract Postscript PDF
• L. de Alfaro, L. Dias Da Silva, M. Faella, A. Legay, P. Roy, M. Sorea. Sociable Interfaces. In FROCOS 2005: 5th International Workshop on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 3717, pages 81-105, Springer-Verlag, 2005. Postscript PDF
• L. de Alfaro and M. Stoelinga. Interfaces: A Game-Theoretic Framework to Reason about Open Systems. InFOCLASA 03: Proceedings of the 2nd International Workshop on Foundations of Coordination Languages and Software Architectures, 2003. In Electronic Notes on Theoretical Computer Science, Elsevier Science Publishers. Postscript PDF
• L. de Alfaro. Game Models for Open Systems. In Proceedings of the International Symposium on Verification (Theory in Practice), Lecture Notes in Computer Science 2772, pages 269-289, Springer-Verlag, 2003. AbstractPostscript PDF
• A. Chakrabarti, L. de Alfaro, T.A. Henzinger, and M. Stoelinga. Resource Interfaces. In EMSOFT 03: Proceedings of the 3rd International Workshop on Embedded Software, Lecture Notes in Computer Science 2855, pages 117-133, Springer-Verlag, 2003. Postscript PDF
• R. Passerone, L. de Alfaro, T.A. Henzinger, and A.L. Sangiovanni-Vincentelli. Convertibility Verification and Converter Synthesis: Two Faces of the Same Coin. In ICCAD 02: Proceedings of the International Conference on Computer Aided Design, pages 132-139, IEEE Computer Society Press, 2002. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and M. Stoelinga. Timed Interfaces. In EMSOFT 02: Proceedings of the Second International Workshop on Embedded Software, Lecture Notes in Computer Science 2491, pages 108-122, Springer-Verlag, 2002. Postscript PDF
• A. Chakrabarti, L. de Alfaro, T.A. Henzinger, M. Jurdzinski, and F.Y.C. Mang. Interface Compatibility Checking for Software Modules. In CAV 02: 14th International Conference on Computer Aided Verification, Lecture Notes in Computer Sciences, pages 428-441, Springer Verlag, 2002. Postscript PDF
• A. Chakrabarti, L. de Alfaro, T.A. Henzinger, and F.Y.C. Mang. Synchronous and Bidirectional Component Interfaces. In CAV 02: 14th International Conference on Computer Aided Verification, Lecture Notes in Computer Sciences, pages 414-427, Springer Verlag, 2002. Postscript PDF
• L. de Alfaro and T.A. Henzinger. Interface Theories for Component-Based Design. In EMSOFT 01: Proceedings of the First International Workshop on Embedded Software, Lecture Notes in Computer Science 2211, pages 148-165, Springer-Verlag, 2001. Postscript PDF
• L. de Alfaro and T.A. Henzinger. Interface Automata. In ESEC/FSE 01: Proceedings of the Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, pages 109-120, ACM Press, 2001. Abstract Postscript PDF

Embedded Software

• K. Chatterjee, L. de Alfaro, V. Raman, C. Sanchez. Analyzing the Impact of Change in Multi-threaded Programs.In FASE 2010: Fundamental Approaches to Software Engineering, ETAPS 2010, Lecture Notes in Computer Science 6013, pages 293-307, Springer-Verlag, 2010. PDF
• L. de Alfaro, M. Faella, R. Majumdar, V. Raman. Code Aware Resource Management. In EMSOFT 05: Fifth ACM International Conference on Embedded Software, pages 191-202, ACM Press, 2005. Postscript PDF
• A. Chakrabarti, L. de Alfaro, T.A. Henzinger, and M. Stoelinga. Resource Interfaces. In EMSOFT 03: Proceedings of the 3rd International Workshop on Embedded Software, Lecture Notes in Computer Science 2855, pages 117-133, Springer-Verlag, 2003. Postscript PDF
• R. Passerone, L. de Alfaro, T.A. Henzinger, and A.L. Sangiovanni-Vincentelli. Convertibility Verification and Converter Synthesis: Two Faces of the Same Coin. In ICCAD 02: Proceedings of the International Conference on Computer Aided Design, pages 132-139, IEEE Computer Society Press, 2002. Postscript PDF
• A. Chakrabarti, L. de Alfaro, T.A. Henzinger, M. Jurdzinski, and F.Y.C. Mang. Interface Compatibility Checking for Software Modules. In CAV 02: 14th International Conference on Computer Aided Verification, Lecture Notes in Computer Sciences, pages 428-441, Springer Verlag, 2002. Postscript PDF
• A. Chakrabarti, L. de Alfaro, T.A. Henzinger, and F.Y.C. Mang. Synchronous and Bidirectional Component Interfaces. In CAV 02: 14th International Conference on Computer Aided Verification, Lecture Notes in Computer Sciences, pages 414-427, Springer Verlag, 2002. Postscript PDF
• L. de Alfaro and T.A. Henzinger. Interface Theories for Component-Based Design. In EMSOFT 01: Proceedings of the First International Workshop on Embedded Software, Lecture Notes in Computer Science 2211, pages 148-165, Springer-Verlag, 2001. Postscript PDF
• L. de Alfaro and T.A. Henzinger. Interface Automata. In ESEC/FSE 01: Proceedings of the Joint 8th European Software Engineering Conference and 9th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, pages 109-120, ACM Press, 2001. Abstract Postscript PDF

Quantitative Systems Theory

• L. de Alfaro, M. Faella, M. Stoelinga. Linear and Branching System Metrics. IEEE Transactions on Software Engineering, pages 258-273, volume 35, number 2, March 2009. PDF
• L. de Alfaro, P. Roy. Magnifying-Lens Abstraction for Markov Decision Processes. In CAV 2007: Proceedings of the 19th International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Springer-Verlag, 2007. Abstract Postscript PDF
• K. Chatterjee, L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga. Compositonal Quantitative Reasoning. In QEST 06: International Conference on Quantitative Evaluation of Systems, pages 157-166, IEEE Computer Society Press, 2006. Postscript PDF
• L. de Alfaro, M. Faella, M. Stoelinga. Linear and Branching System Metrics. Technical Report ucsc-crl-05-01, School of Engineering, University of California, Santa Cruz, April 8, 2005. This is an extended and improved version of anICALP 2004 paper. Postscript PDF
• L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga. Model Checking Discounted Temporal Properties. In Theoretical Computer Science, Elsevier. This is the journal version of a TACAS 2004 paper. PostscriptPDF
• L. de Alfaro, M. Faella, and M. Stoelinga. Linear and Branching Metrics for Quantitative Transition Systems. InICALP 04: 31st International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 3142, pages 97-109, Springer-Verlag, 2004. Postscript PDF
• L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, and M. Stoelinga. Model Checking Discounted Temporal Properties. In TACAS 2004: 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 2988, pages 77-92, Springer-Verlag, 2004. Postscript PDF
• L. de Alfaro and R. Majumdar. Quantitative Solution of Omega-Regular Games. In Journal of Computer and System Sciences 68, pages 374-397, 2004. Postscript PDF
• A preliminary version of this paper appeared in STOC 01: 33rd Annual ACM Symposium on Theory of Computing,2001.
• L. de Alfaro. Quantitative Verification and Control via the Mu-Calculus. In CONCUR 03: Concurrency Theory, 14th International Conference, Lecture Notes in Computer Science 2761, pages 103-127, Springer-Verlag, 2003. PostscriptPDF
• L. de Alfaro, T.A. Henzinger, and R. Majumdar. Discounting the Future in Systems Theory. In ICALP 03: 30th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science 2719, pages 1022-1037, Springer-Verlag, 2003. Postscript PDF
• L. de Alfaro and R. Majumdar. Quantitative Solution of Omega-Regular Games. In STOC 01: 33rd Annual ACM Symposium on Theory of Computing, 2001. Postscript PDF
• An extended version of this paper appeared in Journal of Computer and System Sciences 68, pages 374-397, 2004.
• L. de Alfaro. From Fairness to Chance. In ENTCS: Electronic Notes on Theoretical Computer Science 22, Elsevier Science Publishers, 2000. Postscript PDF

System Control and Verification

• K. Chatterjee, L. de Alfaro, R. Majumdar. The Complexity of Coverage. In APLAS 2008: Asian Symposium on Programming Languages and Systems, Lecture Notes in Computer Science, volume 5356, pages 91-106, 2008.Abstract PDF
• K. Chatterjee, L. de Alfaro, R. Majumdar. The Complexity of Coverage. Technical Report UCSC-SOE-08-03, School of Engineering, University of California, Santa Cruz, CA, USA. April 2008. Abstract PDF
• L. de Alfaro, P. Roy. Solving Games via Three-Valued Abstraction Refinement. In CONCUR 2007: Proceedings of the 18th International Conference on Concurrency Theory, Lecture Notes in Computer Science, Springer-Verlag, 2007.Abstract Postscript PDF
• L. de Alfaro, T.A. Henzinger, and F.Y.C. Mang. The Control of Synchronous Systems Part II. In CONCUR 01: Concurrency Theory, 12th International Conference, Lecture Notes in Computer Science 2154, pages 566-581, Springer-Verlag, 2001. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and R. Majumdar. Symbolic Algorithms for Infinite-State Games. In CONCUR 01: Concurrency Theory, 12th International Conference, Lecture Notes in Computer Science 2154, pages 536-550, Springer-Verlag, 2001. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and R. Majumdar. From Verification to Control: Dynamic Programs for Omega-Regular Objectives. In LICS 01: 16th International IEEE Symposium on Logic in Computer Science, pages 279-290, IEEE press, 2001. Postscript PDF
• R. Alur, L. de Alfaro, R. Grosu, T. Henzinger, M. Kang, R. Majumdar, F. Mang, C. Meyer-Kirsch, and B.Y. Wang.JMocha: A Model Checking Tool that Exploits Design Structure. In ICSE 01: Proceedings of the 23rd International Conference on Software Engineering, pages 835-836, 2001. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and F.Y. Mang. The Control of Synchronous Systems. In CONCUR 00: Concurrency Theory, 11th International Conference, Lecture Notes in Computer Science 1877, pages 458-473, Springer Verlag, 2000. Postscript PDF
• L. de Alfaro, T.A. Henzinger, and F. Mang. Detecting Errors Before Reaching Them. In CAV 00: Proceedings of the 12th International Conference on Computer Aided Verification, Lecture Notes in Computer Science 1855, pages 186-201, Springer Verlag, 2000. Postscript PDF
• R. Alur, L. de Alfaro, R. Grosu, T. Henzinger, M. Kang, R. Majumdar, F. Mang, C. Meyer-Kirsch, and B.Y. Wang.Mocha: Exploiting Modularity in Model Checking. Unpublished, 2000. Postscript PDF
• R. Alur, L. de Alfaro, T.A. Henzinger, and F.Y. Mang. Automating Modular Verification. In CONCUR 99: Concurrency Theory, 10th International Conference, Lecture Notes in Computer Science 1664, pages 82-97, Springer Verlag, 1999.Postscript PDF

Verification of Probabilistic Systems

• K. Chatterjee, L. de Alfaro, M. Faella, A. Legay. Qualitative Logics and Equivalences for Probabilistic Systems.Logical Methods in Computer Science, volume 5, issue 2, 2009. Abstract PDF
• K. Chatterjee, L. de Alfaro, R. Majumdar, V. Raman. Algorithms for Game Metrics. In Proceedings of FSTTCS 08: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Abstract PDF An extended version of this paper can be found on Arxiv.
• P. Roy, D. Parker, G. Norman, L. de Alfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes.In QEST 2008: Proceedings of the International Conference on Evaluation of Systems, 2008. Abstract PDF
• P. Roy, D. Parker, G. Norman, L. de Alfaro. Symbolic Magnifying Lens Abstraction in Markov Decision Processes.Technical Report UCSC-SOE-08-05, School of Engineering, University of California, Santa Cruz, CA, USA. May 2008.Abstract PDF
• L. de Alfaro, P. Roy. Magnifying-Lens Abstraction for Markov Decision Processes. In CAV 2007: Proceedings of the 19th International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, Springer-Verlag, 2007. Abstract Postscript PDF
• L. de Alfaro, T.A. Henzinger, and R. Jhala. Compositional Methods for Probabilistic Systems. In CONCUR 01: Concurrency Theory, 12th International Conference, Lecture Notes in Computer Science 2154, pages 351-365, Springer-Verlag, 2001. Postscript PDF
• L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala. Symbolic Model Checking of Concurrent Probabilistic Processes Using MTBDDs and the Kronecker Representation. In TACAS 00: 6th International Worskshop on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 1785, pages 395-410, Springer-Verlag, 2000. Postscript PDF
• L. de Alfaro. From Fairness to Chance. In ENTCS: Electronic Notes on Theoretical Computer Science 22, Elsevier Science Publishers, 2000. Postscript PDF
• L. de Alfaro. Computing Minimum and Maximum Reachability Times in Probabilistic Systems. In CONCUR 99: 10th International Conference on Concurrency Theory, Lecture Notes in Computer Science 1664, pages 66-81, Springer Verlag, 1999. Postscript PDF
• L. de Alfaro. Stochastic Transition Systems. In CONCUR 98: 9th International Conference on Concurrency Theory,Lecture Notes in Computer Science 1466, pages 423-438, Springer-Verlag, 1998. Postscript PDF
• L. de Alfaro. How to Specify and Verify the Long-Run Average Behavior of Probabilistic Systems. In LICS 98: 13th Annual IEEE Symposium on Logic in Computer Science, IEEE Press, pages 454-465, 1998. Postscript PDF
• L. de Alfaro. Formal Verification of Probabilistic Systems. Ph.D. Dissertation, Stanford University, 1997. Technical report STAN-CS-TR-98-1601. Abstract Postscript PDF
• Errata Corrige: Postscript PDF
• L. de Alfaro. Temporal Logics for the Specification of Performance and Reliability. In STACS 97: 14th Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 1200, pages 165-176, Springer Verlag, 1997. Postscript PDF
• Erraga Corrige: Postscript PDF
• A. Bianco and L. de Alfaro. Model Checking of Probabilistic and Nondeterministic Systems. In FST TCS 95: Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 1026, pages 499-513. Springer-Verlag, 1995. Postscript PDF

Deductive Methods for Verification

• L. de Alfaro and A. Kapur. Hybrid Diagrams. Theoretical Computer Science 290(1), pages 565-597, 2002. PostscriptPDF
• L. de Alfaro, Z. Manna, and H.B. Sipma. Decomposing, Transforming and Composing Diagrams: The Joys of Modular Verification. Technical report STAN-CS-98-1614, Stanford University, 1998. Postscript PDF
• L. de Alfaro, Z. Manna, H.B. Sipma, and T. Uribe. Visual Verification of Reactive Systems. In TACAS 97: 3rd International Worskshop on Tools and Algorithms for the Construction and Analysis of Systems, Lectures Notes in Computer Science 1217, pages 334-350, Springer-Verlag, 1997. Postscript PDF
• L. de Alfaro, A. Kapur, and Z. Manna. Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification. In STACS 97: 14th Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 1200, pages 153-164, Springer Verlag, 1997. Postscript PDF
• A. Browne, L. de Alfaro, Z. Manna, H.B. Sipma, and T.E. Uribe. Diagram-based Formalisms for the Verification of Reactive Systems. In CADE-13: Workshop on Visual Reasoning, 1996. Postscript PDF
• L. de Alfaro and Z. Manna. Temporal Verification by Diagram Transformations. In CAV 96: 8th International Conference on Computer Aided Verification Lecture Notes in Computer Science 1102, pages 288-299, Springer Verlag, 1996. Postscript PDF
• Z. Manna, A. Anuchitanukul, N. Bjorner, A. Browne, E. Chang, M. Colon, L. de Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Stanford University, 1994.

Error Correcting Codes

• L. de Alfaro and A.R. Meo. Codes for Second and Third Order GH-ARQ Schemes. IEEE Transactions on Communication 42(2-4) pages 899-910, 1994. Postscript PDF