| Version 90 (modified by , 10 years ago) ( diff ) |
|---|
CIVL: The Concurrency Intermediate Verification Language
Tool Development
- Static analysis
- Performance
- Coding standards
- 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
CIVL-C Language
Contents
- IR : CIVL-IR
- DataStructures
- Arrays
- Pointers
- Choose
- MessagePassing
- OmnibusChanges
- ContractReduction
- VerificationWithContracts
- Examples
- CommonHelperFunctionsForDifferentParallelLanguage
Case Studies
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
Paper
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 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
Note:
See TracWiki
for help on using the wiki.
