List of Tools For Static Code Analysis - Formal Methods Tools

Formal Methods Tools

Tools that use a formal methods approach to static analysis (e.g., using static program assertions):

  • ECLAIR — Uses formal methods-based static code analysis techniques such as abstract interpretation and model checking combined with constraint satisfaction techniques to detect or prove the absence of certain run time errors in source code.
  • ESC/Java and ESC/Java2 — Based on Java Modeling Language, an enriched version of Java.
  • MALPAS; A formal methods tool that uses directed graphs and regular algebra to prove that software under analysis correctly meets its mathematical specification.
  • Polyspace — Uses abstract interpretation, a formal methods based technique, to detect and prove the absence of certain run time errors in source code for C/C++, and Ada
  • SofCheck Inspector — Statically determines and documents pre- and postconditions for Java methods; statically checks preconditions at all call sites; also supports Ada.
  • SPARK Toolset including the SPARK Examiner — Based on the SPARK language, a subset of Ada.

Read more about this topic:  List Of Tools For Static Code Analysis

Famous quotes containing the words formal, methods and/or tools:

    It is in the nature of allegory, as opposed to symbolism, to beg the question of absolute reality. The allegorist avails himself of a formal correspondence between “ideas” and “things,” both of which he assumes as given; he need not inquire whether either sphere is “real” or whether, in the final analysis, reality consists in their interaction.
    Charles, Jr. Feidelson, U.S. educator, critic. Symbolism and American Literature, ch. 1, University of Chicago Press (1953)

    How can you tell if you discipline effectively? Ask yourself if your disciplinary methods generally produce lasting results in a manner you find acceptable. Whether your philosophy is democratic or autocratic, whatever techniques you use—reasoning, a “star” chart, time-outs, or spanking—if it doesn’t work, it’s not effective.
    Stanley Turecki (20th century)

    The study of tools as well as of books should have a place in the public schools. Tools, machinery, and the implements of the farm should be made familiar to every boy, and suitable industrial education should be furnished for every girl.
    Rutherford Birchard Hayes (1822–1893)