Yahoda

Filtering query not set.

Found 68 matching records.

Purpose
<AND>

Specific Features
<AND>

Graphical Interface
<AND>

Availability
<OR>

Platforms
<OR>

Contact
<AND>

Name

Equiv. Checking

Theorem Proving

Free Under Cond.

Yes

Yes

Yes

Yes

MacOS X; any with OCaml compiler

http://lampwww.epfl.ch/~sbriais/abc/abc.html

mailto:sebastien.briais(a)epfl.ch

Yes

Yes

Yes

Yes

http://www.cs.utexas.edu/users/moore/acl2/

mailto:kaufmann(a)cs.utexas.edu

Yes

Yes

Yes

Yes

Yes

Yes

http://alpina.unige.ch

mailto:didier.buchs(a)unige.ch

Yes

Yes

Yes

Yes

Yes

http://apmc.berbiqui.org

mailto:syp(a)lrde.epita.fr

Yes

Yes

Yes

Yes

http://altarica.labri.fr/wiki/tools:arc

mailto:altarica-admin.labri(a)listes.u-bordeaux1.fr

Yes

Yes

Yes

Yes

http://www.atelierb.societe.com/index.html

mailto:atelierb(a)clearsy.com

Yes

Yes

Yes

Yes

Yes

Yes

http://bandera.projects.cis.ksu.edu/

mailto:bandera(a)cis.ksu.edu

Yes

Yes

Yes

Yes

http://www.eecs.berkeley.edu/~tah/blast

mailto:tah(a)eecs.berkeley.edu

Yes

Yes

Yes

Yes

Yes

Yes

http://www-cad.eecs.berkeley.edu/~kenmcmil/smv

mailto:mcmillan(a)cadence.com

Yes

Yes

Yes

Yes

http://www-users.cs.york.ac.uk/~ian/cadiz/

mailto:ian(a)cs.york.ac.uk

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

macOS, Linux, Solaris, Windows

http://www.inrialpes.fr/vasy/cadp

mailto:cadp(a)inrialpes.fr

Yes

Yes

Yes

Yes

http://www.cs.cmu.edu/~modelcheck/cbmc/

mailto:kroening(a)handshake.de

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.cs.sunysb.edu/~cwb/

mailto:cwb-nc(a)cs.sunysb.edu

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.dbrover.com

mailto:ask(a)time-rover.com

Yes

Yes

Yes

http://anna.fi.muni.cz/divine

mailto:divine(a)fi.muni.cz

Yes

Yes

Yes

Yes

Yes

Any platform supporting ANSI C++ / gcc. The XML parser features can be disabled.

http://dre.sourceforge.net

gabe at uci dot edu

Yes

Yes

Yes

Yes

Yes

Any with SML/NJ compiler

http://www.lfcs.ed.ac.uk/cwb

mailto:cwb-users(a)inf.ed.ac.uk

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://ls5-www.cs.uni-dortmund.de/~peter/Expander2/Expander2.html

mailto:peter.padawitz(a)udo.edu

Yes

Yes

Yes

Yes

Yes

Yes

http://www-sop.inria.fr/meije/verification/

mailto:fc2team(a)sophia.inria.fr

Yes

Yes

Yes

Yes

Yes

http://www.fsel.com/

mailto:enquiries(a)fsel.com

Yes

Yes

Yes

Yes

Yes

Yes

http://jabc.de/gear

Yes

Yes

Yes

Yes

http://hsolver.sourceforge.net

mailto:stefan.ratschan(a)cs.cas.cz

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.eecs.berkeley.edu/~tah/hytech

mailto:hytech(a)eecs.berkeley.edu

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://arpont.imag.fr/~async/IF/

mailto:Marius.Bozga(a)imag.fr

Yes

Yes

Yes

Yes

http://www.informatik.hu-berlin.de/lehrstuehle/automaten/ina/

mailto:starke(a)informatik.hu-berlin.de roch@informatik.hu-berlin.de

Yes

Yes

Yes

Yes

Anything that supports Java

http://theory.lcs.mit.edu/tds/ioa.html

mailto:ioa(a)theory.lcs.mit.edu

Yes

Yes

Yes

Yes

Mac OS X

http://isabelle.in.tum.de/

mailto:isabelle-enquiries(a)cl.cam.ac.uk

Yes

Yes

Yes

Yes

http://javapathfinder.sourceforge.net/

mailto:pcmehlitz(a)email.arc.nasa.gov

Yes

Yes

Yes

Yes

Yes

http://www.key-project.org

mailto:support(a)key-project.org

Yes

Yes

Yes

Yes

Yes

Yes

http://www-verimag.imag.fr/TEMPORISE/kronos

Yes

Yes

Yes

Yes

http://pag.lcs.mit.edu/~garland/LP/overview.html

mailto:garland(a)lcs.mit.edu

Yes

Yes

Yes

Yes

Yes

Yes

http://www.doc.ic.ac.uk/~jnm/book/

