The goal of this session is to learn about how the government currently certifies different kinds of software, and how current efforts are attempting to improve this.
10:00–12:00 Current certification processes.
What is the state of the art in program analysis and program verification relevant to this study? Are fundamental limits to what can be achieved? How should these methods be used as part of a larger assurance mechanism?
1:00–2:15 Analysis and verification.
This session examines how methods for annotating programs with types, specifications, or other annotations can be used to obtain assurance. Again, we want to understand the limits and potential synergies of such methods.
2:30–3:55 Exploiting annotations and specifications
The plan is to talk about more dynamic methods that involve running program code to obtain added assurance, such as testing and model checking, and other program transformations that add assurance.
4:10–5:00 Model checking, transformation and monitoring
5:00–5:30 Wrap-up discussion
In closing, we want to identify promising directions for improving software assurance. Are there underexplored ideas or synergies between existing approaches? We also want to discuss what related approaches we haven't spent enough time looking at yet.