Skip to main content

TITLE: Finding Liveness Bugs in Systems Code

Note that you are all welcome to attend all colloquium talks.  You can subscribe to the talks list here: https://mailman.cs.washington.edu/mailman/listinfo/talks

NOTE:  Corrections – this talk will *not* be taped or broadcast live!  Location has also been changed!

UNIVERSITY OF WASHINGTON
Computer Science and Engineering
Research Seminar

SPEAKER:    Ranjit Jhala, UCSD

TITLE:        Finding Liveness Bugs in Systems Code

DATE:        Tuesday, February 9, 2010
TIME:        3:30pm
PLACE:        403 Paul G. Allen Center for CSE
HOST:        Michael Ernst

ABSTRACT:
In this talk, we describe a technique for finding bugs in complex concurrent and distributed systems implementations. To do so, the developer formally specifies high-level liveness properties which define desirable end-to-end system conditions, which need not always hold, perhaps as a result of failure or during system initialization, but which must eventually be satisfied.

Unfortunately, previous techniques cannot find liveness bugs because doing so requires finding an infinite execution that does not satisfy a liveness property.

We present probabilistic heuristics to find a large class of liveness violations and the critical transition of the violating execution.  The critical transition is the step in an execution that moves the system from a state that can satisfy the liveness property in the future, to a dead state that can never achieve the liveness property, regardless of any subsequent sequence of actions.

Our approach is implemented in a software model checker, MaceMC. MaceMC isolated, without any false warnings, complex liveness errors in implementations of Pastry, Chord, a reliable transport protocol, an aggregation service, Overcast, and an overlay tree implementing a failure-resilient random tree, allowing us to understand and fix problems that had eluded detection for several years.

(Joint work with Chip Killian, James Anderson and Amin Vahdat)

BIO:
Ranjit Jhala is an Assistant Professor in the Department of Computer Science and Engineering at UC San Diego. Before joining UCSD, he was a graduate student at UC Berkeley. Ranjit is is interested in applying techniques from Programming Languages and Software Engineering to solve computing problems, in particular, to build reliable computer systems. His work draws from, combines and contributes to methods the areas of Model Checking, Program Analysis, Type Systems and Automated Deduction.

Email: talk-info@cs.washington.edu
Info: http://www.cs.washington.edu/
(206) 543-1695

The University of Washington is committed to providing access, equal opportunity and reasonable accomodation in its services, programs, activities, education and employment for individuals with disabilities. To request disability accommodation, contact the Disability Services Office at least ten days in advance of the event at: (206) 543-6450/V, (206) 543-6452/TTY, (206) 685-3885/FAX, or access@u.washington.edu.
_______________________________________________

February 8, 2010

FW: UW EIC Thinking Through “Market Opportunity” Feb 10, 2010, 5:30 to 7 pm in Sieg Hall 225

UW Environmental Innovation Challenge

Thinking Through “Market Opportunity” February 10, 2010, 5:30 to 7 pm in Sieg Hall 225

Still looking for a team/team members?  This is a good opportunity to meet-up.

One of the key elements of the UW Environmental Innovation Challenge is the market opportunity summary. If you build this prototype or create this computer simulation, will anyone buy it?  Is it appropriate for the audience you’ve identified? Who has a similar product or service? Who’s your competition? What are the resources on campus that you can tap into to do market research? How much research is enough? What is “addressable market size”?

To help you answer these questions, we’re bringing in John Browne, the founder and managing director of Workpump. John spent more than 25 years in the software industry (including 11 at Microsoft) and, by his own admission, can’t remember all the products he’s shipped or the projects he’s worked on. He understands every aspect of designing, developing, testing, and marketing world-class software.

In 2001 John started Workpump to bring Microsoft-quality best practices in marketing and product development to technology firms, working with clients from Silicon Valley to British Columbia. Starting in 2003 John began assembling a team of like-minded individuals who could bring years of successful operational experience to clients. He knows this stuff.

Join us on February 10—and come with your questions!

Connie Bourassa-Shaw, Director

Center for Innovation and Entrepreneurship

cbshaw@uw.edu

Pamela Tufts

Center for Innovation & Entrepreneurship
ptufts@uw.edu 206.685.3813

foster.washington.edu/cie

February 8, 2010

Winterfest: 2/19, Save the Date!

Winterfest is coming on the evening of February 19th!

