May 18–20, 2016
The Ohio State University, Columbus, Ohio
To serve as a forum for interaction among researchers, practitioners, and educators interested in software engineering with emphasis on formal specification and reasoning.
The workshop will take place in Dreese Labs at The Ohio State University. The closest visitor parking is in Tuttle Park Garage.
For internet access, SSID WiFi@OSU provides an open, unencryped connection. For secure access, eduroam is available (if your home institute is a member).
The plenary sessions and research workshop will take place in room 480, while the educators sessions will take place in 698.
A summary of local arrangements, including hotel, parking, and restaurant information is available here.
| 1:45 | Paul Sivilotti | Welcome and Introductions DL 480 |
||
| 2:00 | Session I: Foundations and Types DL 480 |
Educators Session
DL 698 |
||
| Blair Durkee (author) Bill Ogden (discussant) |
Implementing Class Theory for Mathematical Type Checking | Murali Sitaraman Joe Hollingsworth |
Reasoning with RESOLVE Basics (slides) |
|
| 3:30 | Break | |||
| 3:45 | Session II: Prover DL 480 |
Educators Session
DL 698 |
||
| Mike Kabbani (author) Bill Ogden (discussant) |
Developments in the Integrated Prover | Murali Sitaraman Joe Hollingsworth |
Reasoning with Objects (slides) |
|
| 5:00 | Adjourn | |||
| 6:00 | Group Dinner The Wine Bistro, 1750 Lane Avenue |
|||
| 9:00 | Keynote DL 480 |
||
| Joan Krone Bruce Weide Joe Hollingsworth Wayne Heym Greg Kulczycki Murali Sitaraman |
History of RESOLVE, as told through selected dissertations (slides for Krone, Weide, Hollingsworth, Heym, Kulczycki, Sitaraman) |
||
| 10:30 | Break | ||
| 10:45 | Session III: Aliasing and Sharing DL 480 |
||
| Yu-Shan Sun | Towards Automated and Modular Verification in the Presence of Objects that Share Space | ||
| Diego Zaccai | Not Seeing The Objects For The References | ||
| 12:15 | Lunch (on your own) | ||
| 2:00 | Session IV: Concurrency DL 480 |
||
| Alan Weide | Intermediate Models for Expressing Parallelization Opportunities with Abstract Data Types | ||
| 3:00 | Break | ||
| 3:15 | Session V: HPI (Human-Prover Interaction) DL 480 |
||
| Matthew Pfister | Summary of Progress and Future Plans for the Novel Logical Reasoning Tutor (slides) |
||
| Daniel Welch | Designing a Fully Featured IDE for Engineering Modular, Verified Software | ||
| 4:45 | Adjourn | ||
| Dinner on your own Suggestion: variety of options at 1301 W. Lane Ave. |
|||
| 8:30 | Session VI: Discussion DL 480 |
Educators Session
DL 698 |
||
| Joe Hollingsworth | Effective Teaching: Make it Stick (notes) |
Murali Sitaraman | Reasoning with RESOLVE (slides 1, slides 2) |
|
| 10:30 | Break | |||
| 10:45 | Session VII: Teaching with Specs DL 480 |
|||
| Paolo Bucci | Recursion (slides) |
|||
| Murali Sitaraman | Iteration (slides) |
|||
| 11:45 | Group Lunch The Blackwell Bistro, 2110 Tuttle Park Place |
|||
| 1:30 | Session VIII: Connecting with Practice DL 480 |
|||
| Joan Krone | The Gap between Theory and Practice: A Challenge | |||
| Ferry Pramudianto | A Peer-Assessment Experiment in Object-Oriented Design (slides) |
|||
| Dustin Hoffman | A tool demo | |||
| 3:00 | Session IX: Conclusion DL 480 |
|||
| 3:30 | Adjourn | |||
Submissions may be made in the form of short position statements or extended abstracts. They should be targeted at raising a question or framing an issue for discussion during the workshop. The papers may be 1 or 2 pages. The papers should conform to the two column IEEE Transactions style [http://www.ieee.org/web/publications/authors/transjnl/index.html] should be sent as PDF attachments via email to Diego Zaccai (zaccai.1 [at] osu . edu). The proceedings will be published electronically.
For questions regarding registration, please contact Joe Hollingsworth (jholly [at] ius . edu). The recommended hotel is the Holiday Inn Express at 3045 Olentangy River Road.
Registration is now closed.