• ML

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

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

  • Referenced in 131 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 71 articles [sw00973]
  • theorem proving include hardware and software verification, partial automation of various mathematical activities, promoting development...
  • CoLoR

  • Referenced in 38 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 33 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 41 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 27 articles [sw09786]
  • separation logic based automated verification system for a simple imperative language, able to modularly verify...
  • PRISM-games

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

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

  • Referenced in 20 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...
  • Predator

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

  • Referenced in 25 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...
  • F*

  • Referenced in 20 articles [sw27563]
  • effects aimed at program verification. It puts together the automation of an SMT-backed deductive...
  • 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 38 articles [sw04648]
  • particularly suited to verification and optimization problems in electronic design automation. SATIRE builds...
  • EAGLE

  • Referenced in 8 articles [sw31989]
  • tool for the automated verification of Nash equilibria in concurrent games. Reactive Modules...
  • 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...
  • CITP

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