Abstract | ||
---|---|---|
Hoareu0027s logic helps with program state descriptions, but is difficult to manipulate. Model checking emerged as a new trend in program verifications is best applied to system designs rather than implementations. This paper is committed to establish a component-based verification framework that combines both of them. The method applied consists of two steps: regarding predicates as states and connecting them with functional components in light of their relationships. Once a framework is set up, both program generation and verification can be automatically carried out. The principle presented here is not only applicable to sequential programs, but also to other types of program structures and paradigm such as iteration, branch structure and grammatical evolution, etc. |
Year | Venue | Field |
---|---|---|
2015 | JSW | Functional verification,Programming language,Model checking,Computer science,Implementation,Theoretical computer science,Artificial intelligence,Predicate (grammar),Grammatical evolution,Machine learning |
DocType | Volume | Issue |
Journal | 10 | 11 |
Citations | PageRank | References |
0 | 0.34 | 8 |
Authors | ||
4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Pei He | 1 | 0 | 0.34 |
Achun Hu | 2 | 0 | 0.68 |
Dongqing Xie | 3 | 277 | 24.78 |
Zhi-ping Fan | 4 | 6 | 2.92 |