Luca de Alfaro

Professor

luca@ucsc.edu

Computer Science and Engineering

University of California, Santa Cruz

Ph.D. Stanford University, 1998

Exploring Subgroup Performance in End-To-End Speech Models.
In *Proceedings of the International Conference on Acoustings, Speech, and Signal Processing* (ICASSP), 2023.

A Hierarchical Approach to Anomalous Subgroup Discovery.
In *Proceedings of the 39th IEEE International Conference on Data Engineering* (ICDE), 2023.

Making Slotted ALOHA Efficient and Fair Using Reinforcement Learning.
*Computer Communications* 181, 58--68, 2022.

Identifying Biased Subgroups in Ranking and Classification.
In *Proceedings of the Responsible AI @ KDD 2021 Workshop*, 2021.

How Divergent Is Your Data?
In *Proceedings of the 47th International Conference on Very Large Data Bases (VLDB), Demo Track*, 2021.

Looking for Trouble: Analyzing Classifier Behavior via Pattern Divergence.
In *Proceedings of the 2021 ACM SIGMOD Conference*, 2021.

CONCUR Test-Of-Time Award 2021.
In *Proceedings of the 32nd International Conference on Concurrency Theory* (CONCUR 21), 2021.

Adaptive Policy Tree Algorithm to Approach Collision-Free Transmissions in Slotted ALOHA.
In *Proceedings of the 17th International Conference on Mobile Ad-Hoc and Smart Systems* (IEEE MASS), 2020.

Online Top-K Selection in Crowdsourcing Environments.
In *Proceedings of the 6th International Conference on Computing and Data Engineering* (ICCDE), 2020.

Using Reinforcement Learning in Slotted Aloha for Ad-Hoc Networks.
In *Proceedings of the 23rd International ACM Conference on Modeling, Analysis, and Simulation of Wireless and Mobile Systems* (MSWiM), pages 245-252, 2020.

An Adaptive Tree Algorithm to Approach Collision-Free Transmission in Slotted ALOHA.
In *Proceedings of the ACM SIGCOMM 2020 Workshop on Network Meets AI & ML (NetAI)*, 2020.

Approaching Fair Collision-Free Channel Access with Slotted ALOHA Using Collaborative Policy-Based Reinforcement Learning.
In *Proceedings of the IFIP Networking 2020 Conference*, 2020.

Learning Edge Properties in Graphs from Path Aggregations.
In *Proceedings of The Web Conference*, 2019.

A New Family of Neural Networks Provably Resistant to Adversarial Attacks.
Technical Report UCSC-SOE-19-01, 2019.

Automatic Online Fake News Detection Combining Content and Social Signals.
In *Proceedings of the 22nd Conference of Open Innovations Association* (FRUCT), 2018.

Automated Audience Segmentation Using Reputation Signals.
In *Proceedings of KDD 2018, the 24th ACM SIGKDD Conference on Knowledge Discovery and Data Mining*, 2018.

Efficient Techniques for Crowdsourced Top-k Lists.
In *Proceedings of the International Joint Conference on Artificial Intelligence* (IJCAI), 2017.

Efficient Selection of Pairwise Comparisons for Computing Top-Heavy Rankings.
In *Proceedings of the International Conference on Advances in Information Mining and Data Management* (IMMM), 2017.

Some Like It Hoax: Automated Fake News Detection in Social Networks.
In *Proceedings of the Second Workshop on Data Science for Social Good* (SoGood), Skopje, Macedonia. CEUR Workshop Proceedings Volume 1960, 2017.
Also available as arXiv:1704.07506, and as Technical Report UCSC-SOE-17-05.

Learning from Graph Neighborhoods Using LSTMs.
In *Proceedings of the AAAI Workshop on Crowdsourcing, Deep Learning and Artificial Intelligence Agents, 2017*, held with the 31st AAAI Conference (AAAI-17), 2017.
Also available as arXiv:1611.06882.

TrueReview: A Platform For Post-Publication Peer Review.
Technical Report UCSC-SOE-16-13, 2016.
Also available as arXiv:1608.07878.

Efficient Techniques for Crowdsourced Top-k Lists.
In *Proceedings of the Fourth AAAI Conference on Human Computation and Crowdsourcing* (HCOMP), 2016.

Predicting the quality of user contributions via LSTMs.
In *Proceedings of OpenSym 2016, the 12th International Symposium on Open Collaboration*, 2016.

Dynamics of Peer Grading: An Empirical Study.
In *Proceedings of the 9th International Conference on Educational Data Mining* (EDM), 2016.
A version appeared as the Technical Report UCSC-SOE-16-04, School of Engineering, University of California, Santa Cruz, 2016.

