• CakeML

  • Referenced in 53 articles [sw08799]
  • more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself...
  • Checkfence

  • Referenced in 19 articles [sw09939]
  • CheckFence is a SAT-based formal verification tool that analyzes C code implementing concurrent data ... interleavings and reorderings. CheckFence does not require formal specifications or annotations, but mines a specification...
  • Predator

  • Referenced in 18 articles [sw07396]
  • Predator is a tool for automated formal verification of sequential C programs operating with pointers...
  • PolyBoRi

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

  • Referenced in 16 articles [sw09952]
  • code validation tool (CVT). Automatic verification of a compilation process. We describe CVT -- a fully ... viable alternative to a full formal verification of the code-generator program...
  • WoLFram

  • Referenced in 15 articles [sw02075]
  • WoLFram -- a word level framework for formal verification and its application. A framework that automatically ... WoLFram is successfully applied to the verification of PLC programs. Equivalence checking and property checking ... shown, that modern SAT solvers can formally verify PLC programs within a short run time...
  • CORA

  • Referenced in 15 articles [sw25659]
  • collection of MATLAB classes for the formal verification of cyber-physical systems using reachability analysis...
  • Reveal

  • Referenced in 21 articles [sw00801]
  • describe the Reveal formal functional verification system and its application to four representative hardware test...
  • Lava

  • Referenced in 13 articles [sw28643]
  • standard circuit analyses such as simulation, formal verification and the generation of code...
  • ISP

  • Referenced in 12 articles [sw04895]
  • Order”) is a tool for the formal verification of MPI(Message Passing Interface) programs developed...
  • TPS

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

  • Referenced in 26 articles [sw03423]
  • prone and therefore an evolutionary process. Verifying formal specifications usually reveals hidden errors causing ... verification work already done. In this paper we describe the system Maya which maintains formal ... developments. The Maya-system supports an evolutionary formal development since it allows users to specify ... structured manner, incorporates a uniform mechanism for verification in-the-large to exploit the structure...
  • Java-MaC

  • Referenced in 11 articles [sw20000]
  • time. MaC bridges the gap between formal verification, which ensures the correctness of a design ... implementation, and testing, which does not provide formal guarantees about the correctness of the system...
  • ChC 3

  • Referenced in 11 articles [sw09781]
  • correctness of many important formal verification tasks, including search, LTL model checking, and the development...
  • Exp.Open

  • Referenced in 10 articles [sw07702]
  • Methods. It is desirable to integrate formal verification techniques applicable to different languages. We present...
  • ANNA

  • Referenced in 10 articles [sw36323]
  • include not only testing, debugging and formal verification of a finished program, but also specification...
  • Why3

  • Referenced in 135 articles [sw04438]
  • used as an intermediate language for the verification of C, Java, or Ada programs. Why3 ... user a possibility to easily reuse Why3 formalizations or to add support...
  • NetKAT

  • Referenced in 23 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...
  • TRX

  • Referenced in 9 articles [sw08800]
  • attention has been devoted to its formal verification. In this paper, we present...
  • Rebeca

  • Referenced in 9 articles [sw09422]
  • effort to bridge the gap between formal verification approaches and real applications. Rebeca is supported...