Name
Abstract | ||
|---|---|---|
We present a hybrid approach to program veriflcation: a higher-order logic, used as a speciflcation language, and a human-driven proof environment, with a process-algebraic engine to allow the use of process simulation as an abstraction technique. The domain of appli- cation is the validation of object code, and our intent is to adapt and mix existing formalisms to make the veriflcation of representative pro- grams possible. In this paper, we describe the logic in question and an underlying semantics given in terms of a process algebra. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/BFb0055128 | TPHOLs |
Keywords | Field | DocType |
higher-order logic framework,program abstraction,process simulation,higher order logic,process algebra | Functional verification,Programming language,Computer science,Algorithm,Multimodal logic,Bunched logic,Theoretical computer science,Logic simulation,High-level verification,Dynamic logic (modal logic),Higher-order logic,Formal verification | Conference |
Volume | ISSN | ISBN |
1479 | 0302-9743 | 3-540-64987-5 |
Citations | PageRank | References |
2 | 0.41 | 5 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marco Benini | 1 | 16 | 4.85 |
| Sara Kalvala | 2 | 59 | 9.03 |
| Dirk Nowotka | 3 | 213 | 42.90 |