--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on September 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Message-passing (concurrent) code verification



On Thu, 2010-09-16 at 17:45 -0700, Jo?o Paulo Carvalho wrote:
> Hi,
> 
> Do you know if there exists any way of verifying a message-passing
> program (concurrent), using annotations in pre/postcondition style,
> like those in ACSL and JML?
> 
> I'm not interested in concurrent code based on syncronization
> variables.

You may want to have a look at VCC, which has been designed to verify
concurrent C code. A tutorial is available at
http://research.microsoft.com/en-us/um/people/moskal/pdf/vcc-tutorial-2col.pdf.
However, I don't think there's explicit support for message passing.

-- 
Best regards,
Boris Hollas