Progress and challenges in software verification

May 29–30, 2018

480 Dreese Labs
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.


Tuesday, May 29

9:00 Joe Hollingsworth and
Paul Sivilotti
Opening remarks
9:15 Session 1: Looking backwards and forwards
Murali Sitaraman and
Bruce Weide
A Synopsis of Twenty Five Years of RESOLVE PhD Research Efforts
Daniel Welch Formalization Integrated Development Environments: The Current Landscape
Paul Sivilotti Verification Benchmarks
11:30 lunch (Blackwell Bistro)
1:00 Session 2: Education
Eileen Kraemer Teaching the Design-by-Contract Concept in a Software Engineering Course Using RESOLVE
Aubrey Lawson and
Eileen Kraemer
Reasoning About Concurrency: Scenarios for Activities
Megan Fowler and
Tim Schwab
BeginToReason: Understanding the Purpose of Code
3:30 Session 3: Keynote
Harvey Friedman This Foundationalist Looks at P = NP

Wednesday, May 30

9:00 Joe Hollingsworth and
Paul Sivilotti
Opening remarks
9:15 Session 4: Sharing and concurrency
Alan Weide Reasoning Challenges of Data Abstraction and Aliasing in Concurrent Programs
Yu-Shan Sun Reasoning About Reference Behavior with RESOLVE
Bill Ogden A New Concept for Realizing and Reasoning about Linked Structures
11:45 lunch (on your own)
1:00 Session 5: Going forward
Saad Asim An Exercise in Design: The Binary Decision Diagram
Joan Krone Food for Thought
3:00 Workshop conclusion


Program Committee


The workshop will take place in Dreese Labs (room 480) at the Ohio State University. The closest visitor parking is in Tuttle Park Garage.

Instructions for internet access while on campus are available here. An unencrypted network available for guest access (WiFi@OSU), as well as a secure connection through eduroam (if your home institution is a member).

Registration for the workshop is now closed. However, anyone is welcome to attend the talks listed in the program.

Workshop History