Mohamed Gouda (Texas)

Using Formal Methods in Network Research? What a Beautiful Idea!

Abstract: There are two types of benefits that result from using formal methods in network research: short-term and long-term. The short-term benefits are rather obvious. After all formal methods have been widely used for several decades in specifying, designing, verifying, implementing, and debugging network protocols. However, the long-term benefits of using formal methods in network research are decidedly subtle. Rather than merely establish the correctness of a single protocol, formal methods can be employed to deepen our understanding of large classes of protocols. We attempt to make this point clear by discussing some results that we obtained recently from our work in developing a new logic for designing and verifying network firewalls.


Bio: Mohamed G. Gouda received his first B.Sc. in Aeronautical Engineering and his second in Mathematics; both from Cairo University, Egypt. He then obtained an M.A. in Mathematics from York University and a Master and Ph.D. in Computer Science from the University of Waterloo, Canada. Later he worked for the Honeywell Corporate Technology Center in Minneapolis 1977-1980. In 1980, he joined the University of Texas at Austin where he currently holds the Mike A. Myers Centennial Professorship in Computer Sciences. He spent one summer at Bell labs in Murray Hill, one summer at MCC, Inc. in Austin, and one winter at the Eindhoven Technical University in the Netherlands. Since 2009, he serves as Program Director of the Computer Systems Research Program in the National Science Foundation.

His research areas are distributed and concurrent computing and network protocols. In these areas, he has been working on abstraction, formality, correctness, non-determinism, atomicity, reliability, security, convergence, and stabilization. He has published three books, over twenty book chapters, over one hundred journal papers, and over one hundred and fifty conference papers.

He supervised twenty three Ph.D. Dissertations. Five of his former Ph.D. students are now Full Professors at the University of Colorado at Colorado Springs, the University of California at Santa Barbara, the University of North Carolina at Chapel Hill, Ohio-State University, and the University of Iowa. Another four of his former students are now Associate Professors, and two of his former students are still Assistant Professors in the U. S.

Jayadev Misra (Texas)

Structured Orchestration of Data and Computation

Abstract: This talk will describe our attempt at integrating data and services within a large organization, or using the internet. We have developed a theory, called Orc, in which we specify the sources of data and computations and how to orchestrate their executions (concurrently, one after the other, only when the majority of data is available, ...). The Orc programming language has a very small kernel, using external libraries of sites for support functions. The language starts with concurrency as the defining characteristic of programs. With its hierarchical and recursive combination facilities, it provides a model of structured concurrency. It can be used to orchestrate a small application or a giant one with many millions of threads, running in real time, from milliseconds to months. We have developed an experimental implementation of the language. The language, its documentation, and a web-interface are available at orc.cres.utexas.edu where programs can also be submitted for execution.

Bio: Jayadev Misra is a professor and holder of the Schlumberger Centennial chair in Computer Science at the University of Texas at Austin. He is known for his work in the area of concurrent programming, with emphasis on rigorous methods to improve the programming process. His work on the UNITY methodology, jointly with Chandy, has been influential in both academia and industry, and has spawned a large number of tools and research projects. He has recently developed a programming language, called "Orc", for concurrent orchestrations of interacting components. He is also spear-heading an effort, jointly with Tony Hoare, to automate large-scale program verification.

Misra is a fellow of ACM and IEEE; he held the Guggenheim fellowship during 1988-1989. He was the Strachey lecturer at Oxford University in 1996, and has held the Belgian FNRS International Chair of Computer Science in 1990. He is a member of the Academy of Distinguished Teachers at the University of Texas at Austin.

Misra has been the past editor of several journals including: Computing Surveys, Journal of the ACM, Information Processing Letters and the Formal Aspects of Computing. He is the author of two books, "Parallel Program Design: A Foundation", Addison-Wesley, 1988, co-authored with Mani Chandy, and "A Discipline of Multiprogramming", Springer-Verlag, 2001.