Name
Abstract | ||
|---|---|---|
For software components to be reused with confidence, they must be correct. Unlike testing, formal verification can be used to certify that a component will behave correctly regardless of context, as long as that context satisfies component assumptions. Some verification systems for developing correct components in languages such as Java are simplified to be practical, but are not complete. Other systems that account for necessary semantic complications arising from underlying reference behavior demand non-trivial specification and verification. This paper describes an alternative. Under this approach, reusable components are specified, implemented, and verified in RESOLVE, a language with clean semantics, and are translated to Java. To improve confidence in the verification process, we are currently re-engineering the RESOLVE verification system itself with generated verified components. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-04211-9_2 | ICSR |
Keywords | Field | DocType |
software component,reusable component,necessary semantic complication,component assumption,correct component,verification system,verification process,generating verified java components,clean semantics,formal verification,resolve verification system,satisfiability | Functional verification,Programming language,Intelligent verification,Computer science,Verification,Runtime verification,High-level verification,Java,Formal verification,Software verification | Conference |
Volume | ISSN | Citations |
5791 | 0302-9743 | 6 |
PageRank | References | Authors |
0.51 | 17 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hampton Smith | 1 | 56 | 5.01 |
| Heather Harton | 2 | 56 | 4.00 |
| David Frazier | 3 | 6 | 0.51 |
| Raghuveer Mohan | 4 | 6 | 0.85 |
| Murali Sitaraman | 5 | 270 | 40.99 |