Advertisement

The industrial success of verification tools based on stålmarck's method

  • Arne Borälv
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

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.

Keywords

Safety Property Industrial Problem Verification Tool Proof Checker Axiomatic Semantic 
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

  1. [BÅ95]
    Arne Borälv and Herman Ågren. Feasibility Study SVT. Technical Report U-95002, Logikkonsult NP AB, 1995. Internally published at Logikkonsult.Google Scholar
  2. [Bol96]
    Hans Bolinder. LSA 1.0. Technical Report NPT-01-07-0-3, Issue 2 Rev 1, Logikkonsult NP AB, 1996.Google Scholar
  3. [Bor97]
    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).Google Scholar
  4. [E+96]
    Love Ekenberg et al. Reference Manual, NP-Tools 2.2. Logikkonsult NP AB, October 1996. NPT-01-07-02 2.0.Google Scholar
  5. [GKvV94]
    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.Google Scholar
  6. [Har96]
    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.Google Scholar
  7. [Mei97a]
    Karl Meinke. Axiomatic Semantics and Automatic Verification of Statecharts. Technical report, Logikkonsult NP AB, April 1997.Google Scholar
  8. [Mei97b]
    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.Google Scholar
  9. [SS90]
    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.Google Scholar
  10. [Stå92]
    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).Google Scholar
  11. [Stå94]
    Gunnar Stålmarck. A Proof Theoretic Concept of Tautological Hardness. Unpublished manuscript, 1994.Google Scholar
  12. [Wid96]
    Filip Widebäck. Stålmarck's Notion of n-saturation. Technical Report NP-K-FW-200, Logikkonsult NP AB, January 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Arne Borälv
    • 1
  1. 1.Logikkonsult NP ABStockholmSweden

Personalised recommendations