• Cogent

  • Referenced in 14 articles [sw01300]
  • proving for program verification. Many symbolic software verification engines such as Slam and ESC/Java rely...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • correctness of models of hardware and software systems. UCLID can be used to model ... level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based verification ... explored to-date include microprocessor design verification, analyzing software for security exploits, and verifying distributed...
  • CSIsat

  • Referenced in 15 articles [sw11407]
  • tool on benchmarks from software verification. Binaries and the source code of CSIsat are publicly...
  • Lambda-Clam

  • Referenced in 24 articles [sw19614]
  • outlined, in particular the synthesis and verification of software and hardware systems...
  • SNOOPY

  • Referenced in 34 articles [sw04386]
  • verification of technical systems, especially software-based systems, as well as for the validation...
  • fc2tools

  • Referenced in 11 articles [sw12386]
  • fc2tools set: a toolset for the verification of concurrent systems. The FC2Tools package, together with ... forerunner amongst softwares dealing with model-based, automatic verification of distributed communicating systems ... format for easy interface with other verification softwares...
  • SYMBA

  • Referenced in 12 articles [sw08528]
  • created numerous uses for them in software verification, program synthesis, functional programming, refinement types...
  • IMITATOR

  • Referenced in 29 articles [sw00439]
  • IMITATOR is a software tool for parametric verification and robustness analysis of real-time systems...
  • Isabelle/ZF

  • Referenced in 63 articles [sw04973]
  • particular formal verification, which includes proving the correctness of computer hardware or software and proving...
  • SMACK

  • Referenced in 9 articles [sw23311]
  • SMACK is both a modular software verification toolchain and a self-contained software verifier ... depth; it contains experimental support for unbounded verification as well. Under the hood, SMACK...
  • PeRIPLO

  • Referenced in 7 articles [sw07896]
  • producing effective interpolants in SAT-based software verification Propositional interpolation is widely used ... efficient SAT-based symbolic model checking. Different verification applications exploit interpolants for different purposes ... framework in two software bounded model checking applications: verification of a given source code incrementally ... with respect to various properties, and verification of software upgrades with respect to a fixed...
  • OpenJML

  • Referenced in 6 articles [sw19841]
  • OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. OpenJML is a tool ... many advances in specification-based software verification. The implementation demonstrates the value of integrating specification ... several college-level courses on software specification and verification and for small-scale studies...
  • CompCert

  • Referenced in 48 articles [sw09737]
  • investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers...
  • Bogor

  • Referenced in 36 articles [sw06858]
  • Building your own software model checker using the Bogor extensible model checking framework Model checking ... technology for verification and debugging in hardware and more recently in software domains. We believe...
  • Zap

  • Referenced in 8 articles [sw06823]
  • component that many software verification and program analysis tools rely on. However, the basic interface...
  • SAT competition

  • Referenced in 8 articles [sw04623]
  • their area (planning, hardware or software verification, etc.) to submit benchmarks to be used...
  • eVolCheck

  • Referenced in 6 articles [sw09711]
  • practical for software developers, the software verification tools should be able to cope with changes ... tool, eVolCheck, that focuses on incremental verification of software as it evolves. During the software ... function summaries are used to localize verification of an upgrade to analysis of the modified...
  • TCAS

  • Referenced in 5 articles [sw21413]
  • TCAS software verification using constraint programming. Safety-critical software must be thoroughly verified before being ... theory that regulates the controlled airspace. This verification step is currently realized with manual code ... capabilities of Constraint Programming for automated software verification and testing. We built a dedicated constraint...
  • Why3

  • Referenced in 132 articles [sw04438]
  • used as an intermediate language for the verification of C, Java, or Ada programs. Why3 ... allowing to use Why3 as a software library. An important emphasis is put on modularity...
  • Ultimate Automizer

  • Referenced in 4 articles [sw07407]
  • contribution) Ultimate automizer is an automatic software verification tool for C programs. This tool ... automata-theoretic approach to software verification. The implemented algorithm uses nested interpolants in its interprocedural...