Forgot your password?
New user?
Draft Outline
Document Actions
last edited 2 years ago by shankar
Outline of the Verified Software Roadmap
[[Introduction]]?
Background
[[Technical]]?
Highlights of Forty Five Years of Verification
Motivation
The Verified Software Grand Challenge
Executive Summary of the Roadmap
Organization
Salient Points
Milestones
System Reliability and Certification
Pilot Projects
Repository
Benchmarks
Tools
Tutorials
Research Directions
Requirements, Models, Specifications
The challenges involved in translating informal descriptions of expected software behavior into a formal model are outlined in this subsection.
Design Methods
The challenges/milestones in designing correct software relative to formal specifications are outline here, including refinement, program generation, and staging.
Verification Methods
The methods used for verifying software include
- Logics
- Proof rules
- Proof techniques: refinement
- Language features: Types, analysis, language subsets, assertions
Integrated Verification Environments
Interoperable Tools
- Intermediate and interchange formats
- Libraries
- Tools
- Semantic Tool Bus
- Systems
- Proof Libraries
Linking Theories
Verified Tools
Experiments
- Device drivers
- Web services
- openSSL
- Hypervisor
- Libraries: Eiffel, Java
- Operating Systems security
- Lightweight runtime environments
- Web browser
- Scientific software packages
- Javacard
- TCP/IP
- Medical devices
- Avionics
- Automobiles and embedded systems
- Domain modeling
- E-Voting
- SCADA
- Middleware platforms