Reliable Aggregation of Boolean Crowdsourced Tasks.
In *Proceedings of the Third AAAI Conference on Human Computation and Crowdsourcing* (HCOMP), 2015.

WorkerRank: Using Employer Implicit Judgements to Infer Worker Reputation.
In *Proceedings of the Eight International Conference on Web Search and Data Mining* (WSDM), 2015.

CrowdGrader: A tool for crowdsourcing the evaluation of homework assignments.
In *Proceedings of SIGCSE 2014*, ACM, 2014.

On Assigning Implicit Reputation Scores in an Online Marketplace.
In *Proceedings of EDBT/ICDT, joint conference of International Conference on Extending Database Technology and International Conference on Database Theory*, 2014.

Strategy improvement for concurrent reachability and turn-based stochastic games.
Journal of Computer and System Sciences 79(5), 640-657, 2013.

Content-Driven Reputation for Collaborative Systems.
In *Proceedings of Trustworthy Global Computing* 2013. Lecture Notes in Computer Science, Springer, 2013.

The complexity of coverage.
International Journal of Foundations of Computer Science 24 (02), 165-185, 2013.

CrowdGrader: Crowdsourcing the Evaluation of Homework Assignments.
Technical report UCSC-SOE-13-11, August, 2013.
Also available as arXiv:1308.5273

Attributing Authorship of Revisioned Content.
In *Proceedings of the 22nd International Conference on the World Wide Web* (WWW), 2013.

Human-Powered Top-k Lists.
In *Proceedings of the 16th International Workshop of the Web and Databases* (WebDB), 2013.

Toward 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.

The Gene Wiki in 2011: community intelligence applied to human gene annotation.
Nucleic Acids Research, Vol. 40, D1255-D1261, 2012.

Reputation Systems for Open Collaboration.
Communications of the ACM, Volume 54, Issue 8, August, 2011.

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.

Qualitative Concurrent Parity Games.
ACM Transactions on Computational Logic, 12, 4, Article 28, 51 pages, July, 2011.
This is a journal version of a LICS 2000 paper; the LICS paper won the LICS 2020 Test-Of-Time Award.

Detecting Wikipedia Vandalism Using WikiTrust.
PAN lab report, CLEF (Conference on Multilingual and Multimodal Information Access Evaluation), 2010.

Solving Games via Three-Valued Abstraction Refinement.
Information and Computation, volume 208, issue 6, pages 666-676, June, 2010.
This is the journal version of a CONCUR 2007 paper.

Algorithms for Game Metrics.
Logical Methods in Computer Science, Volume 6 (3:13), pages 1-27, 2010.
This is the journal version of our FSTTCS 08 paper.

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.

Termination Criteria for Solving Concurrent Safety and Reachability Games.
In *Proceedings of SODA 09: ACM-SIAM Symposium on Discrete Algorithms*, ACM Press, 2009.

Qualitative Logics and Equivalences for Probabilistic Systems.
Logical Methods in Computer Science, volume 5, issue 2, 2009.

Linear and Branching System Metrics.
IEEE Transactions on Software Engineering, pages 258-273, volume 35, number 2, March, 2009.
This is the journal version of our ICALP 2004 paper.

Game Refinement Relations and Metrics.
Logical Methods in Computer Science, volume 4, issue 3, 2008.

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.

Algorithms for Game Metrics.
In *Proceedings of FSTTCS 08: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science*, 2008.
An extended version of this paper was published on arXiv; the Journal version appeared in Logical Methods in Computer Science, Volume 6 (3:13), pages 1-27, 2010.

Algorithms for Game Metrics.
arXiv:0809.4326, 2008.
(arXiv:0809.4326). The Journal version appeared in Logical Methods in Computer Science, Volume 6 (3:13), pages 1-27, 2010

Robust Content-Driven Reputation.
In *Proceedings of AISec 08: First ACM Workshop of AISec*, ACM Press, 2008.
A version of this work appeared in the Technical Report UCSC-SOE-08-09, School of Engineering, University of California, Santa Cruz, CA, USA, 2008.

Measuring Author Contributions to the Wikipedia.
In *WikiSym 2008: International Symposium on Wikis*, 2008.
A version of this work was published as the Technical Report UCSC-SOE-08-08, School of Engineering, University of California, Santa Cruz, CA, USA, May 2008.

