CIVL: The Concurrency Intermediate Verification Language

Tool Development

• Static analysis
  • Overview
  • MemoryAnalysis
• Performance
  • IdeasForPerformance
  • HeapCanonicalization
• Coding standards
  • Coding Standards
  • Coding Standards for CIVL models
• Comparison
  • Comparison
• Transformers
  • GeneralTransformation: translates away arguments of main.
  • IOTransformation: translates stdio.h-related code to fit CIVL's stdio implementation.
  • MPITransformation: translates MPI to CIVL.
  • PthreadTransformation: translates Pthread code to CIVL code.
  • OpenMPTransformation: translates OpenMP to CIVL.
  • CudaTransformation: translates Cuda to CIVL.
  • OpenCLTransformation: translates OpenCL to CIVL.
• CIVL pragma: CIVLPragmas
• GUI
  • GUIRequirements
  • GUIDesign
  • TraceViewer

CIVL-C Language

Contents

• IR : CIVL-IR
• DataStructures
• Arrays
• Pointers
• Choose
• MessagePassing
• OmnibusChanges
• ContractReduction
• VerificationWithContracts
• Examples
• CommonHelperFunctionsForDifferentParallelLanguage

Case Studies

• StandardHPCExamples
• BattleOfTheDialects

Competition

Some information concerning SV-COMP.

• ​http://sv-comp.sosy-lab.org/2015/ : SV-COMP 2015
• ​http://gcc.gnu.org/onlinedocs/gcc/C-Extensions.html : the GNU extensions to C
• ​http://www.sosy-lab.org/~dbeyer/cpa-witnesses/ : Error witness format
• ​http://sv-comp.sosy-lab.org/2015/Minutes-2014.txt : Minutes of 2014 meeting

Meetings

• CIVLmeeting2013

Paper

• ExampleList

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.

When reporting a bug, you are greatly recommended to provide specific information as much as possible, such as the civl command, the source files, the civl version, the error message or exception, etc. The minimum is to provide sufficient information for others to reproduce the problem.

Other Links

• Paper reading:
  • Sources ​https://vsl.cis.udel.edu/readings.html
  • Schedule ​https://docs.google.com/spreadsheet/ccc?key=0AvyY9XPxT2MVdFJzMThfWVdGZFpsYkNCcEJzUGdyYWc#gid=0
• Conferences: ​https://docs.google.com/spreadsheet/ccc?key=0AvyY9XPxT2MVdEx6OFJ5b2MzMms1UW1YQjhSdXdpU3c&usp=drive_web#gid=0