Professor of Electrical Engineering and Computer Sciences
and Director, Electronics Research Laboratory
Field of Specialization
Robotics, Complex systems and hybrid control, Simulation and Visualization
Experience
Professor, University of California, Berkeley, 1988 - present,
Gordon Mc Kay Professor of Electrical Engineering and Computer
Sciences, Harvard University, 1994, Visiting Vinton Hayes Professor of
Electrical Engineering, MIT, Fall 1992,
Directeur Recherche, Center Nationale Recherche Scientifique (CNRS),
Toulouse, France, Summer 1991,
Professore A Contratto, Universita di Roma. Summer
1990, 1991,
Associate Professor, University of California, Berkeley, 1984 -
1988,
Visiting Fellow, Australian National University, Canberra,
Summer 1985,
Assistant Professor, University of California, Berkeley, 1983 - 1984,
Assistant Professor, MIT,
Cambridge, 1980 - 1982.
Awards
President of India Medal, 1977,
IBM Faculty Development Grant, 1983,
NSF Presidential Young Investigator Award, 1985,
IEEE Student Best Paper Award, 1977,
Eckmann Award of the American Control Council, 1990.
M. A. Arts and Sciences, (honorary, 1994), Harvard University,
Cambridge, Fellow IEEE (1995).
Books Published
1. S.S. Sastry and M. Bodson, Adaptive Control: Stability,
Convergence and Robustness, Prentice Hall, 1989.
2. R. Murray, Z. Li and S. Sastry A Mathematical Introduction to
Robotic Manipulation, CRC Press, 1994.
3. P. Antsaklis, W. Kohn, A. Nerode and S. Sastry (editors), Hybrid
Systems II, Springer Verlag, Lecture Notes in Computer Science,
Vol. 999, 1995.
4. P. Antsaklis, W. Kohn, A. Nerode and S. Sastry (editors), Hybrid
Systems IV, Springer Verlag, Lecture Notes in Computer Science,
Vol. 1293, 1997.
Publications
Here are a selection of some papers relevant to the
proposal from over 200 papers:
1. Lygeros, J.; Godbole, D.N.; Sastry, S.
"Hybrid controller design for multi-agent systems,"
IN: Control Using Logic-Based Switching. Block Island, RI, USA, Fall
1995. Edited by: Morse, A.S. London, UK: Springer-Verlag,
1997. p. 59-78.
2. Pappas, G.J.; Sastry, S.
" Towards continuous abstractions of dynamical and control systems",
IN: Hybrid Systems IV, Ithaca, NY, USA, 12-14 Oct. 1996,
Edited by:
Antsaklis, P.; Kohn, W.; Nerode, A.; Sastry, S. Berlin, Germany:
Springer-Verlag, 1997. p. 329-41.
3. Tomlin, C.; Pappas, G.; Lygeros, J.; Godbole, D., and S. Sastry,
"Hybrid control models of next generation air traffic management",
IN: Hybrid Systems IV, Ithaca, NY, USA, 12-14 Oct. 1996). Edited by:
Antsaklis, P.; Kohn, W.; Nerode, A.; Sastry, S. Berlin, Germany:
Springer-Verlag, 1997. p. 378-404.
4. Lygeros, J.; Tomlin, C.; Sastry, S.
"Multiobjective hybrid controller synthesis",
IN: Hybrid and Real- Time Systems. International Workshop, HART'97.
Proceedings, Grenoble, France, 26-28 March 1997). Edited by: Maler,
O. Berlin, Germany: Springer-Verlag, 1997. p. 109-23.
5. Lygeros, J.; Godbole, D.N.; Sastry, S.
"A game-theoretic approach to hybrid system design",
IN: Hybrid Systems III. Verification and Control, New
Brunswick, NJ, USA, 22-25 Oct. 1995). Edited by: Alur, R.; Henzinger, T.A.;
Sontag, E.D. Berlin, Germany: Springer-Verlag, 1996. p. 1-12.
6. J. Lygeros, D. Godbole and S. Sastry, ``Verified hybrid
controllers for automated vehicles'', to appear in the
IEEE Transactions on Automatic Control, April 1998.
7. C. Tomlin, G. Pappas and S. Sastry, ``Conflict Resolution in
Multi-Agent systems: A case study in air traffic control,'' to appear
in IEEE Transactions in Automatic Control, April 1998.
Sastry's current major support obligations are:
NSF Grant No. IRI-9531837
(PI), ``Millirobotics for Tissue Manipulation in Minimally Invasive''
Telesurgery,'' $422,355 from 6/1/96 to 5/31/99.
ARO MURI Initiative,
Grant No. DAA-96-1-0341 (PI),
``An Integrated Approach to Intelligent Systems,''
$ 3,000,000 from 9/1/96 to 8/31/99 with 2 option years.
ONR Grant No. N00014-97-1-096
(PI)
``Intelligent Control Architectures for Unmanned Air Vehicles,''
$ 622,507 from
7/1/97 to 6/31/00
On this project Sastry will devote about 25 % of his academic
year research effort (not billed to grant: academic
year salary paid by state) and 1 summer month. He will be supervising
3 students and 1.5 post doctoral scholars on the grant.
Thomas Henzinger is an Associate Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received the MS degree in Computer Science from the University of Delaware in 1986, the Dipl.-Ing. in Computer Science from Kepler University in Linz, Austria, in 1987, and the PhD degree in Computer Science from Stanford University in 1991. He spent a postdoctoral semester in Grenoble, France. From 1992 to 1995, he was an Assistant Professor of Computer Science at Cornell University. In 1996, he joined the faculty of the University of California at Berkeley.
Professor Henzinger's research interests center around formal methods for the design and analysis of software and hardware systems. He has published more than 50 articles on formal verification in refereed journals and conference proceedings, served on numerous scientific program committees, and been invited as plenary speaker at international meetings including the 1996 IEEE Symposium on Logic in Computer Science (LICS), the 1998 International Colloquium on Automata, Languages, and Computation (ICALP), the 1998 Conference on Concurrency Theory (CONCUR), the 1998 IFIP World Computer Congress, and the 1999 International Congress of Logic, Methodology, and Philosophy of Science. Henzinger organized and chaired, together with Rajeev Alur, the 1995 Workshop on Hybrid Systems, and the 1996 Conference on Computer-Aided Verification (CAV). CAV is the premier forum for the presentation of research in computer-aided verification techniques, tools, and applications. Henzinger will organize and chair, together with Shankar Sastry, the 1998 Workshop on Hybrid Systems. He serves on the editorial board of the journals Formal Methods in System Design (Kluwer) and Software Tools for Technology Transfer (Springer).
Professor Henzinger pioneered formal methods for the design and analysis of
real-time and hybrid systems.
A hybrid system is a digital computer system that controls an analog object,
such as an airplane.
The model checker HYTECH developed by Professor Henzinger's research
team is the first tool for the automatic analysis of hybrid systems.
It is currently installed at over 100 academic and research institutions
wordwide.
More details on Professor Henzinger's research, including pointers to all
projects and publications, can be found on his home page at
www.eecs.berkeley.edu/~tah.
Henzinger's current grant obligations are:
Office of Naval Research Young Investigator Award N00014-95-1-0520
(Thomas A. Henzinger, PI),
``Algorithms and Tools for the Automatic Analysis of Embedded Systems,''
6/1/1995-5/31/1998,
$ 235,407.
Expires in 1998.
National Science Foundation CAREER Award CCR-9501708
(Thomas A. Henzinger, PI),
``Computer-Aided Verification'',
8/1/1995-7/31/1998,
$ 133,332.
Expires in 1998.
National Science Foundation Grant CCR-9504469
(Thomas A. Henzinger, PI),
``Algorithms and Tools for the Automatic Analysis of Embedded Systems'',
9/1/1996-8/31/1998,
$ 135,000.
Expires in 1998.
Semiconductor Research Corporation Contract 98-DC-324.036
(Robert Brayton, PI),
``Center of Excellence in Design Automation,''
1/1/1998-12/31/1998,
$ 136,789.
Professor Henzinger is co-investigator on the task
``Compositional/hierarchical Formal Verification.''
Includes 1 month of summer support, and during the academic year,
5% of Professor Henzinger's research effort.
His pending obligations are to
Defense Advanced Research Projects Agency (Thomas A. Henzinger, PI;
subcontract to Univ. of Pennsylvania), "Mocha: Modularity in Model
Checking," in the amount of 850,000 (Berkeley's share is 457,152) for two
years beginning in 1998 (date to be determined).
Henzinger will be able to devote about 30 % of
his academic year research effort (not billed to grant) and
1 month (summer) to this project. He will supervise 3 students and 1.5
post doctoral scholars on this project.
Edward A. Lee is a Professor in the Electrical Engineering and Computer Science Department at U.C. Berkeley. His research interests include real-time systems, signal processing, discrete-event systems, concurrency, and system-level design technology. He is director of the Ptolemy project at UC Berkeley. He is co-author of four books, numerous papers, and two patents. His bachelors degree (B.S.) is from Yale University (1979), his masters (S.M.) from MIT (1981), and his Ph.D. from U. C. Berkeley (1986). From 1979 to 1982 he was a member of technical staff at Bell Telephone Laboratories in Holmdel, New Jersey, in the Advanced Data Communications Laboratory. He is a founder of BDTI, Inc., and has consulted for a number of other companies. He is a fellow of the IEEE, was an NSF Presidential Young Investigator, and won the 1997 Frederick Emmons Terman Award for Engineering Education.
Some of the more relevant papers:
[1] A. Girault, B. Lee, and E. A. Lee, ``A Preliminary Study of Hierarchical
Finite State Machines with Multiple Concurrency Models,'' Memorandum
UCB/ERL M97/57, Electronics Research Laboratory, University of
California, Berkeley, CA 94720, August 1997.
http://ptolemy.eecs.berkeley.edu/papers/97/preliminaryStarcharts/
[2] S. Edwards, L. Lavagno, E. A. Lee, and A. Sangiovanni-Vincentelli,
``Design of Embedded Systems: Formal Models, Validation, and Synthesis,''
Proceedings of the IEEE, Vol. 85, No. 3, March 1997.
http://ptolemy.eecs.berkeley.edu/papers/97/codesign/
[3] C. Hylands, E. A. Lee, and H. J. Reekie, ``The Tycho User Interface
System,'' 5th Annual Tcl/Tk Workshop '97, Boston, Massachusetts, July,
1997.
http://ptolemy.eecs.berkeley.edu/papers/97/tcltk-97/
[4] S. S. Bhattacharyya, P. K. Murthy and E. A. Lee, ``Software Synthesis from Dataflow Graphs'', Kluwer Academic Publishers, Norwell, Mass, 1996.
[5] E. A. Lee and A. Sangiovanni-Vincentelli, ``A Denotational Framework for
Comparing Models of Computation,'' ERL Memorandum UCB/ERL M97/11,
University of California, Berkeley, CA 94720, January 30, 1997.
http://ptolemy.eecs.berkeley.edu/papers/97/denotational/
[6] W.-T. Chang, A. Kalavade, and E. A. Lee, ``Effective Heterogeneous Design
and Cosimulation,'', chapter in Hardware/Software Co-design, G. DeMicheli
and M. Sami, eds., NATO ASI Series Vol. 310, Kluwer Academic
Publishers,1996. Also presented at NATO Advanced Study Institute
Workshop on Hardware/Software Codesign, Lake Como, Italy, June 18 - 30,
1995.
http://ptolemy.eecs.berkeley.edu/papers/effective/
[7] E. A. Lee and T. M. Parks, ``Dataflow Process Networks,'', Proceedings
of the IEEE, vol. 83, no. 5, pp. 773-801, May, 1995.
http://ptolemy.eecs.berkeley.edu/papers/processNets/
Lee's current grant obligations are:
PI DARPA grant ``Design of Sitributed Adaptive Signal Processing
Systems, $2.407M 11/18/96 - 11/30/99. He devotes 25 % of his
academic year research effort and 1 month summer to this project.
c-PI SRC grant ``Computer Aided Design of Heterogeneous
Hardware/Software Systems'', $ 80K, 1/1/98 - 12/31/98. He devotes
5 % academic research time to this project and 1 summer month.
Lee will devote about 20 % of his academic year research time (not billed to the grant) and 1 month summer working on this project. He will supervise 2 graduate students and 1 post doctoral scholar on the grant.
Alex Aiken is an Associate Professor of Electrical Engineering and Computer Science of the University of California at Berkeley. He received his Bachelors degree in Computer Science and Music from Bowling Green State University in 1983 and his Ph.D. from Cornell University in 1988. Before joining the Berkeley faculty in 1993, he spent five years as a Research Staff Member at the IBM Almaden Research Center. Professor Aiken's interests include the design and analysis of programming languages and software systems, with particular emphasis on techniques for automatic program analysis.
Professor Aiken is an NSF National Young Investigator, and is the Program Chair for the 1999 ACM Symposium on Principles of Programming Languages (POPL). He has also published widely in computer science conferences and journals. Professor Aiken has developed or co-developed several software systems used at hundreds of institutions, including a popular project and set of lecture notes for undergraduate compiler courses. While at IBM, he and Ed Wimmers wrote a series of seminal papers on the theory of set constraints. This work is generally recognized as a breakthrough in the understanding of algorithms for inclusion constraints and subtyping problems. Since joining the Berkeley faculty in 1993, Professor Aiken has continued working in constraint-based program analysis with the development of BANE, the Berkeley ANalysis Engine. The focus of BANE has been on program analyses to support software engineering and compilation applications.
Aiken's current grant obligations are:
Co-PI on the NSF Titanium project.
The Titanium project ($2,030,736, 3 years, 2.25 academic
year months, 2 summer months of salary) completes 5/31/98.
Aiken is currently the
PI on two NSF grants, a National Young Investigator award (NSF, $237,500,
9/15/94-8/31/99, .2 summer months)
and a smaller regular NSF grant ($134,750, 3 years, .6 summer
months)
The regular NSF grant will expire 8/31/98.
Aiken's pending grant obligations are
PI on a DARPA grant ``A Scalable Analysis Toolkit''
$ 450,000, 2 years, start date undetermined at this time.
Aiken will be able to devote 20 % of his academic year research
effort (not billed) and 1 month summer to this project. He will
supervise 2 students on the grant.