CIVL: The Concurrency Intermediate Verification Language

Related Projects

This is the Trac site of CIVL, including its related projects:

• ABC
• GMC
• SARL

Tool Development

• Be a CIVL developer
• Analysis
  • Overview
  • MemoryAnalysis
  • PointsToAnalysis
  • AliasAnalysis
• Performance
  • IdeasForPerformance
  • HeapCanonicalization
  • PolynomialExpansion
• Coding standards
  • Coding Standards
  • Coding Standards for CIVL models
• Comparison
  • Comparison
• Fortran Translation
  • FortranTranslationIssues
• 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

-Plans

• IntDivOperations

CIVL-C Language

Contents

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

Case Studies

• StandardHPCExamples
• BattleOfTheDialects

Related Works

• Insieme

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: ​http://vsl.cis.udel.edu/lib/sw/civl/current/latest/
• Latest unstablerelease: ​http://vsl.cis.udel.edu/lib/sw/civl/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 source 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