Difference between revisions of "Public:Third Party Applications"

From CVC4
Jump to: navigation, search
Line 1: Line 1:
 
*[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.
 
*[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.
 +
*[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.
  
 
'''Please contact us and we'll add your applications here!'''
 
'''Please contact us and we'll add your applications here!'''

Revision as of 13:37, 11 July 2013

  • Stardust: Refinement typechecker for an ML-like language that uses CVC4 as a backend for solving constraints arising from indexed types.
  • 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.

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