• SPIN

  • Referenced in 723 articles [sw03455]
  • used for the formal verification of distributed software systems. The tool was developed at Bell...
  • Isabelle/HOL

  • Referenced in 1018 articles [sw01569]
  • particular formal verification, which includes proving the correctness of computer hardware or software and proving...
  • Isabelle

  • Referenced in 698 articles [sw00454]
  • particular formal verification, which includes proving the correctness of computer hardware or software and proving...
  • ETPS

  • Referenced in 160 articles [sw06302]
  • software verification, partial automation of various mathematical activities, promoting development of formal theories...
  • KeY

  • Referenced in 64 articles [sw09969]
  • software development tool that aims to integrate design, implementation, formal specification, and formal verification...
  • PolyBoRi

  • Referenced in 48 articles [sw00723]
  • growing importance of formal hardware and software verification based on Boolean expressions, which suffer-besides...
  • Isabelle/ZF

  • Referenced in 63 articles [sw04973]
  • particular formal verification, which includes proving the correctness of computer hardware or software and proving ... properties of computer languages and protocols. Isabelle/ZF formalizes the greater part of elementary set theory...
  • TPS

  • Referenced in 73 articles [sw00973]
  • software verification, partial automation of various mathematical activities, promoting development of formal theories...
  • CompCert

  • Referenced in 49 articles [sw09737]
  • investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers ... guarantees that can be obtained by applying formal methods to source programs. The main result...
  • Why3

  • Referenced in 134 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 ... user a possibility to easily reuse Why3 formalizations or to add support...
  • MAYA

  • Referenced in 26 articles [sw03423]
  • size software is an error-prone and therefore an evolutionary process. Verifying formal specifications usually ... specification which always endangers the verification work already done. In this paper we describe ... structure of the specification, and maintains the verification work already done when changing the specification ... various (structured) specification languages to formalize the software development. Moreover, Maya allows the integration...
  • PPL

  • Referenced in 101 articles [sw05357]
  • systems for the analysis and verification of hardware and software components. Current applications span imperative ... thus played an important role in the formal methods community and several critical tasks rely...
  • WoLFram

  • Referenced in 15 articles [sw02075]
  • formal verification and its application. A framework that automatically transforms PLC software to SystemC ... WoLFram is successfully applied to the verification of PLC programs. Equivalence checking and property checking ... software. It is shown, that modern SAT solvers can formally verify PLC programs within...
  • IMITATOR

  • Referenced in 29 articles [sw00439]
  • IMITATOR is a software tool for parametric verification and robustness analysis of real-time systems ... with parameters. It relies on the formalism of networks of parametric timed automata, augmented with...
  • NetKAT

  • Referenced in 22 articles [sw16269]
  • NetKAT -- a formal system for the verification of networks. This paper presents a survey ... work in the development of NetKAT, a formal system for reasoning about packet switching networks ... role in the emerging area of software-defined networking...
  • LOTOSphere

  • Referenced in 9 articles [sw14748]
  • vehicle for efficient, yet formally based industrial software specification, design, verification, implementation and testing. LOTOSphere ... each treat an important part of the software development life cycle using LOTOS. This ... comprehensive treatment of the use of these formal description techniques in a software engineering environment...
  • FShell

  • Referenced in 8 articles [sw14481]
  • performance requirements for software testing are quite different from formal verification. Our tool FShell provides ... scripting language. More than a frontend for software model checkers, FShell is designed...
  • KRATOS

  • Referenced in 8 articles [sw07808]
  • KRATOS: A software model checker for SystemC. he growing popularity of SystemC has attracted research ... formal verification of SystemC designs. In this paper we present Kratos, a software model checker...
  • SCADE

  • Referenced in 20 articles [sw00829]
  • Environment for critical embedded software. With native integration of the formally-defined Scade language, SCADE ... spanning requirements management, model-based design, simulation, verification, qualifiable/certified code generation, and interoperability with other...
  • Gappa

  • Referenced in 18 articles [sw04885]
  • tool intended to help verifying and formally proving properties on numerical programs dealing with floating ... backend prover for the Why software verification plateform or as an automatic tactic...