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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arne Borälv and Herman Ågren. Feasibility Study SVT. Technical Report U-95002, Logikkonsult NP AB, 1995. Internally published at Logikkonsult.
Hans Bolinder. LSA 1.0. Technical Report NPT-01-07-0-3, Issue 2 Rev 1, Logikkonsult NP AB, 1996.
Arne Borälv. A Fully Automated Approach for Proving Safety Properties in Interlocking Software Using Automatic Theorem-Proving. Technical report, Logikkonsult NP AB, March 1997. Submitted to the World Congress on Railway Research 1997 (WCRR'97).
Love Ekenberg et al. Reference Manual, NP-Tools 2.2. Logikkonsult NP AB, October 1996. NPT-01-07-02 2.0.
J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd. Technical report, Department of Philosophy — Utrecht University, 1994.
John Harrison. The Stålmarck Method as a HOL Derived Rule. In Theorem Proving in Higher Order Logics, pages 221–234. TPHOLs'96, Springer Verlag, 1996.
Karl Meinke. Axiomatic Semantics and Automatic Verification of Statecharts. Technical report, Logikkonsult NP AB, April 1997.
Karl Meinke. Industrial Formal Methods: A Case Study in Public Transport Vehicles, February 1997. In Formal Methods Europe Tour 2, 1997. http://www.ifad.dk/projects/tour2.html.
Mårten Säflund and Gunnar Stålmarck. Modelling and Verifying Systems and Software in Propositional Logic. In Proceedings of IFAC/EWICS/SARS Symposium SAFECOMP '90, pages 31–36. Pergamon Press, 1990.
Gunnar Stålmarck. A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula, 1992. Swedish Patent No. 467 076 (approved 1992), U.S. Patent No. 5 276 897 (1994), European Patent No. 0403 454 (1995).
Gunnar Stålmarck. A Proof Theoretic Concept of Tautological Hardness. Unpublished manuscript, 1994.
Filip Widebäck. Stålmarck's Notion of n-saturation. Technical Report NP-K-FW-200, Logikkonsult NP AB, January 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Borälv, A. (1997). The industrial success of verification tools based on stålmarck's method. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_3
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive