Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Luca de Alfaro: Publications
Luca de Alfaro: Publications
Most of the papers available from this page appear in print, and the
corresponding copyright is held by the publisher. While the papers
provided here can be accessed for personal use, redistribution, or
reprinting for commercial purposes, is prohibited.
Recent work
L. de Alfaro, T.A. Henzinger.
Interface-Based Design.
In Engineering Theories of Software Intensive Systems,
proceedings of the Marktoberdorf Summer School, Kluwer, 2004.
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, 2004.
Postscript,PDF.
L. de Alfaro, P. Godefroid, R. Jagadeesan.
Three-Valued Abstractions of Games:
Uncertainty, but with Precision.
In LICS 04: Proceedings of 19th IEEE Symposium on Logic in
Computer Science, 2004.
Postscript,PDF.
L. de Alfaro, M. Faella, M. Stoelinga.
Linear and Branching Metrics
for Quantitative Transition Systems.
In ICALP 04: 31st International Colloquium on Automata, Languages,
and Programming, LNCS, Springer-Verlag, 2004.
Postscript,PDF.
L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar,
M. Stoelinga.
Model Checking Discounted Temporal
Properties.
In TACAS 2004: 10th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, LNCS,
Springer-Verlag, 2004.
Postscript,PDF.
L. de Alfaro, R. Majumdar.
Quantitative Solution of Omega-Regular Games.
In Journal of Computer and System Sciences68, 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.
Interface theory
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.
Postscript,PDF.
L. de Alfaro.
Game Models for Open Systems.
To appear in Proceedings of the International Symposium on
Verification (Theory in Practice),
Lecture Notes in Computer Science 2772, Springer-Verlag, 2003.
Postscript,PDF.
A. Chakrabarti, L. de Alfaro, T.A. Henzinger, M. Stoelinga.
Resource Interfaces.
In EMSOFT 03: Proceedings of the 3rd International Workshop on
Embedded Software,
Lecture Notes in Computer Science 2855, Springer-Verlag, 2003.
Postscript,PDF.
R. Passerone, L. de Alfaro, T.A. Henzinger,
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, 2002.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, M. Stoelinga.
Timed Interfaces.
In EMSOFT 02: Proceedings of the Second International Workshop on
Embedded Software, Lecture Notes in Computer
Science, pages 108-122, Springer-Verlag, 2002.
Postscript,PDF.
A. Chakrabarti, L. de Alfaro, T.A. Henzinger,
M. Jurdzinski, 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, 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, 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, Springer-Verlag, 2001.
Postscript,PDF.
L. de Alfaro, 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,
2001.
Postscript,PDF.
There are some minor errors in the formalism proposed in this paper.
Please see the paper
Interface-Based Design
in the proceedings of Marktobderdorf 2004 for a revised
and corrected version of the formalism.
Game theory
L. de Alfaro, M. Faella, T.A. Henzinger, R. Majumdar, M. Stoelinga.
The Element of Surprise in Timed Games.
In CONCUR 03: Concurrency Theory, 14th International Conference,
Lecture Notes in Computer Science, Springer-Verlag, 2003.
Postscript,PDF.
L. de Alfaro, M. Faella.
Information Flow in
Concurrent Games.
In ICALP 03: 30th International Colloquium on Automata, Languages,
and Programming, Lecture Notes in Computer
Science, Springer-Verlag, 2003.
Postscript,PDF.
L. de Alfaro, 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 Sciences68, pages
374-397, 2004.
L. de Alfaro, T.A. Henzinger, R. Majumdar.
Symbolic Algorithms for Infinite-State Games.
In CONCUR 01: Concurrency Theory, 12th
International Conference, Lectures Notes in Computer Science,
Springer-Verlag, 2001.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, R. Majumdar.
From Verification to Control: Dynamic Programs for
Omega-Regular Objectives.
In LICS 01:
16th International IEEE Symposium on Logic in Computer Science,
IEEE press, 2001.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger.
Concurrent Omega-Regular Games.
In LICS 2000: 15th International
IEEE Symposium on Logic in Computer Science, IEEE press, 2000.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, 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.
Quantitative systems theory
L. de Alfaro.
Quantitative Verification and Control via
the Mu-Calculus.
In CONCUR 03: Concurrency Theory, 14th International Conference,
Lecture Notes in Computer Science, Springer-Verlag, 2003.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, R. Majumdar.
Discounting the Future in
Systems Theory.
In ICALP 03: 30th International Colloquium on Automata, Languages,
and Programming, Lecture Notes in Computer
Science, Springer-Verlag, 2003.
Postscript,PDF.
Component-based design and verification
L. de Alfaro, T.A. Henzinger, R. Jhala.
Compositional Methods for Probabilistic Systems.
In CONCUR 01: Concurrency Theory, 12th
International Conference, Lectures Notes in Computer Science,
Springer-Verlag, 2001.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, F.Y.C. Mang.
The Control of Synchronous Systems Part II.
In CONCUR 01: Concurrency Theory, 12th
International Conference, Lectures Notes in Computer Science,
Springer-Verlag, 2001.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, F.Y. Mang.
The Control of Synchronous Systems.
In CONCUR 00: Concurrency Theory, 11th International
Conference, Lecture Notes in Computer Sciences, Springer Verlag, 2000.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, F. Mang.
Detecting Errors Before Reaching Them.
In CAV 00: Proceedings of the 12th International
Conference on Computer Aided Verification, Lecture Notes in
Computer Sciences, Springer Verlag, 2000.
Postscript,PDF.
R. Alur, L. de Alfaro, T.A. Henzinger, F.Y. Mang.
Automating Modular Verification.
In CONCUR 99: Concurrency Theory, 10th International
Conference, Lecture Notes in Computer Sciences, Springer Verlag,
1999.
Postscript,PDF.
Probabilistic systems
L. de Alfaro, M. Kwiatkowska, G. Norman, D. Parker, 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, Lectures Notes in Computer Science, 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
Sciences, 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, 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.
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.
L. de Alfaro.
Formal Verification of Performance and
Reliability of Real-Time Systems.
Stanford University Technical Report STAN-CS-TR-96-1571, June 1996.
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.
Reactive systems, hybrid systems, and the Web
L. de Alfaro.
Model Checking the World Wide Web.
In CAV 01: 13th Conference on Computer Aided
Verification, Lectures Notes in Computer Science,
Springer-Verlag, 2001.
Postscript,PDF.
L. de Alfaro, T.A. Henzinger, 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.
Mocha: A Model Checking Tool that Exploits Design Structure.
In ICSE 01: Proceedings of the 23rd International Conference
on Software Engineering, 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.
Mocha: Exploiting Modularity in Model Checking.
Unpublished, 2000.
Postscript,PDF.
L. de Alfaro, Z. Manna, 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, 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, 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, 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 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.
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.
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.
L. de Alfaro.
Determination of automorphic codes.
In Proceedings of the International Conference on Digital Signal
Processing, pages 840-844. North Holland Press, 1987.