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.

Important Dates


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.

Workshop Program

Wednesday, May 18

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
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
5:00 Adjourn
6:00 Group Dinner
The Wine Bistro, 1750 Lane Avenue

Thursday, May 19

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
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.

Friday, May 20

8:30 Session VI: Discussion
DL 480
Educators Session
DL 698
Joe Hollingsworth Effective Teaching: Make it Stick
Murali Sitaraman Reasoning with RESOLVE
(slides 1, slides 2)
10:30 Break
10:45 Session VII: Teaching with Specs
DL 480
Paolo Bucci Recursion
Murali Sitaraman Iteration
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
Dustin Hoffman A tool demo
3:00 Session IX: Conclusion
DL 480
3:30 Adjourn


Program Committee


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 [] should be sent as PDF attachments via email to Diego Zaccai (zaccai.1 [at] osu . edu). The proceedings will be published electronically.

Participation and Accommodation

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.

Workshop History