Specification engineering and modular verification using a web-integrated verifying compiler

This demonstration will present the RESOLVE web-integrated environment, which has been especially built to capture component relationships and allow construction and composition of verified generic components. The environment facilitates team-based software development and has been used in undergrad...

Full description

Saved in:
Bibliographic Details
Main Authors: Cook, C. T., Harton, H., Smith, H., Sitaraman, M.
Format: Conference Proceeding
Language:English
Subjects:
automation
Cognition
Component architectures
education
Educational institutions
generic components
Java
Software
Software engineering
Sorting
specification
system description
verification
web IDE
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This demonstration will present the RESOLVE web-integrated environment, which has been especially built to capture component relationships and allow construction and composition of verified generic components. The environment facilitates team-based software development and has been used in undergraduate CS education at multiple institutions. The environment makes it easy to simulate "what if" scenarios, including the impact of alternative specification styles on verification, and has spawned much research and experimentation. The demonstration will illustrate the issues in generic software verification and the role of higher-order assertions. It will show how logical errors are pinpointed when verification fails. Introductory video URL: http://www.youtube.com/watch?v=9vg3WuxeOkA.
ISSN:0270-5257
1558-1225
DOI:10.1109/ICSE.2012.6227243