Third Northeastern Verification Meeting
NEVER (again)
NEVER (again)
NEVER
We would like to invite you to the NEVER (Again): The Third Northeastern Verification Seminar. The third meeting will be held at NEC Labs America, Princeton, NJ on Friday, the 18th of May 2007.Previous meetings were held at Bell Laboratories in March 2006 and at NYU in October 2006. The goal of these meetings is to encourage interaction among local research groups interested in formal methods for system verification. Our third meeting will be similar in format to the previous meetings with 30 minute presentations from each research group. For this meeting, we propose the theme "Software Verification". We are also pleased to host a special panel discussion titled "Verification - What works and what does not?".
If you plan to attend, please send a RSVP to the organizers in advance.
Panel Discussion: Verification - What works and what does not?
We are pleased to host a panel discussion titled "Verification - What works and what does not?". This discussion is meant to be a lively exploration of the current and emerging trends in formal verification, with an emphasis on its practical application to the many real world problems that we face.| Moderator | Kedar Namjoshi (Lucent) |
| Panelists | Rajeev Alur (U Penn) |
| Stephen Edwards (Columbia) | |
| John Field (IBM) | |
| Aarti Gupta (NEC Labs) | |
| Bob Kurshan (Cadence) | |
| Sharad Malik (Princeton) |
Program
| 9:15 - 9:45 | Coffee & Breakfast |
| 9:45 - 10:00 | Welcome Address: Roger Tran (President, NEC Labs) |
| Session #1 | |
| 10:00 - 10:30 | Dennis Dams (Bell Labs), StackSnuffer: Curing Orion's Unsoundness |
| 10:30 - 11:00 | Stephen Edwards (Columbia), Verification Challenges in the SHIM Concurrent Language |
| 11:00 - 11:30 | Yogesh Mahajan (Princeton), Verification Driven Formal Microarchitecture Modeling |
| 11:30 - 12:00 | John Field (IBM), Semantics-Based Reverse Engineering of Logical Data Models |
| 12:00 - 1:30 (LUNCH) | |
| 1:30 - 2:30 | Panel Discussion |
| 2:30 - 3:00 | Scott Stoller (SUNY Sb), Efficient Policy Analysis for Administrative Role Based Access Control |
| 3:00 - 3:30 | Richard Chang (UT Austin), Formal Analysis of Authentication in Bluetooth Device Pairing |
| 3:30 - 4:00 (COFFEE BREAK) | |
| 4:00 - 4:30 | Nina Amla (Cadence), Combining Abstraction Refinement and Interpolation-based Model Checking. |
| 4:30 - 5:00 | Sebastian Burckhardt (U Penn), Checking Consistency of Concurrent Data Types on Relaxed Memory Models |
| 5:00 - 5:30 | Yeting Ge (NYU), Solving Quantified Verification Conditions using Satisfiability Modulo Theories |
| 5:30 - 6:00 | 5 Minute Madness |
| Gera Weiss (U Penn), Automata based interfaces for control and scheduling | |
| Swarat Chaudhuri (U Penn), TBA | |
| Sriram Sankaranarayanan (NEC Labs), Milk Cartons, Soup Cans, Cornflakes, Pokemon & Models. |