Join us for dancing, video games, and of course free food and drink.  The DJ’s will be two of your favorite Rainy Dawg Radio stars: Kelly and Sam!

– Your Favorite ACM Officers

February 8, 2010

Clustrix Talk: Wednesday, 2/10, 5:30-7 in the Atrium

Graduating? Looking for a job?

Come to this one time event and hear UW alum Paul Mikesell speak about a future with Clustrix.

Free dinner! will be served!

Who?

Clustrix is developing a next generation clustered, scalable, fault-tolerant, relational database solution. Founded by a UW CSE alum and Isilon co-founder, Paul Mikesell.

What?

Clustrix, Inc. is looking for Software Engineers who enjoy design as well as development. We have a focused engineering team with little management overhead.

Where?

Atrium in Computer Science & Engineering Building

When?

Wednesday, Feb. 10, 2010

5:30-7:00 pm

For more information, please visit our website www.clustrix.com

February 8, 2010

CSE Study Abroad Application

Hi all,

Just a reminder that the CSE Study Abroad application for the KTH, ETH, and the new Saarland University exchanges is now online at: http://www.cs.washington.edu/education/exchanges.html.

Applications are due this Friday, February 12th at 5pm. Let me know if you have any questions.

If you’d like to study abroad at a different location or for a shorter period of time, you should check out the IP&E’s webpage of UW exchanges or look for a shorter summer Exploration Seminar (They’re fun! I’ve been to one in Israel and had a great experience).

February 8, 2010

Reminder: Google Tech Talk Tonight!

Come hear more about the different roles at Google, and how employees have applied their education and experiences to work on interesting challenges today at 5:30 PM in EE 105.

Please sign up for this event by RSVP’ing here<https://spreadsheets.google.com/viewform?formkey=dG0yOUZCbWUwZ1ltbERxNXNaX2pxeUE6MA>. RSVPing helps us know how many people to order food for, but everyone is welcome!

February 3, 2010

Google Tech Talk: Wednesday, 2/3

Come join Google in EEB 105 tomorrow, 2/3, from 5:30-7:30

February 2, 2010

Reminder to check out Exploration Seminars – study abroad

We know that many of you are interested in Study Abroad opportunities but you are often concerned about time away from UW.  If you haven’t looked into Exploration Seminars, we highly recommend you consider it.

Here is general information, and below is info on a program to Japan as an example. They are generally open to students from any major and often fulfill general education requirements.

Exploration Seminars: http://depts.washington.edu/explore/

_________________________________________

Gods and Mountains: Icons, Temples, and Pilgrimage
2010 Exploration Seminar in Japan

Program Director: Cynthea J. Bogel <mailto:cjbogel@u.washington.edu> , Art History
Dates of Instruction: August 20 – September 10, 2010

FOR MORE INFORMATION SEE

http://depts.washington.edu/explore/programs/2010/japantemples.htm

$1000 scholarships (merit based) are available for undergraduates.

Financial Aid is applicable to the Early Fall Program

DESCRIPTION

On this 21-day seminar we will explore the artistic and religious culture of Japan’s mountains and ancient capitals and walk the World Heritage ancient pilgrimage mountain route from the Kumano region (south Wakaama Prefecture) to Mt. Koya.  Visits to Buddhist temples and Shinto shrines in the mountains near Kyoto and Nara comprise a major element of Japanese religious practices, past and present. The early fall Exploration Seminar features the study of temples and shrines in the mountains outside the eighth-century capital of Nara, the ninth- to twelfth-century capital of Kyoto, and pilgrimage routes to sites in the Wakayama peninsula south of Nara. Our visits to remote regions of Japan will provide first-hand experience of rigors demanded of religious devotees, and allow us to consider the important role travel has played in Japan’s rich religious history. During the seminar we experience the power of the natural world and Japan’s rich pilgrimage and more isolated temple traditions by experiencing the natural world through hiking and walking, staying at temples, close visual study of icons and icon halls and discussions with pilgrims, monks and nuns, and temple experts.

Students will live in a traditional Buddhist temple during their stay on Mt. Kōya (stay 5-6 days), an esoteric Buddhist temple complex founded by Kūkai Kōbō Daishi in the ninth century and important pilgrimage site for royalty, warriors, and ordinary people from the tenth century until today. From Kōya we will head south on the Kumano–Kodo (ancient road) toward the Kumano Sanzan (Three Shrines of Kumano), staying in traditional lodges along the way (3–4 days rigorous hike). This pilgrimage route, traveled since the middle of the Heian period (eighth to twelfth centuries), links the sacred Buddhist grounds of Mt. Kōya with the Shinto shrines of the Kii Mountain range, which are considered some of the oldest religious sites in all of Japan.

