Abstract
Stålmarck’s Method is a patented natural deduction proof method with a novel proof-theoretic notion of proof depth, defined as the largest number of nested assumptions in the proof. An implementation of the method, called Prover, has been used as proof engine in various commercial tools since 1990, and is now integrated in a formal verification framework called NP-Tools. Prover searches for shallow subformula proofs, which has proven to be an efficient strategy for solving many industrial problems, the largest of which today consists of several 100,000’s of sub-formulas. Stålmarck's method is in industrial use, for instance in the areas of telecom service specification analysis, analysis of railway interlocking software, analysis of programmable controllers and analysis of aircraft systems. The method seems suitable also for hardware verification.
Cite
CITATION STYLE
Borälv, A. (1997). The industrial success of verification tools based on stålmarck’s method. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1254, pp. 7–10). Springer Verlag. https://doi.org/10.1007/3-540-63166-6_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
