Changes between Version 107 and Version 108 of WikiStart

Timestamp:

08/31/18 11:33:58 (8 years ago)

Author:

ziqing

Comment:

--

WikiStart

@@ -1 +1 @@
 = CIVL: The Concurrency Intermediate Verification Language =
-[[Image(logo.png)]]
+{{{
+#!comment
+[[Image(wiki:WikiStart:logo.png)]]
+}}}
 
-== Related Projects ==
+== About ==
+CIVL is a framework encompassing…
 
-This is the Trac site of CIVL, including its related projects:
-- [wiki:ABC]
-- [wiki:GMC]
-- [wiki:SARL]
+* a programming language, CIVL-C, which adds to C a number of concurrency primitives, as well as the ability to define functions in any scope. Together, these features make for a very expressive concurrent language that can faithfully represent programs using various APIs and parallel languages, such as MPI, OpenMP, CUDA, and Chapel. CIVL-C also provides a number of primitives supporting verification.
+* a model checker which uses symbolic execution to verify a number of safety properties of CIVL-C programs. The model checker can also be used to verify that two CIVL-C programs are functionally equivalent.
+* a number of translators from various commonly-used concurrency languages/APIs to CIVL-C (currently, MPI, OpenMP, Pthreads, and CUDA).
 
-== Tool Development ==
-- [wiki:"Be a CIVL developer"]
-- Analysis
-   * [wiki:Overview]
-   * [wiki:MemoryAnalysis]
-   * [wiki:PointsToAnalysis]
-   * [wiki:AliasAnalysis]
-- Performance
-   * [wiki:IdeasForPerformance]
-   * [wiki:HeapCanonicalization]
-   * [wiki:PolynomialExpansion]
-- Coding standards
-   * [wiki:"Coding Standards"]
-   * [wiki:"Coding Standards for CIVL models"]
-- Comparison
-   * [wiki:Comparison]
-- Fortran Translation
-   * [wiki:FortranTranslationIssues]
-- Transformers
-   * [wiki:GeneralTransformation]: translates away arguments of main.
-   * [wiki:IOTransformation]: translates stdio.h-related code to fit CIVL's stdio implementation.
-   * [wiki:MPITransformation]: translates MPI to CIVL.
-   * [wiki:PthreadTransformation]: translates Pthread code to CIVL code.
-   * [wiki:OpenMPTransformation]: translates OpenMP to CIVL.
-   * [wiki:CudaTransformation]: translates Cuda to CIVL.
-   * [wiki:OpenCLTransformation]: translates OpenCL to CIVL.
-- CIVL pragma: [wiki:CIVLPragmas]
-- GUI
-   * [wiki:GUIRequirements]
-   * [wiki:GUIDesign]
-   * [wiki:TraceViewer]
--Plans
-  * [wiki:IntDivOperations]
+== Downloads ==
 
+* Latest stable release: [http://vsl.cis.udel.edu/lib/sw/civl/current/latest/]
+* Latest unstable release: [http://vsl.cis.udel.edu/lib/sw/civl/trunk/latest/]
+* Older releases: [http://vsl.cis.udel.edu/lib/sw/civl/]
+* Online application: [http://civl.cis.udel.edu/app/]
 
+== Examples & Case Studies ==
 
-==  CIVL-C Language ==
+* [wiki:Tour A Brief Tour of CIVL with Examples]
+* [https://dl.acm.org/citation.cfm?id=3090070 CIVL Solutions to VerifyThis 2016 Challenges]
+{{{
+#!comment
+* [https://vsl.cis.udel.edu/lib/downloads/civl_verifythis_2016.pdf CIVL Solutions to VerifyThis 2016 Challenges]
+}}}
+* [https://dl.acm.org/citation.cfm?id=3145488 Towards Self-Verification in Finite Difference Code Generation]
+* [https://link.springer.com/chapter/10.1007/978-3-319-99725-4_14 Verifying Properties of Differentiable Programs] 
+== Documents & Publications ==
 
-Contents
-* [wiki:IR] : CIVL-IR
-* [wiki:DataStructures]
-* [wiki:Arrays]
-* [wiki:Pointers]
-* [wiki:Choose]
-* [wiki:MessagePassing]
-* [wiki:OmnibusChanges]
-* [wiki:ContractReduction]
-* [wiki:VerificationWithContracts]
-* [wiki:Examples]
-* [wiki:CommonHelperFunctionsForDifferentParallelLanguage]
+* [http://vsl.cis.udel.edu/lib/sw/civl/1.16/r4871/release/civl-manual-1.16_4871.pdf  Manual for CIVL v1.16]
+* [https://vsl.cis.udel.edu/pubs/civl_verifythis_2016.html CIVL Solutions to VerifyThis 2016 Challenges]
+* [https://vsl.cis.udel.edu/pubs/civl_eurompi_2017.html  Verification of MPI programs using CIVL]
 
-== Case Studies ==
-* [wiki:StandardHPCExamples]
-* [wiki:BattleOfTheDialects]
-
-== Related Works ==
-* [wiki: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 ==
-
-* [wiki:CIVLmeeting2013]
-
-== Weekly presentations ==
-
-* [wiki:2018_06_28]
-* [wiki:2018_07_05]
-
-== Paper ==
-* [wiki: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/]
+== How to Cite CIVL ==
+{{{
+@Inproceedings{siegel-etal:2015:civl_sc,
+  author = {Stephen F.\ Siegel and Manchun Zheng and Ziqing Luo and
+            Timothy K.\ Zirkel and Andre V.\ Marianiello and John G.\ Edenhofner
+            and Matthew B.\ Dwyer and Michael S.\ Rogers},
+  title = {{CIVL}: The Concurrency Intermediate Verification Language},
+  booktitle = {SC15: International Conference for High Performance
+               Computing, Networking, Storage and Analysis, Proceedings},
+  series = {SC '15},
+  year = {2015},
+  month = {Nov},
+  publisher = {IEEE Press},
+  address = {Piscataway, NJ, USA},
+  pages = {61:1-61:12}
+}
+}}}
 
 == Bug Report ==
@@ -101 +58 @@
 
 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
-* [wiki:Conferences]
-* [wiki:DeveloperPage]
-* [wiki:UserPage]