Luca de Alfaro: Publications (by year)
2006
- 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
- L. de Alfaro, P. Roy. Magnifying-Lens Abstraction for Markov Decision Processes. Technical report ucsc-crl-06-15, School of Engineering, University of California, Santa Cruz, 2006. Abstract Postscript PDF
- 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
- 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, 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
- 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 - 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
2005
- 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
- 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, 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
- 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
- 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 an ICALP 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. Postscript PDF
2004
- 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. Postscript PDF
- L. de Alfaro, M. Faella, and M. Stoelinga. Linear and Branching Metrics for Quantitative Transition Systems. In ICALP 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, 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, 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.
2003
- L. de Alfaro and M. Stoelinga. Interfaces: A Game-Theoretic Framework to Reason about Open Systems. In FOCLASA 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. Abstract 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
- 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 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. 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
2002
- 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 A. Kapur. Hybrid Diagrams. Theoretical Computer Science 290(1), pages 565-597, 2002. Postscript PDF
2001
- 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
- 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. 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, 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. 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
- 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 and S. Gilmore (editors). Process Algebra and Probabilistic Methods, proceedings. Lecture Notes in Computer Science 2165, Springer-Verlag, 2001. Front matter: PDF
2000
- 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
- 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, 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
- 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
1999
- 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
- 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
1998
- 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 - 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, 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
1997
- 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, 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
- 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
1996
- 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
- L. de Alfaro. Formal Verification of Performance and Reliability of Real-Time Systems. Stanford University Technical Report STAN-CS-TR-96-1571, June 1996.
1995
- 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
- L. de Alfaro and Z. Manna. Verification in continuous time by discrete reasoning. In AMAST 95: 4th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science 936, pages 292-306, Springer-Verlag, 1995.
1994
- 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.
- L. de Alfaro. Logica Temporale e Sistemi in Tempo Reale. Doctoral Dissertation, Politecnico di Torino, 1994.
- 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
1987
- L. de Alfaro. Determination of automorphic codes. In Proceedings of the International Conference on Digital Signal Processing, pages 840-844. North Holland Press, 1987.