Symbolic Magnifying Lens Abstraction in Markov Decision Processes.
In *QEST 2008: Proceedings of the International Conference on Evaluation of Systems*, 2008.
A preliminary version of this work appeared as Technical Report UCSC-SOE-08-05, School of Engineering, University of California, Santa Cruz, CA, USA, May 2008.

Robust Content-Driven Reputation.
Technical Report UCSC-SOE-08-09, School of Engineering, University of California, Santa Cruz, CA, USA. May, 2008.
A version of this work was published in the Proceedings of AISec 2008.

Measuring Author Contributions to the Wikipedia.
Technical Report UCSC-SOE-08-08, School of Engineering, University of California, Santa Cruz, CA, USA, May, 2008.
A version of this work appeared in WikiSym 2008.

Assigning Trust to Wikipedia Content.
Technical Report UCSC-SOE-08-07, School of Engineering, University of California, Santa Cruz, CA, USA, May, 2008.
This is a revised version of the Technical Report UCSC-CRL-07-09, School of Engineering, University of California, Santa Cruz, CA, USA, 2007.

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.
This work was published later in the proceedings of QEST 2008.

Strategy Improvement for Concurrent Safety Games.
Technical Report UCSC-SOE-08-04, School of Engineering, University of California, Santa Cruz, CA, USA, April, 2008.

The Complexity of Coverage.
Technical Report UCSC-SOE-08-03, School of Engineering, University of California, Santa Cruz, CA, USA, April, 2008.

Qualitative Concurrent Parity Games.
Technical Report UCSC-CRL-08-02, School of Engineering, University of California, Santa Cruz, CA, USA, April, 2008.
The definitive version of this work was published in the ACM Transactions on Computational Logic, 2011.

Assigning Trust To Wikipedia Content.
Technical Report UCSC-CRL-07-09, School of Engineering, University of California, Santa Cruz, CA, USA. November, 2007.

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.
A journal version of this work appeared in Information and Computation, volume 208, issue 6, pages 666-676, June 2010.

Game Relations and Metrics.
In *LICS 2007: Proceedings of the 22nd IEEE Symposium on Logic in Computer Science*, 2007.

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.
A version of this work previously appeared as the Technical report ucsc-crl-06-18, School of Engineering, University of California, Santa Cruz, November 2006.

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.

A Content-Driven Reputation System for the Wikipedia.
In WWW 2007, Proceedings of the 16th International World Wide Web Conference, ACM Press, 2007.

A Content-Driven Reputation System for the Wikipedia.
Technical report ucsc-crl-06-18, School of Engineering, University of California, Santa Cruz, November, 2006.
Errata corrige. A revised version of this paper was accepted at the World Wide Web 2007 conference.

Magnifying-Lens Abstraction for Markov Decision Processes.
Technical report ucsc-crl-06-15, School of Engineering, University of California, Santa Cruz, 2006.
A version of this work appeared in CAV 2007.

An Introduction to the Tool Ticc.
Technical report ucsc-crl-06-14, School of Engineering, University of California, Santa Cruz, 2006.
This work was presented at the Workshop on Trustworthy Software, which took place in Saarbrücken, Germany, 2006

Strategy Improvement for Concurrent Reachability Games.
In *QEST 06: International Conference on Quantitative Evaluation of Systems*, pages 291-300, IEEE Computer Society Press, 2006.

Compositonal Quantitative Reasoning.
In *QEST 06: International Conference on Quantitative Evaluation of Systems*, pages 157-166, IEEE Computer Society Press, 2006.

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.
An extended version of this work has been published as the Technical Report ucsc-crl-06-01, School of Engineering, University of California, Santa Cruz, 2006

Ticc: A Tool for Interface Compatibility and Composition.
Technical Report ucsc-crl-06-01, School of Engineering, University of California, Santa Cruz, 2006.

The Complexity of Quantitative Concurrent Parity Games.
In *SODA 06: ACM-SIAM Symposium on Discrete Algorithms*, pages 678-687, ACM Press, 2006.

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.

Code Aware Resource Management.
In *EMSOFT 05: Fifth ACM International Conference on Embedded Software*, pages 191-202, ACM Press, 2005.

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.

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, 2005.

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.

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 version of an ICALP 2004 paper. The journal version appeared in the IEEE Transactions on Software Engineering, pages 258-273, volume 35, number 2, March 2009.

Model Checking Discounted Temporal Properties.
Theoretical Computer Science, Elsevier, 2005.
This is a journal verson of a TACAS 2004 paper.

Trading Memory for Randomness.
In *QEST 04: 1st International Conference on the Quantitative Evaluation of Systems*, pages 206-217, IEEE Computer Society Press, 2004.

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.
A journal version of this work appeared in IEEE Transactions on Software Engineering, pages 258-273, volume 35, number 2, March 2009.

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.

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.

