RESOLVE 2013: Progress towards Software Verification

June 3 -- 4, 2013

Denison University, Granville, Ohio


Monday, June 3

Time Topic Speaker(s)
8:45 am Welcome and Introductions Joan Krone
Session I: Specification and Verification Progress (Olin Hall, Second Floor)
9:00 am A Language for Building Verified Software Components Greg Kulczycki
9:30 am Verification of VCs involving multiple theories Blair Durkee
9:55 am Refuting Untrue Verification Conditions Diego Zaccai
10:20 am Questions and Discussion
10:30 am Break
10:45 am Finer Technical Details in Specifying a Concept for Pointer Behavior Yu-Shan Sun
11:10 am Questions and Discussion
11:20 am Tuning a Minimalist Prover for the Verification Task Hampton Smith
11:45 am General Discussion
12:00 noon Lunch (Welch Hills Room)
Session II: Teaching Matters (Olin Hall, Second Floor)
1:30 pm Education Directions Bruce Weide
2:15 pm Using the RESOLVE Web IDE in the Classroom Nigamanth Sridhar
2:40 pm A Framework for Teaching and Assessment of Math Reasoning Principles Joe Hollingsworth
3:10 pm Questions and Discussion
3:20 pm Break
3:35 pm Outreach: Who Needs It? Yvon Feaster
4:00 pm On Teaching Mathematical Reasoning Murali Sitaraman
4:25 pm Questions and Discussion
6:00 pm Dinner (Buxton Inn)

Tuesday, June 4

Time Topic Speaker(s)
9:00 am RESOLVE: Future Directions Bill Ogden
Session III: Work in Progress(Olin Hall, Second Floor)
9:45 am Prioritizer Application Dan Welch
10:10 am Verifying Robotic Movement on a 2- Dimensional Plane Mark Todd
10:35 am Break
10:55 am The Internet of Things Farha Ali
11:20 am Integrating Performance Profiles and Verification Conditions with Functionality Verification Nighat Yasmin
11:45 am Questions and Discussion
12:15 pm Lunch (Picnic)
Session IV: A Look to the Future (Olin Hall, Second Floor)
1:30 pm Invitation to share work in progress
2:20 pm Final Thoughts: Goals for the Future
3:00 pm End