ASE 2006 Keynote Speakers
Verifying Specifications with Proof Scores in CafeOBJ
Wednesday, Sep 20, 9:00-10:30
Room: Hitotsubashi Memorial Hall
Kokichi Futatsugi, Graduate School of Information Science, JAIST (Japan Advanced Institute of Science and Technology), Nomi, Ishikawa, Japan
Verifying specifications is still one of the most important undeveloped topics in software engineering. It is important because quite a few critical bugs are caused at the level of domains, requirements, and/or designs. It is also important for the cases where no program codes are generated and specifications are analyzed and verified only for justifying models of problems in real world. In this talk, a survey of our research activities in verifying specifications is given. After explaining fundamental issues and importance of verifying specifications, the proof score approach in CafeOBJ and its applications to several areas are described.
 Kokichi Futatsugi is a professor of Graduate School of Information Science, JAIST (Japan Advanced Institute of Science and Technology), Ishikawa, Japan. His research interest includes formal methods, software requirements and specifications, modeling and specification languages. An important part of his research activities is done around the CafeOBJ formal specification language (www.ldl.jaist.ac.jp/cafeobj). CafeOBJ is an executable formal specification language which has been designed and developed by an international team headed by Prof. Futatsugi. He was a co-chair of the program committee of 20th ICSE (1998) and an associate editor of ACM TOSEM for 1995-2002. He is a member of the advisory board of Journal of Higher-Order and Symbolic Computation (www.wkap.nl/journals/hosc), and the editorial board of Journal of Object Technology (www.jot.fm) and Journal of Applied Logic (www.elsevier.com/locate/jal). |
Winning the DARPA Grand Challenge
Thursday, Sep 21, 9:00-10:30
Room: Hitotsubashi Memorial Hall
Sebastian Thrun,
Computer Science Department, Stanford University
The DARPA Grand Challenge has been the most significant event for the robotics community in more than a decade. This challenge required a mobile ground robot to traverse 132 miles of unrehearsed desert terrain in less than 10 hours, and without human intervention. In 2004, the best robot only made 7.3 miles. In 2005, Stanford won the challenge and the $2M prize in less than 7 hours travel time. This talk, delivered by the leader of the Stanford Racing Team, will provide insights into the software architecture of Stanford's winning robot. The robot massively relied on machine learning and probabilistic modeling for sensor interpretation and control. The speaker will explain some of the basic algorithms that made this victory possible, and share some of the excitement characterizing this historic event.
Sebastian Thrun is widely considered a leading expert on robotics and artificial intelligence. Thrun is Associate Professor of Computer Science and Director of the Stanford Artificial Intelligence Laboratory (SAIL). Prior to winning the Grand Challenge, Thrun published seven books, 300 refereed papers, won numerous best paper awards, and served as PI on 6 major DARPA initiatives. His most recent book "Probabilistic Robotics" summarizes research on a new programming methodology for robots that has become mainstream in the field of robotics, with hundreds of papers published every year.
|
Automatic property checking for software: past, present and future
Friday, Sep 22, 14:00-15:30
Room: Hitotsubashi Memorial Hall
Sriram K. Rajamani, Microsoft Research India
Over the past few years, we have seen several automatic static analysis tools being developed and deployed in industrial-strength software development. I will survey several of these tools ranging from heuristic and scalable analysis tools (such as PREFix, PREFast and Metal), to sound analysis tools based on counter example driven refinement (such as SLAM). Then, I will present two exciting recent developments in counterexample driven refinement:(1) generalizing counterexample driven refinement to work with any abstract interpretation, and (2) combining directed testing with counterexample driven refinement.
 Sriram Rajamani is a Senior Researcher and Research Manager with Microsoft Research India, Bangalore. Prior to moving to the India lab, Sriram was most recently manager of the Software Productivity Tools group in Microsoft Research Redmond, where he led several projects together with is wonderful colleagues ---SLAM and Static Driver Verifier, Behave! and Zing. Sriram has a PhD in Computer Science from the University of California at Berkeley. In a previous life Sriram has worked as a programmer for over 5 years writing telecommunication software (for Syntek Inc) and electronic design automation software (for Xilinx Inc). He uses his first hand experience in the realities of commercial software development to guide his choice of problems and approaches to research in software productivity. |
|
|
|
|
|
| |
|
|
|
