• ML

  • Referenced in 479 articles [sw01218]
  • Meta Language’) is a general-purpose functional programming language. It has roots in Lisp ... type safety – there is a formal proof that a well-typed ML program does...
  • JavaFAN

  • Referenced in 29 articles [sw01934]
  • framework, that can symbolically execute multithreaded programs, detect safety violations searching through an unbounded state...
  • Twelf

  • Referenced in 158 articles [sw06888]
  • prove properties of deductive systems such as programming languages and logics. Large research projects using ... proof-carrying-code system, and a type safety proof for Standard...
  • VeriFast

  • Referenced in 51 articles [sw07705]
  • VeriFast program verifier. This note describes a separation-logic-based approach ... specification and verification of safety properties of pointer-manipulating imperative programs. The programmer may declare...
  • ASTREE

  • Referenced in 106 articles [sw13704]
  • programming language. It has been applied with success to large embedded control-command safety critical...
  • BLAST

  • Referenced in 115 articles [sw02937]
  • reachability problem, i.e. whether a given program location can be reached from an entry point ... function) by a valid execution. Verification of safety properties may be reduced to the reachability...
  • CBMC

  • Referenced in 71 articles [sw09719]
  • Model Checker for ANSI-C and C++ programs. It also supports SystemC using Scoot ... allows verifying array bounds (buffer overflows), pointer safety, ex­cep­tions and user-specified ... performed by unwinding the loops in the program and passing the re­sul­ting equation...
  • Infer

  • Referenced in 9 articles [sw20862]
  • automatic program verifier for memory safety of C programs. Infer is a new automatic program ... tool aimed at proving memory safety of C programs. It attempts to build a compositional...
  • Ciao

  • Referenced in 46 articles [sw12088]
  • oriented programming styles. Its main design objectives are high expressive power, extensibility, safety, reliability...
  • MOPS

  • Referenced in 22 articles [sw10117]
  • identify rules of safe programming practice, encode them as safety properties, and verify whether these ... expensive, we have built a program analysis tool to automate this process. Our program analysis...
  • Esterel

  • Referenced in 154 articles [sw20012]
  • reactive kernel in a larger program that handles the interface and data manipulations ... tools that perform either bisimulation reduction or safety property checking. Esterel is now experimentally used...
  • TVLA

  • Referenced in 31 articles [sw09878]
  • programs manipulating linked data structures (singly and doubly linked lists), to prove safety properties...
  • CIL

  • Referenced in 32 articles [sw26691]
  • instruments C programs with run-time checks to ensure type safety. CIL has served...
  • TCAS

  • Referenced in 5 articles [sw21413]
  • TCAS software verification using constraint programming. Safety-critical software must be thoroughly verified before being ... Avoidance System) implementation must be verified against safety properties extracted from the anti-collision theory ... work, we explore the capabilities of Constraint Programming for automated software verification and testing ... over bounded integers extracted from computer programs and safety properties. An experience we made...
  • SLAyer

  • Referenced in 16 articles [sw09712]
  • SLAyer: Memory Safety for Systems-Level Code. SLAyer is a program analysis tool designed...
  • XDuce

  • Referenced in 53 articles [sw12436]
  • processing language. XDuce is a statically typed programming language for XML processing. Its basic data ... core, along with a proof of type safety...
  • CiaoPP

  • Referenced in 40 articles [sw12089]
  • time, etc. The abstract model of the program inferred by the analyzers is used ... abstraction-carrying code approach to mobile code safety...
  • Pavane

  • Referenced in 4 articles [sw29850]
  • capture abstract formal properties of programs (e.g. safety and progress) rather than operational details ... concurrent version of a popular artificial intelligence program provides a vehicle for demonstrating ... formal properties of the program, i.e. from those safety and progress assertions about the program...
  • Threader

  • Referenced in 13 articles [sw09938]
  • automates verification of safety and termination properties for multi-threaded C programs. The distinguishing feature...
  • Dylan

  • Referenced in 13 articles [sw26095]
  • application and systems programming. Dylan includes garbage collection, type-safety, error recovery, a module system...