During our stay in a traditional setting we will explore the Kumano–Nachi area (2 days), including Nachi taki, the tallest waterfall in Japan and the original religious site of the area, and the shrine/temple complex of Kumano Nachi Taisha and Seigantōji. From there, students will go by train to Kyoto. Residing in a Zen monastery there, we will make day trips to Mt. Hiei (mountain headquarters of Tendai Buddhism), Daimonji (a mountainside into which each year a huge Chinese character is burned as part of the O-Bon religious festivities), and Shinto shrines. Then students will move to Nara, where we will hike the Yagyûkaidô and visit temples such as Murôji, Hasedera, and others deep in the forested hills and mountains.  At 3000 feet, and reached by cable car, Mt. Kôya will be the highest peak visited. Hikes are from 800–1600 feet.

This seminar will consider the development of temples, shrines, and religious practices in the hills and mountains from several aspects, creating a rich context of past and present: the historical, the visual (icons, architecture and art study), and the religious and ritual. The religious contextsof pilgrimage and mountain traditions differ in important ways from those found in cities like Kyoto. We will consider the many ways in which the demands of strenuous travel and an itinerant lifestyle affect the contours and contrasts of religious motivations, beliefs, icon-making, and practices to attain enlightenment. Along with Buddhist and native god or “Shintō” traditions, we will explore Shugendō, Japan’s tradition of mountain-dwellers and ascetics that amalgamates Buddhist, Chinese, and local religious practices. We will also consider the comparative dimensions of pilgrimage and attempt to identify common themes, styles, and subjects among Japanese, Chinese, and Korean temples. Study of mountain temples near the great capitals of Kyoto and Nara will serve to highlight the need for monks and nuns to isolate themselves from the activities of the capital even while serving to protect them. The goal of this seminar is to instill in students not only an appreciation of lesser-known aspects of Japanese “syncretic” religion, visual culture, and history but to provide first-hand experience of these historical phenomena in living modern forms. Field trips will take place daily and will be led by the professor and assistant. Students will keep a journal and will respond in their journal to questions distributed at the sites. Additionally, students will be encouraged to explore one aspect of particular interest to them and pursue independent study.

The expertise of assistant Lindsey DeWitt, Ph.D. candidate, Buddhist Studies UCLA (University of Washington M.A., Comparative Religions) will greatly enhance the Seminar. We will also deeply benefit from the guidance of monks on Mt. Koya and at Kumano. In Kyoto, the son of our host temple within Myoshinji is Vice Abbot and speaks fluent English.

Experience of director: Two previous Exploration Seminars in Japan. Director of the Oregon study abroad program at Waseda and Aoyama Gakuin in Tokyo (one academic year), 1995-96. Researched this new Seminar, facilities, routes, etc. during one week stay after 09 Exploration Seminar. Teaching a graduate/undergraduate seminar this Fall term (09) on the subject of Mountain Temples, Icons, and Gods to prepare all background and readings for the proposed Seminar. This seminar combines previous seminar cities (Kyoto and Nara) with entirely new temples there, and entirely new mountain pilgrimage trips. Fluent in Japanese.

Credits: Participants may receive 5 credits of either:

