Floating point arithmetic

first post: aaa111 wrote: Is there a plan to support verification of floating point arithmetic?

VCC doesnt find vcc.h

first post: 13deepakjain wrote: I am using vcc from command line. When I run the command "vcc dem...

latest post: yop wrote: This problem got solved for me when I installed VS2012 and reinstal...

Can VCC verify gcd (greatest common divider) progam

first post: yongjian wrote: Dear expert: The following is a Boogie-code to verify gcd algori...

create Visual Studio Code Extension

first post: Craven wrote: Hi, I'm wondering if a Visual-Studio-Code-Extension could be develo...

Giving write permission to 2D array

first post: yzhiren wrote: Hi, Is there any way to give write permission to a 2D array? Give...

Add two preconditions and it will always be "Verification succeeded"!!

first post: zdaijie wrote: void vListInsert( xList *pxList, xListItem *pxNewListItem ) _(requ...

latest post: erniecohen wrote: It verifies because your preconditions are inconsistent. A writes ...

error VC0000

first post: bpankaj wrote: Please help me with these errors, error VC0000: unions with primit...

latest post: erniecohen wrote: Did you mean to have a union somewhere?

answered by: bpankaj wrote: Sorry, wrong question. Correct definitions: struct foo{ int el...

2-dim list of parameters for _(writes)

first post: akarimi16 wrote: I need to declare a function that writes into a matrix C of given s...

Admissibility of invariants of dependent types

first post: bpankaj wrote: Hello, I am not getting, in the following type definitions, why in...

latest post: bpankaj wrote: Thank you for your reply. It was helpful. Can you please, tell spec...

Doubt with quantifiers.

first post: RahulUday wrote: Hi all, How to use the \forall quantifier with variables of dif...

latest post: RahulUday wrote: Thank You Sir. Can we use the \exists quantifier along with the \fo...