• ML

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

  • Referenced in 145 articles [sw06302]
  • theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting development...
  • Why3

  • Referenced in 113 articles [sw04438]
  • Why3 is a platform for deductive program verification. It provides a rich language for specification ... external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with ... automated extraction mechanism. WhyML is also used as an intermediate language for the verification...
  • TPS

  • Referenced in 67 articles [sw00973]
  • theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting development...
  • CoLoR

  • Referenced in 36 articles [sw09806]
  • relations and its application to the automated verifications of termination certificates. Termination is an important ... also present its application to the automated verification of termination certificates, as produced by termination...
  • VerICS

  • Referenced in 31 articles [sw02011]
  • VerICS) is our original tool for automated verification of Timed Automata and protocols written ... part of the research project Automated Verification of Time Dependent Systems held in the Institute...
  • KeYmaera

  • Referenced in 32 articles [sw03709]
  • hybrid systems. KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real ... automated and interactive theorem prover for a natural specification and verification logic for hybrid systems ... program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free...
  • HIP

  • Referenced in 20 articles [sw09786]
  • separation logic based automated verification system for a simple imperative language, able to modularly verify...
  • Threader

  • Referenced in 13 articles [sw09938]
  • programs. Threader is a tool that automates verification of safety and termination properties for multi...
  • Reveal

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

  • Referenced in 11 articles [sw12934]
  • multi-player games, which supports modelling, automated verification and strategy synthesis for probabilistic systems with...
  • Predator

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

  • Referenced in 22 articles [sw09709]
  • various existing automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML ... automated extraction mechanism. WhyML is also used as an intermediate language for the verification...
  • visualSTATE

  • Referenced in 9 articles [sw07481]
  • Verification of large state/event systems using compositionality and dependency analysis A state/event model ... state/event models. It makes possible automated verification of large industrial designs with...
  • HSF

  • Referenced in 9 articles [sw09937]
  • Clauses. SF is a framework that automates verification of programs. HSF(C) is the instantiation...
  • SATIRE

  • Referenced in 36 articles [sw04648]
  • particularly suited to verification and optimization problems in electronic design automation. SATIRE builds...
  • F*

  • Referenced in 16 articles [sw27563]
  • effects aimed at program verification. It puts together the automation of an SMT-backed deductive...
  • scyther

  • Referenced in 16 articles [sw09467]
  • scyther tool: verification, falsification, and analysis of security protocols. With the rise of the Internet ... approach so far has been automated falsification or verification of such protocols with state...
  • Verics

  • Referenced in 6 articles [sw09464]
  • paper presents a new tool for automated verification of Timed Automata as well as protocols...
  • CITP

  • Referenced in 6 articles [sw25269]
  • default proof strategy for the automated verification of observational transitional systems (OTS), but the area...