CIVL: The Concurrency Intermediate Verification Language

The CIVL-C Language

Contents

• Arrays
• Pointers
• MessagePassing
• OmnibusChanges
• LanguageSubset
• Examples

Thoughts about the CIVL-C language

• It might be nice to introduce some convenience constructs that are syntactic sugar for commonly occurring patterns. For example, something like "$proc p = $run stmt" which is short for declaring a temporary procedure with body stmt and spawning that procedure. Also, something like "$waitall($proc procs[], int numProcs);" (that one can be defined as a library function).

Meetings

• CIVLmeeting2013

Tool Development

• Performance
  • IdeasForPerformance
• Coding standards
  • Coding Standards
  • Coding Standards for CIVL models
• Comparison
  • Comparison
• Transformers
  • MPITransformation
  • OpenMPTransformation
  • IOTransformation

Release

Junit reports, download:

• Latest release: ​https://vsl.cis.udel.edu/civl/test/current/latest/
• Latest unstablerelease: ​https://vsl.cis.udel.edu/civl/test/trunk/latest/

Bug Report

If you have any problem when using CIVL, you can report it by creating a new ticket: https://vsl.cis.udel.edu/trac/civl/newticket It would be helpful for us to trace the bug if you also submit your CIVL-C programs as attachments of the ticket.

Other Links

• Paper reading: ​https://docs.google.com/spreadsheet/ccc?key=0AvyY9XPxT2MVdFJzMThfWVdGZFpsYkNCcEJzUGdyYWc#gid=0
• Conferences: ​https://docs.google.com/spreadsheet/ccc?key=0AvyY9XPxT2MVdEx6OFJ5b2MzMms1UW1YQjhSdXdpU3c&usp=drive_web#gid=0