CIVL: The Concurrency Intermediate Verification Language

CIVL-C Language

Contents

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

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

Proposals & Plans

These are proposed plans for enhancing CIVL or related tools

• IntDivOperations

Weekly Presentation Schedule

This is the schedule list of weekly presentations

• 2018_06_28 Control Flow Graph
• 2018_07_05 C Implementation of Naive Decision Tree

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

Related Tools

These are links to wiki-pages or official sites of tools used by CIVL

• ABC
• GMC
• SARL
• Z3 (​https://github.com/Z3Prover/z3/wiki)
• CVC4 (​http://cvc4.cs.stanford.edu/web/)
• Why3 (​http://why3.lri.fr/)
• Frama-C (​https://frama-c.com/)

Other Links

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

Depricated Pages

Pages are going to be deleted.

• Insieme
• StandardHPCExamples
• BattleOfTheDialects