• ML

  • Referenced in 524 articles [sw01218]
  • compiler writing, automated theorem proving and formal verification. (wikipedia...
  • ETPS

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

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

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

  • Referenced in 136 articles [sw04438]
  • automated extraction mechanism. WhyML is also used as an intermediate language for the verification ... user a possibility to easily reuse Why3 formalizations or to add support...
  • PSync

  • Referenced in 5 articles [sw17450]
  • fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding...
  • CoLoR

  • Referenced in 38 articles [sw09806]
  • relations and its application to the automated verifications of termination certificates. Termination is an important ... subject of research in the Turing-complete formalism of term rewriting. Over the years, many ... also present its application to the automated verification of termination certificates, as produced by termination...
  • ESC4

  • Referenced in 2 articles [sw07219]
  • Static Checking (ESC) is a fully automated formal verification technique. Verification in ESC is achieved...
  • scyther

  • Referenced in 16 articles [sw09467]
  • scyther tool: verification, falsification, and analysis of security protocols. With the rise of the Internet ... deployment. This has driven the research in formal analysis of security protocols. Unfortunately, there ... efficient protocols, and work on concise formal logics that might allow one to easily prove ... formal model, is still ongoing. The most effective approach so far has been automated falsification...
  • SAD

  • Referenced in 15 articles [sw09796]
  • System for automated deduction (SAD): A tool for proof verification. In this paper a proof ... deals with mathematical texts that are formalized in the ForTheL language (a brief description...
  • verifier

  • Referenced in 3 articles [sw12878]
  • This paper presents a formal framework for semi-automated verification of security proofs of quantum...
  • EVE

  • Referenced in 4 articles [sw31990]
  • Verification Environment) is a formal verification tool for the automated analysis of temporal equilibrium properties...
  • Reveal

  • Referenced in 22 articles [sw00801]
  • describe the Reveal formal functional verification system and its application to four representative hardware test ... experience with this system, we believe that automating the verification for a useful class...
  • VeriFun

  • Referenced in 10 articles [sw22187]
  • system for teaching Automated Reasoning, Semantics, Verification and similar subjects and has been used ... beginner courses about Formal Methods as well as in practical courses about Program Verification...
  • CD++

  • Referenced in 8 articles [sw00112]
  • modeling and simulation based on the DEVS formalism are presented. The tool is built ... automated fashion, simplifying the construction of new models and easing their verification ... this formal approach has allowed the development of safe and cost-effective simulations, significantly reducing...
  • MOPS

  • Referenced in 23 articles [sw10117]
  • security properties of software. We describe a formal approach for finding bugs in security-relevant ... manual verification is too expensive, we have built a program analysis tool to automate this...
  • Smt-Switch

  • Referenced in 2 articles [sw41581]
  • areas such as automated reasoning, planning, and formal verification. It defines an abstract interface, which...
  • Ivy

  • Referenced in 10 articles [sw41668]
  • infinite-state systems via three modes: deductive verification using an SMT solver, abstraction and model ... using natural deduction. It supports light-weight formal methods via compositional specification-based testing ... code. It is designed to support decidable automated reasoning, to improve proof stability ... counterexamples, automatically audits proofs for decidability of verification conditions, and provides modular hiding of theories...
  • LegalRuleML

  • Referenced in 6 articles [sw30411]
  • reasoning with LegalRuleML. In order to automate verification process, regulatory rules written in natural language ... understand. However, none of the existing formalisms can fully represent the elements that appear ... legal norms. For instance, most of these formalisms do not provide features to capture ... effects, which is an important aspect in automated compliance checking. This paper presents an approach...
  • Truth/SLC

  • Referenced in 8 articles [sw01623]
  • correctness of their implementation. Formal specification and verification methods are therefore becoming more and more ... view of the inherent complexity of formal methods it is desirable to provide the user ... There is one particularly successful automated approach to verification, called model checking, in which...