Name
Abstract | ||
|---|---|---|
There is a growing trend to integrate theorem proving systems with specialized decision procedures and model checking systems.
The proving capabilities of the PVS theorem prover, for example, have been improved considerably by extending it with new
proof tactics based on a BDD package, a μ-calculus model-checker [4], and a polyhedral library. In this way, a theorem proving system like PVS provides a common front-end
and specification language for a variety of specialized tools. This makes it possible to use a whole arsenal of verification
and validation methods in a seamless way, combine them using a strategy language, and provide development chain analysis.
|
Year | DOI | Venue |
|---|---|---|
2000 | 10.1007/10722167_42 | CAV |
Keywords | Field | DocType |
arsenic,verification and validation,theorem proving,specification language,theorem prover,front end,model checking | Specification language,Model checking,Programming language,Verification and validation,Computer science,Automated theorem proving,Algorithm,Theorem Proving System,Binary decision diagram,Theoretical computer science,Formal verification | Conference |
ISBN | Citations | PageRank |
3-540-67770-4 | 6 | 0.58 |
References | Authors | |
3 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sam Owre | 1 | 1323 | 104.39 |
| Harald Rueß | 2 | 526 | 38.69 |