Difference between revisions of "Public:Third Party Applications"

From CVC4
Jump to: navigation, search
(UpDwZmriQQsJQBbPfRH)
 
(46 intermediate revisions by 27 users not shown)
Line 1: Line 1:
As Robert notes, you can do:svn merge -c-Xwhere X is the single riivseon the change happened. the -c is to specify a single riivseon, and leading the riivseon with a '-' indicates it should be reversed.Ash, that's just wrong!  The whole point of riivseon control is that it should maintain a complete history of the changes to your code.  The metadata associated with each change (the log message, for example) is invaluable in explaining *why* something was done, or why it was wrong.  It's one of the major problems I have with most dvcs (git, darcs, etc) solutions; it becomes possible to lose riivseons and revise history.
+
*[http://multicore.doc.ic.ac.uk/tools/GPUVerify/ GPUVerify]: A tool for formal static analysis of GPU kernels written in OpenCL and CUDA. It can prove that kernels are free from defects such as data races and barrier divergence. It is built on top of the Boogie verification engine, using CVC4 as one of the available theorem provers.
 +
*[http://stardust.qc.com Stardust]: Refinement typechecker for an ML-like language that uses CVC4 as a backend for solving constraints arising from indexed types.
 +
*[https://github.com/cristina-serban/inductor Inductor]: a theorem prover for entailments between inductive definitions in first order and separation logics.
 +
 
 +
'''Please contact us and we'll add your applications here!'''

Latest revision as of 06:04, 25 September 2017

  • GPUVerify: A tool for formal static analysis of GPU kernels written in OpenCL and CUDA. It can prove that kernels are free from defects such as data races and barrier divergence. It is built on top of the Boogie verification engine, using CVC4 as one of the available theorem provers.
  • Stardust: Refinement typechecker for an ML-like language that uses CVC4 as a backend for solving constraints arising from indexed types.
  • Inductor: a theorem prover for entailments between inductive definitions in first order and separation logics.

Please contact us and we'll add your applications here!