Quantitative Solution of Omega-Regular Games.
Journal of Computer and System Sciences 68, pages 374-397, 2004, 2004.
This is a journal version of our STOC 2001 paper.

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*, Electronic Notes on Theoretical Computer Science, Elsevier Science Publishers, 2003.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.
**This paper received the ESWEEK 2020 Test-of-Time Award,** the second such award given in the Embedded System Week (ESWEEK) history.

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.
**This paper received the 2011 ACM SIGSOFT Impact Paper Award.**

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.

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.
**This paper won the CONCUR 01 Best Paper Award.**

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.

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.

Quantitative Solution of Omega-Regular Games.
In *STOC 01: 33rd Annual ACM Symposium on Theory of Computing*, 2001.
This may be the paper that I had the most fun writing ever. An extended version appeared in Journal of Computer and System Sciences 68, pages 374-397, 2004.

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.

MCWEB: A Model-Checking Tool for Web Site Debugging.
Poster presented at the *10th World Wide Web Conference*, Hong Kong, 2001.

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.

Process Algebra and Probabilistic Methods.
Proceedings. Lecture Notes in Computer Science 2165, Springer-Verlag, 2001.
Front matter.

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.

Detecting Errors Before Reaching Them.
In *CAV 00: Proceedings of the 12th International Conference on Computer Aided Verification*, Lecture Notes in Computer Science 1855, 2000.

Concurrent Omega-Regular Games.
In *LICS 2000: 15th International IEEE Symposium on Logic in Computer Science*, pages 141-154, IEEE press, 2000.
**This paper received the LICS 2020 Test-Of-Time Award.** The journal version was published in the ACM Transactions on Computational Logic, 12, 4, Article 28, 51 pages, July 2011.

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.

From Fairness to Chance.
In *ENTCS: Electronic Notes on Theoretical Computer Science* 22, Elsevier Science Publishers, 2000.

Mocha: Exploiting Modularity in Model Checking.
University of California, Berkeley, Department of Electrical Engineering and Computer Science, 2000.

The verification of probabilistic systems under memoryless partial-information policies is hard.
In *Proceedings of the Workshop on Probabilistic Methods in Verification*, published as Technical Report CSR-99-9, pages 19-32, University of Birmingham, 1999.

Automating Modular Verification.
In *CONCUR 99: Concurrency Theory, 10th International Conference*, Lecture Notes in Computer Science 1664, pages 82-97, Springer Verlag, 1999.

Computing Minimum and Maximum Reachability Times in Probabilistic Systems.
In *CONCUR 99: Concurrency Theory, 10th International Conference*, Lecture Notes in Computer Science 1664, pages 82-97, Springer Verlag, 1999.

Concurrent Reachability Games.
In *FOCS 98: 39th Annual IEEE Symposium on Foundations of Computer Science*, pages 564-575, IEEE Press, 1998.

Concurrent Reachability Games.
Technical report UCB/ERL M98/33, University of California at Berkeley, 1998.

Stochastic Transition Systems.
In *CONCUR 98: 9th International Conference on Concurrency Theory*, Lecture Notes in Computer Science 1466, pages 423-438, Springer-Verlag, 1998.

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.

Decomposing, Transforming and Composing Diagrams: The Joys of Modular Verification.
Technical report STAN-CS-98-1614, Stanford University, 1998.

Formal Verification of Probabilistic Systems.
Ph.D. Dissertation, Stanford University, 1997. Technical report STAN-CS-TR-98-1601, 1997.
Errata Corrige. **This thesis won the 1998 Samuel Thesis Award from the Computer Science Department, and it was nominated for the ACM Doctoral Dissertation Award.**

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.

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.

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.
Errata Corrige.

Diagram-based Formalisms for the Verification of Reactive Systems.
In *CADE-13: Workshop on Visual Reasoning*, 1996.

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.

Formal Verification of Performance and Reliability of Real-Time Systems.
Stanford University Technical Report STAN-CS-TR-96-1571, 1996.

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.

STeP: The Stanford Temporal Prover.
In *Colloquium on Trees in Algebra and Programming*, pp. 793-794. Springer, Berlin, Heidelberg, 1995.

Codes for Second and Third Order GH-ARQ Schemes.
*IEEE Transactions on Communication 42(2-4)* pages 899-910, 1994.

Determination of Automorphic Codes.
In *Proceedings of the International Conference on Digital Signal Processing**, pages 840-844. North Holland Press**, 1987.
*