
Isabelle/HOL
 Referenced in 1018 articles
[sw01569]
 mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

SPIN
 Referenced in 723 articles
[sw03455]
 that can be used for the formal verification of distributed software systems. The tool...

Isabelle
 Referenced in 698 articles
[sw00454]
 mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware...

ML
 Referenced in 522 articles
[sw01218]
 compiler writing, automated theorem proving and formal verification. (wikipedia...

NuSMV
 Referenced in 309 articles
[sw04131]
 verification tools, as a testbed for formal verification techniques, and applied to other research areas...

HOL Light
 Referenced in 307 articles
[sw06580]
 formalization of mathematics and industrial formal verification...

UNITY
 Referenced in 185 articles
[sw13461]
 formal assertions, permitting formal verification of the transition systems, and second into an executable program ... transition systems: one can specify properties formally that the model should obey and prove them...

seL4
 Referenced in 90 articles
[sw15222]
 seL4: formal verification of an OS kernel. Complete formal verification is the only known ... experience in performing the formal, machinechecked verification of the seL4 microkernel from an abstract ... used a unique design approach that fuses formal and operating systems techniques. To our knowledge...

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

KeY
 Referenced in 64 articles
[sw09969]
 integrate design, implementation, formal specification, and formal verification of objectoriented software as seamlessly...

MathSAT
 Referenced in 61 articles
[sw09449]
 explicitly designed for being used in formal verification, and thus provides functionalities which extend...

ABC
 Referenced in 40 articles
[sw12910]
 domain system for logic synthesis and formal verification of binary logic circuits appearing in synchronous ... synergy of sequential synthesis and sequential verification leads to improvements in both domains. This paper ... development, and illustrates its use in formal verification...

MathSAT5
 Referenced in 56 articles
[sw09569]
 tool for formal verification (and other applications). MathSAT5 is the latest version of the tool...

PVS
 Referenced in 629 articles
[sw03484]
 verification system: that is, a specification language integrated with support tools and a theorem prover ... stateoftheart in mechanized formal methods and to be sufficiently rugged that...

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

STeP
 Referenced in 36 articles
[sw17948]
 group to support the computeraided formal verification of reactive, realtime and hybrid systems...

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

Cadence SMV
 Referenced in 27 articles
[sw07795]
 possible input sequences. While formal verification is often equated with equivalence checking, model checking...

VIS
 Referenced in 17 articles
[sw40003]
 with Synthesis) is a system for formal verification, synthesis, and simulation of finite state systems ... interest has increased in methods of formal verification, such as language containment and temporal logic...

FoCs
 Referenced in 20 articles
[sw01591]
 FoCs  automatic generation of simulation checkers from formal specifications. For the foreseeable future, industrial hardware ... simulation and model checking in the design verification process. To date, these techniques are applied ... individual advantages of simulation and formal verification...