Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Jonathan Aldrich: Typestate Verification for Aliased Objects using Assume-Guarantee Permissions</h1> <div class='date'><time class="dtstart dt-start" title="2008-08-12T10:30:00" datetime="2008-08-12T10:30:00">Tuesday, August 12, 2008 from 10:30</time>–<time class="dtend dt-end" title="2008-08-12T11:30:00" datetime="2008-08-12T11:30:00">11:30am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390386'><span class='fn org p-name'>Portland State University Engineering Building</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">1930 SW 4th Ave</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">Oregon</span> <span class="postal-code p-postal-code">97201</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=1930%20SW%204th%20Ave,%20Portland%20Oregon%2097201%20US'>map</a>) </div> </div> <div class="description p-description"> <p>We are having a special summer colloquium presentation by Jonathan Aldrich of CMU on Tuesday, August 12, at 10:30am. Title and abstract below.</p> <p>The talk will be in the Dean's Conference room (EB 500) in the Engineering Building at Portland State University.</p> <p>Jim Hook (hook at cs dot pdx dot edu) is acting as host.</p> <p>TITLE: Typestate Verification for Aliased Objects using Assume-Guarantee Permissions</p> <p>ABSTRACT: Object-oriented libraries often define usage protocols that clients must follow in order for the system to work properly. Typestates use state machines to specify these protocols, but previous protocol verification systems have significant practical problems in their precision, scaleability, easy of use, and applicability to standard coding styles and idioms.</p> <p>We are exploring a new approach to verifying typestate using assume- guarantee permissions. These permissions track not only the state of an object, but an abstraction of what operations other aliases might perform on the object. Developers annotate their code with state and permission information, which can be automatically and soundly checked for consistency. Our approach is fully modular, yet allows substantial reasoning about objects even when they are aliased by multiple clients. We will describe novel approaches for reasoning about inheritance and concurrency, and show case studies verifying code (and finding one defect) in well-tested Java standard library code.</p> <p>This is joint work with Kevin Bierhoff and Nels Beckman.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://mailhost.cecs.pdx.edu/pipermail/cs-colloq/2008-August/000137.html">Website</a></li> </ul> </div>