Name
Abstract | ||
|---|---|---|
This paper describes a semantic connection between the symbolic trajectory evaluation model-checking algorithm and relational verification in higher-order logic. We prove a theorem that translates correctness results from trajectory evaluation over a four-valued lattice into a shallow embedding of temporal operators over Boolean streams. This translation connects the specialized world of trajectory evaluation to a general-purpose logic and provides the semantic basis for connecting additional decision procedures and model checkers. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48153-2_16 | CHARME |
Keywords | Field | DocType |
higher order logic,theorem proving | Discrete mathematics,Model checking,Computer science,Correctness,Automated theorem proving,Binary decision diagram,Boolean algebra,Temporal logic,Boolean data type,Trajectory | Conference |
Volume | ISSN | ISBN |
1703 | 0302-9743 | 3-540-66559-5 |
Citations | PageRank | References |
3 | 0.50 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mark Aagaard | 1 | 292 | 34.39 |
| Thomas F. Melham | 2 | 384 | 35.63 |
| John W. O'Leary | 3 | 187 | 26.29 |