summaryrefslogtreecommitdiff
path: root/Source/GPUVerify
Commit message (Expand)AuthorAge
* GPUVerify: if one input file is supplied, choose output file name more intell...Gravatar Peter Collingbourne2012-06-08
* GPUVerify: fix line endingsGravatar Peter Collingbourne2012-06-08
* GPUVerify: have StripThreadIdentifiers deal properly with identifiers contain...Gravatar Peter Collingbourne2012-06-07
* GPUVerify: block predicator: use the name '_P' for the procedure predicate fo...Gravatar Peter Collingbourne2012-06-07
* GPUVerify: re-introduce the non-divergence check in unstructured modeGravatar Peter Collingbourne2012-06-07
* GPUVerify: emit assumes for backedgesGravatar Peter Collingbourne2012-06-07
* GPUVerify: refactor candidate invariant generators and analyses to use regionsGravatar Peter Collingbourne2012-06-07
* GPUVerify: recognise offsets in forms other than that produced by the old fro...Gravatar Peter Collingbourne2012-06-01
* GPUVerify: have dualiser reuse blocksGravatar Peter Collingbourne2012-06-07
* GPUVerify: add newly created barrier procedures to resolution contextGravatar Peter Collingbourne2012-06-07
* GPUVerify: fix bug which caused us to log accesses at the end of the block, r...Gravatar Peter Collingbourne2012-06-06
* GPUVerify: use Concat instead of PureCollections.Sequence.operator+Gravatar Peter Collingbourne2012-05-31
* GPUVerify: resolve barrier implementation in unstructured modeGravatar Peter Collingbourne2012-05-31
* GPUVerify: use a Formal for procedure predicatesGravatar Peter Collingbourne2012-05-31
* GPUVerify: teach analyses, dualiser and race instrumenter about assigns with ...Gravatar Peter Collingbourne2012-05-31
* GPUVerify: implement assume stealing in block predicatorGravatar Peter Collingbourne2012-05-30
* GPUVerify: disable barrier divergence check in unstructured mode for nowGravatar Peter Collingbourne2012-05-30
* GPUVerify: have shared state abstraction, race instrumenter reuse blocksGravatar Peter Collingbourne2012-05-30
* GPUVerify: factor shared state abstraction for unstructured blocksGravatar Peter Collingbourne2012-05-29
* GPUVerify: factor the race instrumenter to handle unstructured blocksGravatar Peter Collingbourne2012-05-29
* GPUVerify: mark new work-item constants as non-uniqueGravatar Peter Collingbourne2012-05-29
* GPUVerify: in unstructured mode, disable uniformity analysis and return conse...Gravatar Peter Collingbourne2012-05-25
* GPUVerify: implement a set of BV operation constructors which insert a functi...Gravatar Peter Collingbourne2012-05-25
* GPUVerify: declarations of barrier, work-item constants no longer required; G...Gravatar Peter Collingbourne2012-05-25
* GPUVerify: add reference to Graph projectGravatar Peter Collingbourne2012-05-25
* GPUVerify: add a MakeDual for unstructured blocksGravatar Peter Collingbourne2012-05-25
* GPUVerify: factor out the Cmd dualiserGravatar Peter Collingbourne2012-05-24
* GPUVerify: add block predicatorGravatar Peter Collingbourne2012-05-25
* GPUVerify: add an /unstructured command line optionGravatar Peter Collingbourne2012-05-25
* Get Boogie and GPUVerify to compile and run with MonoGravatar Peter Collingbourne2012-05-02
* Started refactoring invariant generation rules.Gravatar Unknown2012-04-24
* Removed set encoding.Gravatar Unknown2012-04-24
* Significantly changed the way race checking is performed. Made eager race ch...Gravatar Unknown2012-04-24
* removed BoogieDriver from solutionGravatar qadeer2012-04-18
* Made loop predicate invariant optionally generated.Gravatar Unknown2012-04-13
* Added invariant to predicated loops.Gravatar Unknown2012-04-10
* Minor fix to array control flow analysis.Gravatar Unknown2012-04-10
* Inference in GPUVerify now merges candidates for threads 1 and 2 into a singl...Gravatar Unknown2012-04-10
* Don't insert final barrier when eager race checking is enabled.Gravatar paulthomson2012-04-09
* Tweak to inference.Gravatar Unknown2012-04-09
* More accessed offset inferenceGravatar Unknown2012-04-09
* Refined assertion.Gravatar Unknown2012-04-06
* Tuned candidate generation.Gravatar Unknown2012-04-06
* Extended GPUVerify's candidate invariant generation to use thread id inference.Gravatar Unknown2012-04-05
* Inference of thread ids complete.Gravatar Unknown2012-04-05
* Thread id inference now generalised to infer other thread configuration param...Gravatar Unknown2012-04-05
* Thread id inference now generalised to three dimensions.Gravatar Unknown2012-04-05
* Started generalising thread id inferenceGravatar Unknown2012-04-05
* GPUverify now automatically decides then to use adversarial abstraction.Gravatar Unknown2012-04-05
* Fixed bug with handling of return in GPUVerify.Gravatar Unknown2012-04-03