Write a Blog >>
Sun 18 Jun 2017 09:30 - 10:00 at Vertex WS208 - Session 1

This research aims to show through a detailed case study that scaling up modular verification to component-based software is not only possible, but when combined with appropriate tool support, can be made more comprehensible and practicable to researchers and students in the software engineering (SE) curriculum. The study involves an interplay of multiple components that have novel designs and object-oriented interfaces to encapsulate non-trivial data structures and algorithms. Each component is annotated with formal specifications that are all designed to be modular, reusable, and amenable to automated verification and analysis. The components are constructed using a formalization integrated development environment (F-IDE) that we’ve built for this purpose. Experimental evaluation of the F-IDE itself will be performed in the context of the software engineering curriculum at Clemson University over the course of upcoming semesters, while evaluation of the various components involved in the study will be performed on the basis of the provability of mechanically generated proof obligations.

Sun 18 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
09:00
10m
Talk
Introduction
ECOOP Doctoral Symposium

09:10
20m
Talk
Lightning talks
ECOOP Doctoral Symposium

09:30
30m
Talk
Scaling Up Automated Verification: A Case Study and A Formalization IDE for Building High Integrity Software
ECOOP Doctoral Symposium
Daniel Welch Clemson University
10:00
30m
Talk
Enabling Modular Verification of Concurrent Programs
ECOOP Doctoral Symposium