CIVL Archive for 'Verifying Fortran Programs with CIVL'

Resource Download

• VirtualBox
• OS Image 'TACAS 22 AE.ova'
• CIVL Zip Archive
• README

Instruction of Archive Deployment

1. Download Experiment Environment

• Install VirtualBox (version 6.1.28 is used for creating this archive)
• Import Linux OS Image ('TACAS 22 AE.ova' is used for creating this archive)
follow the instruction shown after choosing 'Import Appliance...' from 'File' in menu of VirtualBox.
• Download CIVL Tool Archive and transfer the zip file into a directory in VirtualBox OS

1). Use 'wget' command in the Virtual OS

$ wget https://vsl.cis.udel.edu/lib/archives/tacas2022/civl_tacas22.zip


2). Use 'Guest Additions CD Image':
- Start the Virtual OS Image and then choose 'Insert Guest Additions CD Image...' from 'Devices' the in menu bar.
- Follow the popped instruction to install the plug-in
- Re-boot the Virtual OS Image
- Enable 'Bidirectional' from item 'Drag and Drop' in 'Devices' (which is in the menu bar).
- Drag 'civl_tacas22.zip' from host machine to the GUI of Virtual OS Image and then drop it.

2. Deploy Tool to Virtual OS

• Unzip the tool archive zip file to '/home/tacas22/Documents/':
Note that this archive requires to use the OS Image and to be extracted to this specific directory.
CIVL Jar executable file 'civl.jar' is required to be in '/home/tacas22/Documents/civl_tacas22/bin'.

$ unzip civl_tacas22.zip -d /home/tacas22/Documents/

• Files included are:
'./civl_tacas22/bin/civl.jar': the binary executable jar file of CIVL
'./civl_tacas22/bin/civl': a bash script invoking civl.jar from '/home/tacas22/Documents/civl_tacas22/'
'./civl_tacas22/deps/*.deps': dependencies required by CIVL
'./civl_tacas22/deps/*.deb': offline dependency packages
'./examples/*': source files used in verification experiments
'./out/*': this directory is used for holding verification outputs
'./out_paper/*': this directory is used for holding verification outputs mentioned in the paper,
which are executed in the environment described in paper (Section 5.1)
'./License.txt': Licenses of CIVL, SMACK verification suite, and Nek5000
'./makefile': makefile for executing all verification experiments
'./README': Instruction of using the tool archive

3. Install Dependencies

• change directory to './civl_tacas22/deps/' after the archive is unzipped.

$ cd /home/tacas22/Documents/civl_tacas22/deps/

• install all required dependencies including: openjdk11, cvc4, and z3

$ sudo dpkg -i *.deb

• back to the root directory './civl_tacas22/'

$ cd ..

• check versions of dependencies installed
Check the version of openjdk:

$ java --version
openjdk 11.0.11 2021-04-20
OpenJDK Runtime Environment (build 11.0.11+9-Ubuntu-0ubuntu2.20.04)
OpenJDK 64-Bit Server VM (build 11.0.11+9-Ubuntu-0ubuntu2.20.04, mixed mode, sharing)

Check the version of cvc4:

$ cvc4 --version
This is CVC4 version 1.6
compiled with GCC version 9.2.1 20200202
on 2020-02-03 20:12:28

Check the version of z3:

$ z3 --version
Z3 version 4.8.7 - 64 bit

4. Configure CIVL

• set the bash script ./bin/civl to be executable

$ chmod ugo+x ./bin/civl

• sudo copy the script to directory '/usr/local/bin/'

$ sudo cp ./bin/civl /usr/local/bin/civl

• configure CIVL

$ civl config
CIVL v1.20+ of 2019-09-27 -- http://vsl.cis.udel.edu/civl
Creating SARL configuration file in /home/tacas22/.sarl
Adding Z3 version 4.8.7 - 64 bit at /usr/bin/z3
Adding CVC4 version 1.6 at /usr/bin/cvc4
Ignoring equivalent Z3 version 4.8.7 - 64 bit at /bin/z3
Ignoring equivalent CVC4 version 1.6 at /bin/cvc4
SARL configuration file created successfully in /home/tacas22/.sarl
By default, SARL will use all provers listed in the configuration file,
in order, until a conclusive result is obtained.
Edit the file as necessary to remove or change the order of provers.


* If 'civl' bash script can not be 'sudo cp' to '/usr/local/bin/'
* then 'civl' command used in makefile variable 'CMD_CIVL' (line 8) can be
* replaced by 'java -jar /home/tacas22/Documents/civl_tacas22/bin/civl.jar'
* so that 'make all' can be run from '/home/tacas22/Documents/civl_tacas22/'
* e.g.,
* CMD_CIVL=java -jar /home/tacas22/Documents/civl_tacas22/bin/civl.jar

5. Replicate Experiments

• get verification results for all examples mentioned in the paper
(terminal outputs for each example are saved to directory: ./out)

$ make all