summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
| | | * 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
| | |/ | |/|
| * | MergeGravatar qadeer2012-05-24
| |\|
| * | more refactoring in stratified inliningGravatar qadeer2012-05-24
| | * Boogie: document /typeEncoding:mGravatar Peter Collingbourne2012-05-22
| |/ |/|
* | Fix DomRelation.DominatedBy for the case where the dominator is the sourceGravatar Peter Collingbourne2012-05-22
|/
* MergeGravatar qadeer2012-05-21
|\
* | small fixGravatar qadeer2012-05-21
* | starting the implementation of the new stratified inlining APIGravatar qadeer2012-05-21
| * MergeGravatar Unknown2012-05-18
| |\ | |/ |/|
| * Dafny: more correct checking of co-inductive productivityGravatar Unknown2012-05-18
* | shutting down the prover used for doing houdiniGravatar qadeer2012-05-10
* | MergeGravatar qadeer2012-05-10
|\ \
* | | some other cleanupsGravatar qadeer2012-05-10
| * | Z3: do not assert that the ProgramFiles environment variable is setGravatar Peter Collingbourne2012-05-02
| * | Boogie: handle absolute paths on *nix correctlyGravatar Peter Collingbourne2012-05-02
| * | Get Boogie and GPUVerify to compile and run with MonoGravatar Peter Collingbourne2012-05-02
| * | Slightly better management of outermost Push-Pop and FlushAxiomsGravatar Unknown2012-05-02
|/ /
* | z3 process is killed nowGravatar qadeer2012-05-01
* | MergeGravatar qadeer2012-05-01
|\ \
* | | added counterexample generation based on labels back to stratified inliningGravatar qadeer2012-05-01
| | * Dafny: improve printing of inductive datatypesGravatar Unknown2012-05-01
| |/
| * MergeGravatar Rustan Leino2012-05-01
| |\ | |/ |/|
| * Dafny: print inductive datatypesGravatar Rustan Leino2012-05-01
| * Dafny: added support for co-recursive callsGravatar Rustan Leino2012-05-01
* | log file fixGravatar qadeer2012-04-30
* | UseLabels=false when stratified inline is onGravatar qadeer2012-04-29
* | clean up in stratified inliningGravatar qadeer2012-04-29
|/
* 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