Name
Abstract | ||
|---|---|---|
Automated theorem proving lies at the heart of all tools for formal analysis of software and system descriptions. In formal verification systems such as PVS (10), the deductive capability is explicit and visible to the user, whereas in tools such as test case generators it is hidden and often ad-hoc. Many tools for formal analysis would benefit—both in performance and ease of construction—if they could draw on a powerful embedded service to perform common deductive tasks. An embedded deductive service should be fully automatic, and this suggests that its focus should be restricted to those theories whose decision and satisfia- bility problems are decidable. However, there are some contexts that can tolerate incompleteness. For example, in extended static checking, the failure to prove a valid verification condition results only in a spurious warning message. In other contexts such as construction of abstractions, speed may be favored over com- pleteness, so that undecidable theories (e.g., nonlinear integer arithmetic) and those whose decision problems are often considered infeasible in practice (e.g., real closed fields) should not be ruled out completely. Most problems that arise in practice involve combinations of theories: the question whether f(cons(4◊car(x) 2◊f(cdr(x)),y)) = f(cons(6◊cdr(x),y)) follows from 2◊car(x) 3◊cdr(x) = f(cdr(x)), for example, requires simulta- neously the theories of uninterpreted functions, linear arithmetic, and lists. The ground (i.e., quantifier-free) fragment of many combinations is decidable when the fully quantified combination is not, and practical experience indicates that automation of the ground case is adequate for most applications. Practical experience also suggests several other desiderata for an eective deductive service. Some applications (e.g., construction of abstractions) invoke their deductive service a huge number of times in the course of a single calcula- tion, so that performance of the service must be very good. Other applications such as proof search explore many variations on a formula (i.e., alternately assert- ing and denying various combinations of its premises), so the deductive service should not examine individual formulas in isolation, but should provide a rich application programming interface that supports incremental assertion, retrac- tion, and querying of formulas. Other applications such as test case generation |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-25984-8_14 | Lecture Notes in Artificial Intelligence |
Keywords | Field | DocType |
real closed field,automated theorem proving,application program interface,formal verification,decision problem | Discrete mathematics,Automated reasoning,Programming language,Computer science,Automated theorem proving,Algorithm,Software,Distributed computing,Formal verification | Conference |
Volume | ISSN | Citations |
3097 | 0302-9743 | 29 |
PageRank | References | Authors |
1.62 | 8 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Leonardo de Moura | 1 | 3539 | 150.15 |
| Sam Owre | 2 | 1323 | 104.39 |
| Harald Rueß | 3 | 526 | 38.69 |
| John Rushby | 4 | 2459 | 235.69 |
| Natarajan Shankar | 5 | 3050 | 309.55 |