mailto:jnm(a)doc.ic.ac.uk

Yes

Yes

Yes

Yes

Yes

Yes

http://www.cwi.nl/~mcrl/mutool.html

mailto:Bert.Lisser(a)cwi.nl

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Linux/Mac OS X/FreeBSD/Solaris with a recent version of gcc 4

http://www.mcrl2.org

mailto:info(a)mcrl2.org

Yes

Yes

Yes

Yes

Yes

Mac OS X, Cygwin

http://metaprl.org/

mailto:metaprl(a)metaprl.org

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.eecs.berkeley.edu/~mocha

mailto:mocha(a)eecs.berkeley.edu

Yes

Yes

Yes

Yes

http://www.fmi.uni-stuttgart.de/szs/tools/moped/

mailto:schwoosn(a)fmi.uni-stuttgart.de

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Mac OS X

http://www.mrmc-tool.org

mailto:mrmc-users(a)lists.rwth-aachen.de

Yes

Yes

Yes

http://fmv.jku.at/mucke

Yes

Yes

Yes

Yes

Any with SML/NJ compiler

http://www.it.uu.se/research/group/mobility/mwb

mailto:mwb-bugs(a)it.uu.se

Yes

Yes

Yes

Yes

Yes

http://nusmv.irst.itc.it/

mailto:nusmv(a)irst.itc.it

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Linux, MAC OS

http://www.comp.nus.edu.sg/~pat/

mailto:pat(a)comp.nus.edu.sg

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://parsys.informatik.uni-oldenburg.de/~pep

mailto:pep(a)informatik.uni-oldenburg.de

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Mac OS X

http://www.prismmodelchecker.org/

mailto:david.parker(a)comlab.ox.ac.uk

Yes

Yes

Yes

Yes

http://www.tcs.hut.fi/Software/prod/

mailto:kimmo.varpaaniemi(a)kolumbus.fi

Yes

Yes

Yes

Yes

http://www.lemma-one.com/ProofPower/index/index.html

mailto:rda(a)lemma-one.com

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://pvs.csl.sri.com

mailto:pvs-sri(a)csl.sri.com

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Linux

http://www.reactive-systems.com

mailto:info(a)reactive-systems.com

Yes

Yes

Yes

Yes

Yes

Yes

http://www.cs.ccu.edu.tw/~pahsiung/sgm/

mailto:pahsiung(a)cs.ccu.edu.tw

Yes

Yes

Yes

Yes

Yes

Yes

any platform with Internet Explorer or Gecko (Mozilla) compatible

http://anna.fi.muni.cz/~xsimece1/mc/interface.html

xsimece1 (at) fi.muni.cz

Yes

Yes

Yes

Yes

Yes

http://netlib.bell-labs.com/netlib/spin/

mailto:gerard(a)bell-labs.com

Yes

Yes

Yes

Yes

Yes

Any platform supporting Java.

http://statestep.com

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www-step.stanford.edu/

mailto:step-request(a)cs.stanford.edu

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Mac OS X

http://www.tapaal.net

mailto:tapaal(a)cs.aau.dk

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Any platform with Java Virtual Machine 1.5.0 or above

http://rap.dsi.unifi.it/tapas/en/index.htm

mailto:tapas(a)rap.dsi.unifi.it

Yes

Yes

Yes

Java based

http://www.time-rover.com

mailto:ask(a)time-rover.com

Yes

Yes

Yes

http://www.fmi.uni-stuttgart.de/szs/tools/mckit/

mailto:mckit(a)honolulu.informatik.uni-stuttgart.de

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.timestool.com

mailto:times(a)timestool.com

Yes

Yes

Yes

Yes

http://gtps.math.cmu.edu/tps.html

mailto:Andrews(a)cmu.edu

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.cs.aau.dk/~marius/tron

mailto:marius(a)cs.aau.dk

Yes

Yes

Yes

http://www-i2.informatik.rwth-aachen.de/Forschung/MCS/Truth/

mailto: leucker(a)i2.informatik.rwth-aachen.de

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.sti.uniurb.it/bernardo/twotowers/

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.uppaal.com

mailto:team(a)uppaal.com

Yes

Yes

Yes

Yes

Yes

http://www.bell-labs.com/projects/verisoft

mailto:god(a)bell-labs.com

Yes

Yes

Yes

http://vlsi.colorado.edu/~vis

mailto:vis-users(a)colorado.edu

Yes

Yes

Yes

Yes

Yes

Yes

Yes

Yes

http://www.dfki.de/dmas/fu_m_pro.htm

mailto:rock(a)dfki.de

Yes

Yes

Yes

Yes

Yes

http://www.tempastic.org/ymer/

mailto:hlsyounes(a)gmail.com

Yes

Yes

Yes

Yes

Yes

Yes

http://www-i11.informatik.rwth-aachen.de/index.php?id=mc_square

mailto:mc_square(a)embedded.rwth-aachen.de


Last Modification: 13. 9. 2012 11:40:32	Visits: 4053413