--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on September 2013 ---
Wow, thank you for the fast replies! Thanks for looking for bugs in my specification. That's an interesting attempt to formalise concurrency. Are concurrency proofs that much more difficult because they require strong (an invariant must be maintained inside a function, and any "dysvariancy" must be confined to atomic primitives) as opposed to weak invariants (an invariant must be maintained at function enter, and exit,) or are concurrency proofs difficult for other reasons? Thank you for the help. I'll study it in more detail later. Frama-C is looking really powerful (in particular the value analysis looks like it'll be really useful for debugging,) although I'm still having a few problems with it (Frama-C isn't treating main as anything special, and is paranoid that the system might pass main bad pointers in argv.) This is isn't the thread to discuss this though, and I'll post later when I think out my problems more.