Discussions under General

Apr 25

7:37 PM
(7 posts)

Dafny: cannot generate model file

first post: Yuyan wrote: I tried the command: dafny -mv:foo.model foo.dfy It is supposed to...

latest post: Yuyan wrote: My Z3 is 3.2 and boogie version is 2.2.30705.1126, which source is ...

Apr 11

2:42 PM
(3 posts)

Dafny: termination with datatypes problem

first post: kornevgen wrote: I'm wonder why Dafny can't prove termination in this program http:...

latest post: kornevgen wrote: Thank you, Rustan!

Apr 5

7:31 PM
(4 posts)

Encoding of spatial conjunction in Boogie

first post: ck1909 wrote: How is the concept of the spatial conjunction (also known as the "s...

latest post: rustanleino wrote: There is only one heap, just like there's just one heap when the pr...

Apr 5

12:17 AM
(2 posts)

Boogie: Cannot show error messages in VS2010

first post: Yuyan wrote: Mimicing Dafny, I renamed a copy of "StartDafny.bat" as "StartBoog...

latest post: rustanleino wrote: Strange. What you did works for me. I presume you have built (usi...

Mar 19

9:43 AM
(1 post)

Boogie: name, ref, null ?

first post: ddemange wrote: Dear all, I need to write my own program in Boogie, and don't want...

Mar 11

12:59 PM
(4 posts)

Installation problem

first post: borishollas wrote: Hello, I've installed Z3 and extracted the Boogie-zip-file. When I ...

latest post: jecsicacuk wrote: I had a similar problem. It turned out to be down to the fact that ...

Mar 10

9:49 AM
(6 posts)

Problem running Chalice from command line

first post: ck1909 wrote: I am have problems getting Chalice to work from command line. I al...

latest post: ck1909 wrote: Thanks for your helpful advice Stefan. The verifier seems to work w...

Feb 29

2:52 AM
(1 post)

CFP: BOOGIE 2012 - 2nd International Workshop on Intermediate Verification Languages

first post: zrakamar wrote: ******************************************************************...

Dec 13 2011

8: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 threa...

Oct 31 2011

6:59 PM
(5 posts)

Z3 crash?

first post: marciojc wrote: Hi, i'm work with Boogie and when i try the example in Rise4Fun, th...

latest post: RustanLeino wrote: No, as of last Friday, Boogie now expects Z3 version 3.2. To get t...