CodePlex
Open Source Community
Register | Sign In | CodePlex Home
Search
Latest post:
Dec 13 2011
9:56 AM
1 post

Semaphore in Chalice, shared variable with multiple writers

First post: SRoede wrote: Hi, I'm trying to see if I can prove some properties of .net threaded code I have written. In the code I use the .net "System.T...
Jump to: First Post   
Latest post:
Nov 9 2011
11:28 AM
3 posts

Installation problem

First post: borishollas wrote: Hello, I've installed Z3 and extracted the Boogie-zip-file. When I run Dafny on an example file, I get ~$ /cygdrive/c/Program\ ...
Latest post: borishollas wrote: Thanks, it works now.
Jump to: First Post · Latest Post   
Latest post:
Oct 31 2011
7:59 PM
5 posts

Z3 crash?

First post: marciojc wrote: Hi, i'm work with Boogie and when i try the example in Rise4Fun, the Fibonacci, i get the follow result. Boogie program verifie...
Latest post: RustanLeino wrote: No, as of last Friday, Boogie now expects Z3 version 3.2. To get that version of Boogie today, either synch and build from sou...
Jump to: First Post · Latest Post   
Latest post:
Jul 5 2011
1:35 PM
4 posts

Boogie's /prover option

First post: mschwerhoff wrote: Hi all,how is the /prover option of Boogie supposed to be used? I tried /prover:"C:\Program Files (x86)\Microsoft Researc...
Latest post: mschwerhoff wrote: Hi all,one can now specify the Z3 executable to use via -z3exe:"path\to\z3.exe".Regards, Malte
Jump to: First Post · Latest Post   
Latest post:
Jun 30 2011
11:10 PM
2 posts

Limited number of assignments?

First post: o_p wrote: Hi,Dafny 2.0.0.0 erroneously reports an assertion violation for the following code. Commenting any assignment (except for b0 of...
Latest post: RustanLeino wrote: Thanks for the bug report. Boogie used an implicit limit in Z3, which I have now removed for the axioms needed for this (and s...
Jump to: First Post · Latest Post   
Latest post:
Apr 28 2011
2:38 AM
7 posts

Boogie postcondition violation undetected

First post: imansaleh wrote: Hi,I have been trying Spec# with the following code. The code passes the verification even if I introduce a mutation error in t...
Latest post: imansaleh wrote: Yes, makes sense. However, the code with the error distorts the array to be sorted.To solve that, and have the specification de...
Jump to: First Post · Latest Post   
Latest post:
Apr 8 2011
10:24 PM
2 posts

Check one block

First post: marciojc wrote: I see that boogie check the verification condition(vc) on the method BeginCheck (VC.cs).If i want to check only the vc of one b...
Latest post: RustanLeino wrote: There's currently no support in Boogie for checking only one block, but that shouldn't be too difficult for you to add--if a ch...
Jump to: First Post · Latest Post   
Latest post:
Feb 1 2011
10:57 PM
1 post

Boogie 2011: Call For Papers

First post: MichalMoskal wrote: Boogie 2011: First International Workshop on Intermediate Verification Languages co-located with CADE-23, Wrocław, Poland, Aug...
Jump to: First Post   
Latest post:
Jan 27 2011
9:05 AM
1 post

Order specification

First post: TimmFelden wrote: In krml178 page 40 the semantics of orders are specified. It would be nice to include that const a extends b;is equivalent to a...
Jump to: First Post   
Latest post:
Aug 20 2010
6:29 PM
4 posts

Is verification condition splitting implemented

First post: thorstent wrote: Hi,one quick question: Is the verification condition splitting outlined in the paper "Verification Condition Splitting" by Lein...
Latest post: MichalMoskal wrote: This is expected. There is more Z3 invocations, so randomness in each averages out. Back in Z3 1.x days it used to speed up the...
Jump to: First Post · Latest Post   

Configure View

Search
Topics
All Topics
General
Discussion Notification
Sign in to display notification settings.
Show 10  25 discussions
1-10 of 19 discussions < Previous 1 2 Next >
Updating...
© 2006-2012 Microsoft | Get Help | Privacy Statement | Terms of Use | Code of Conduct | Advertise With Us | Version 2012.2.15.18416