summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Dafny: print inductive datatypesGravatar Rustan Leino2012-05-01
* Dafny: added support for co-recursive callsGravatar Rustan Leino2012-05-01
* eliminated class ErrorModelGravatar qadeer2012-04-28
* removed proccopybounding codeGravatar qadeer2012-04-28
* eliminated LazyInliningInfoGravatar qadeer2012-04-28
* removed lazy inliningGravatar qadeer2012-04-28
* MergeGravatar qadeer2012-04-27
|\
* | unsat core for houdiniGravatar qadeer2012-04-27
| * Dafny: fixed unsoundness having to do with a function depending on the alloca...Gravatar Unknown2012-04-27
| * MergeGravatar Unknown2012-04-26
| |\ | |/ |/|
| * Dafny: fixed bug that had omitted the computation of .DefaultCtor for some in...Gravatar Unknown2012-04-26
| * Dafny: compile co-inductive datatypesGravatar Unknown2012-04-26
| * Dafny: rudimentary translation into Boogie of co-inductive datatypesGravatar Unknown2012-04-25
| * Dafny: fixed resolution bug for inductive datatypes (previous check did not h...Gravatar Unknown2012-04-25
* | MergeGravatar Unknown2012-04-24
|\|
* | 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
| * Added test to stratified inlining.Gravatar Unknown2012-04-24
| * MergeGravatar Unknown2012-04-20
| |\ | |/ |/|
| * Dafny: fixed bug (missing Boogie cast) in translation of induction over gener...Gravatar Unknown2012-04-20
* | removed BoogieDriver from solutionGravatar qadeer2012-04-18
* | various changes for using unsat cores in HoudiniGravatar qadeer2012-04-17
* | MergeGravatar Unknown2012-04-13
|\ \
* | | Made loop predicate invariant optionally generated.Gravatar Unknown2012-04-13
| |/ |/|
| * Added functionality to "skip" procedures. Some cleanup.Gravatar akashlal2012-04-12
|/
* 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
* MergeGravatar Unknown2012-04-05
|\
* | GPUverify now automatically decides then to use adversarial abstraction.Gravatar Unknown2012-04-05
| * Fixed bug with triply nested maps and polymorphism (reported as Item # 10218).Gravatar Unknown2012-04-04
| * small fixGravatar qadeer2012-04-04
| * MergeGravatar qadeer2012-04-03
| |\ | |/ |/|
| * added nonUniformUnfolding optionGravatar qadeer2012-04-03
* | Fixed bug with handling of return in GPUVerify.Gravatar Unknown2012-04-03
* | MergeGravatar Unknown2012-04-03
|\ \
* | | Added support for break and return.Gravatar Unknown2012-04-03
| | * deleted the option UseUnsatCoreForInliningGravatar qadeer2012-04-02
| | * MergeGravatar qadeer2012-04-01
| | |\ | | |/ | |/|