Embedded Systems Professionals

• About this group
• Forums

• Home
• Groups
• Embedded Systems Professionals
• Forums
• Newsflash
• Verifying C Compilier

• 
  Robert Berger    Group moderator

  The company name is only visible to registered members.

  Verifying C Compilier

  VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity.
  
  Full Story:
  http://www.reliableembeddedsystems.com/newsflashes/newsflash...
  
  • 08 Mar 2010, 8:52 pm
  Robert Berger wrote: > VCC is a tool that proves correctness of annotated concurrent C > programs or finds problems in them. VCC extends C with design by > contract features, like pre- and postcondition as well as type > invariants. Annotated programs are translated to logical formulas > using the Boogie tool, which passes them to an automated SMT solver > Z3 to check their validity. > > Full Story: > http://www.reliableembeddedsystems.com/newsflashes/newsflash/verifying-c-compilier.html