• SIMPLIFY

  • Referenced in 135 articles [sw04976]
  • Extended static checking. This paper provides an overview of Extended Static Checking ... have implemented and experimented with two Extended Static Checkers, one for Modula-3, and another ... increase software productivity by providing practical static checking tools for programmers. In general, static checking...
  • ESC/Java

  • Referenced in 133 articles [sw07217]
  • Extended Static Checker for Java version 2 (ESC/Java2) is a programming tool that attempts ... errors in JML-annotated Java programs by static analysis of the program code ... control the amount and kinds of checking that ESC/Java2 performs by annotating their programs with...
  • Calysto

  • Referenced in 7 articles [sw31588]
  • Calysto: scalable and precise extended static checking. Automatically detecting bugs in programs has been ... code bases. This paper presents the Calysto static checker, which achieves an unprecedented combination ... precision and scalability in a completely automatic extended static checker. Calysto is interprocedurally path-sensitive...
  • Omnibus

  • Referenced in 3 articles [sw04600]
  • provided for run-time assertion checking, extended static checking and full formal verification. The language...
  • ESC4

  • Referenced in 2 articles [sw07219]
  • Faster and more complete extended static checking for the Java modeling language Extended Static Checking ... beyond the ability of traditional extended static checking tools to verify. Not being able...
  • Sage

  • Referenced in 3 articles [sw30073]
  • decidable, Sage uses hybrid type checking, which extends static type checking with dynamic contract checking...
  • CCured

  • Referenced in 24 articles [sw10057]
  • that combines type inference and run-time checking to make existing C programs type safe ... describe the CCured type system, which extends that of C by separating pointer types according ... verified statically to be type safe, and pointers whose safety must be checked...
  • ETCH

  • Referenced in 3 articles [sw07636]
  • only limited type checking. In particular, SPIN does not guarantee static detection of mismatched message ... partially specified in Promela. ETCH extends the type checking capabilities of SPIN, using type reconstruction ... recover missing channel type information, allowing strong static type checking. Thus ETCH can detect type...
  • VDMTools

  • Referenced in 2 articles [sw18244]
  • oriented structuring and concurrency, and a version extending VDM++ with features for modeling and analysing ... real-time systems. VDMTools provides extensive static semantics checking, automatic code generation, round-trip mapping...
  • Gopherlyzer

  • Referenced in 2 articles [sw23206]
  • Mini-Go. We consider the problem of static deadlock detection for programs ... channel communications. In our analysis, regular expressions extended with a fork operator capture the communication ... programs, we develop automata-based methods to check for deadlock- freedom. The approach is implemented...
  • BER MetaOCaml

  • Referenced in 3 articles [sw09552]
  • metaocaml. MetaOCaml is a superset of OCaml extending it with the data type for program ... specializations of high-performance computational kernels. By statically ensuring that the generated code compiles ... code, BER MetaOCaml adds a scope extrusion check superseding environment classifiers. Attempting to build code...
  • Hazelnut

  • Referenced in 2 articles [sw22659]
  • small bidirectionally typed lambda calculus extended with holes and a cursor. Hazelnut goes one step ... well-formedness: its edit actions operate over statically meaningful incomplete terms. Na”{i}vely, this ... hole. This meaningfully defers the type consistency check until the term inside the hole ... assistant, serves as a guide when we extend the calculus to include binary sum types...
  • ACL2

  • Referenced in 275 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1758 articles [sw00161]
  • Coq is a formal proof management system. It...
  • GAP

  • Referenced in 2735 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • GreatSPN

  • Referenced in 57 articles [sw00384]
  • GreatSPN2.0 is a software package for the modeling...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • Boogie is a program verification condition generator for...
  • Isabelle

  • Referenced in 601 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Magma

  • Referenced in 2747 articles [sw00540]
  • Computer algebra system (CAS). Magma is a large...
  • Maple

  • Referenced in 4956 articles [sw00545]
  • The result of over 30 years of cutting...