*    ART H 321: Arts of Japan (I&S/VLPA) which can be counted toward the Asian Studies major (Japan or General concentrations), or toward the Japan Studies minor; see (http://jsis.washington.edu/advise/undergradstudy.html).
*    RELIG 399 (I&S) for Comparative Religion majors
*    ART H 499 or 515 , graduate credit and honors credit are also possible but only with approval and consultation with Prof. Bogel or your advisor. Some students may also be permitted to add 2-3 additional credits during the fall term for extended research and writing on exceptional projects.

Participants should check with their academic advisors to determine how these credits may apply to major requirements.

Books and Readings:

*    Required: Moerman, D. Max. Localizing Paradise: Kumano Pilgrimage and the Religious Landscape of Premodern Japan, Harvard East Asian monographs, 235 (Cambridge, Mass.: Harvard University Asia Center: Distributed by Harvard University Press, 2005).
*    Required: Ten Grotenhuis, Elizabeth. Japanese Mandalas: Representations of Sacred Geography. Honolulu: University of Hawai’i Press, 1999. Selections.
*    Recommended: Thal, Sarah. Rearranging the Landscape of the Gods: The Politics of a Pilgrimage Site in Japan, 1573-1912 (Chicago: University of Chicago Press, 2005).

Student costs:

*    $3,350 Program Fee
*    $250 International Programs & Exchanges Fee <http://www.ipe.washington.edu/domestic/cefaq.html>
*    Click here for a Estimated Budget of Student Expenses  <http://depts.washington.edu/explore/docs/budgets/> (for financial aid requests)
*    The program fee includes all lodging, all ground travel costs in Japan (excluding round trip from/to  Kansai/Osaka International airport to/from our base temple, estimate $60), six dinners and six breakfasts, all entry fees to temples, sites, and museums. This extensive coverage at very reduced cost is made possible through arrangements between the director and our host temples and lodgings.
*    Additional costs include: round trip airfare to Japan, health insurance, meals not noted above, and personal expenses including personal travel.

Students attending this exploration seminar are eligible to apply for a $1000 Freeman scholarship, which are given out on the basis of academic merit to select students on Exploration Seminar programs in East and Southeast Asia. The application deadline is March 1

FOR MORE INFORMATION SEE

http://depts.washington.edu/explore/programs/2010/japantemples.htm

$1000 scholarships (merit based) are available for undergraduates.

Financial Aid is applicable to the Early Fall Program

February 2, 2010

Google NSBE Conference Travel Scholarship

Deadline to apply: February 12, 2010

As part of Google’s on-going commitment to diversity and education in computing and technology, we are pleased to announce the Google National Society of Black Engineers (NSBE) Travel Scholarship. At Google, we are enthusiastic about supporting STEM (Science, Technology, Engineering, Math) education for all students, particularly those who represent a broad range of cultures and backgrounds. Through this scholarship, we hope to encourage more underrepresented computer science students to attend and participate at NSBE 2010 in Toronto, Canada, on March 31 – April 4. We hope you take advantage of this opportunity and apply!

The Scholarship is open to all qualified undergraduate and graduate students. Conference details can be found at http://convention.nsbe.org/convention2010/. Each selected student will receive up to $1,500 USD for airfare, hotel, conference registration and other travel requirements.
Applicants must satisfy the following eligibility criteria:
•    Enrolled full-time in their undergraduate or graduate study at a university in the United States, Canada or Puerto Rico
•    Pursuing a Computer Science, Computer Engineering, or related technical field major
•    Maintaining a strong academic background with demonstrated leadership ability
•    Able to attend 2+ days of the conference
How to Apply

Please complete the online application and submit all required documents by Friday, February 12th. First-time users will be required to register and create an account.
___________________

**Other Google Scholarships Open for Application**

•    Google Anita Borg Memorial Scholarship for First Years application is due February 15, 2010
•    Google Hispanic College Fund Scholarship application is due February 16, 2010
•    Google United Negro College Fund Scholarship application is due April 16, 2010

February 2, 2010

Clean Power Research UW employer information session & interviews

Clean Power Research will be holding an employer information session at UW on Wed, Feb 10 and on-campus interviews on Wed, Feb 24.  The information session is a great way to find out about Clean Power Research, our career opportunities, and talk to us.

About the company:
Clean Power Research builds software products for the renewable energy industry.  We’re a small, dynamic company with a great industry position and are growing rapidly.  As part of our growth, we are hiring for full time and intern Software Engineer positions.  We’re looking for people with great core computer science and software engineering skills who are passionate about renewable energy.  Positions are in Kirkland, WA.

Our current products include Clean Power Estimator®, an application that estimates cost and benefits of clean energy systems; PowerClerk®, a web-based application for administrating financial incentives; QuickQuotes, which enables dealers and resellers to quickly generate sales quotes for clean energy systems; SolarAnywhere, which provides real-time and forecasted insolation (sunlight) data; and more products on the way.

Information session:
Wed, Feb 10, 5:30pm
UW Career Center lobby, 134 Mary Gates Hall
Please RSVP on HuskyJobs www.huskyjobs.washington.edu/students/ (under the Info Sessions link)

On-campus interviews:  Wed, Feb 24
Sign up on HuskyJobs www.huskyjobs.washington.edu/students/

Hope to see you there!

Jeremy Stone
Clean Power Research

February 1, 2010

« Newer PostsOlder Posts »