--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on September 2010 ---
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