Compare

.gitignore

@@ -0,0 +1 @@
+local/

LICENSE.txt

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) [2021] [Cesar Sanchez, Borzoo Bonakdarpour, Tzu-Han Hsu]
+Copyright (c) [2021] [César Sánchez, Borzoo Bonakdarpour, Tzu-Han Hsu]
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

Makefile

@@ -7,3 +7,7 @@ clean:
 	find . -name "*.quabs" -delete
 	find . -name "*.qcir" -delete
 	find . -name "*.cex" -delete
+	find . -name "*QS" -delete
+	find . -name "*.cex" -delete
+	find . -name "P.hq" -delete
+	find . -name "*.hoa" -delete

README.md

@@ -1,12 +1,11 @@
-# Welcome to HyperQube!
-
-HyperQube is a home-grown tool of Bounded Model Checking for Hyperproperties.
+# Welcome to HyperQB!
 
+HyperQB is a home-grown tool of Bounded Model Checking for Hyperproperties.
 
 Hyperproperty specifies and reasons about important requirements among multiple traces.
-We implement our algorithm for Bounded Model Checking for Hyperproperty as a tool, HyperQube.
+We implement our QBF-based algorithm for Bounded Model Checking for Hyperproperty as a tool, HyperQB.
 
-HyperQube includes several parts:
+HyperQB includes several parts:
 - NuSMV model parsing and Boolean encoding of transition relation and specification,
 - HyperLTL formula translation,
 - QBF encoding of unfolding with bound k using specific semantics,
@@ -17,39 +16,43 @@ while the existing tool, QuAbs, is under AGPL license.
 
 
 
-## HOW TO USE
-To run HyperQube, install [docker](https://docs.docker.com/get-docker/) then execute ```hyperqube.sh``` with one of the following two scenarios:
-
-   1. BMC with single model:<br/>
-	```./hyperqube.sh <model_file_name.smv> <formula_file_name.hq> <k> ```
-
-   2. BMC with multi-model:<br/>
-	```./hyperqube.sh <model_1_file_name.smv> <model_2_file_name.smv> <formula_file_name.hq> <k>```
-
-Note that <k> is a natural number specifies the length of unrolling.
+## Get Started
+You can start using HyperQB in 2 simple steps:
+1. First install [docker](https://docs.docker.com/get-docker/). 
+HyperQB will automatically pull the image and execute the scripts to avoid possible hassle of compiling dependencies!
 
+2. Next, clone the repository and step into the repo:
+- ```git clone https://github.com/TART-MSU/HyperQB.git```
+- ```cd HyperQB```
 
-To observe the tool outputs, all model checking results with counterexample will output as *_OUTPUT_formatted.cex. The parsed outputs have variables, time stamps, and values neatly presented.
-
+You are now ready to run HyperQB!:D
 
-## GET STARTED
-You can start using HyperQube in 2 simple steps:		
 
-1. First make sure DOCKER is installed from: https://docs.docker.com/get-docker/ . HyperQube will automatically pull the image and execute the scripts to avoid possible hassle of compiling dependencies.
-2. Next, clone the repository and step into the repo:
-- ```git clone https://github.com/TART-MSU/HyperQube.git```
-- ```cd HyperQube```
 
-You are now ready to run HyperQube!
+## How to Use
+To run HyperQB, execute ```hyperqb.sh``` with the following inputs:
+- `<list of models>` written in NuSMV format (as .smv files),
+- `<formula>` written in the grammar described in Sec. 4 (as a .hq file),
+- `<k>` a natural number 0, specifying the unrolling bound,
+- `<sem>` the semantics, which can be -pes, -opt, -hpes or -hopt, and
+- `<mode>` to say performing classic BMC (i.e., negating the formula) or not, which can be -bughunt or -find (we use the former as default value).  
+
+RUN HyperQB in the following format:
+    ```./hyperqube <list of models> <formula> <k> <sem> <mode>```
 
-We provide two demo examples. To run, execute each of the followings:
-- (Example 1: bakery with symmetry:) <br/> ```./hyperqube.sh demo/bakery.smv demo/symmetry 10 pes -single```
-- (Example 2: SNARK with linearizability) <br/> ```./hyperqube.sh demo/SNARK_conc.smv demo/SNARK_seq.smv demo/linearizability 18 pes -multi```
+To observe the tool outputs (i.e., counterexample or witness) 
+    See ```*_OUTPUT_formatted.cex``` for parsed outputs have variables, time stamps, and values neatly presented.
+
+Demo Examples:
+1. [demo 1: run bakery algorithm with symmetry property]
+```./hyperqb.sh demo/bakery.smv demo/bakery.smv demo/symmetry.hq 10 -pes```
 
+2. [dem0 2: run SNARK algorithm with linearizability propoerty]
+```./hyperqb.sh demo/SNARK_conc.smv demo/SNARK_seq.smv demo/lin.hq 18 -pes```    
 
 
 ## Experiments
-(all models and formulas are in directory tacas21_cases)
+(all models and formulas are in directory cases_bmc)
 
 Our evaluations include the following cases,<br/>
 - Case #1.1-#1.4: Symmetry in the Bakery Algorithm<br/>
@@ -58,14 +61,34 @@ Our evaluations include the following cases,<br/>
 - Case #4.1-#4.2: Fairness in Non-repudiation Protocols<br/>
 - Case #5.1-#5.2: Privacy-Preserving Path Synthesis for Robots<br/>
 - Case #6.1: Mutant Synthesis for Mutation Testing<br/>
+- Case #7.1: Co-termination of multiple programs<br/>
+- Case #6.1: Mutant Synthesis for Mutation Testing<br/>
+- Case #6.1: Mutant Synthesis for Mutation Testing<br/>
+- Case #6.1: Mutant Synthesis for Mutation Testing<br/>
+- Case #6.1: Mutant Synthesis for Mutation Testing<br/>
+- Case #7.1: Co-termination<br/>
+- Case #8.1: Deniability<br/>
+- Case #9.1 - #9.3: Intransitive Non-interference<br/>
+- Case #10.1 - #10.2: TINI and TSNI
+- Case #11.1: K-safety
 
-We also provide all the command lines needed for each experiment in the document *RUN.txt*
 
+## One-click Scripts
+We provide several convenient scripts for executing exeperiments. 
 
+- run ```./run_demos.sh``` to run demo examples
+- run ```./run_tacas21.sh``` to run all experiments for TACAS21
+- run ```./run_cav23.sh``` to run all experiments for CAV23 
+
+We also provide all the command lines needed for each experiment in the document *RUN.txt*
 
 
 ## People
 Authors:
 - [Tzu-Han Hsu](https://tzuhancs.github.io/), Michigan State University.
 - [Borzoo Bonakdarpour](http://www.cse.msu.edu/~borzoo/), Michigan State University.
 - [César Sánchez](https://software.imdea.org/~cesar/), IMDEA Software Institute.
+
+Publication:
+- [Bounded Model Checking for Hyperproperties (TACAS'21)](https://link.springer.com/content/pdf/10.1007/978-3-030-72016-2_6.pdf)
+

RUN.txt

@@ -5,96 +5,96 @@ This file provide the command lines to run specific experiments we provided in t
 
 Small demos in the tool paper:
 
-./hyperqube.sh demo/simple.smv demo/simple.hq 1 pes -single
-./hyperqube.sh demo/mini.smv demo/mini.hq 1 pes -single
+./hyperqb.sh demo/simple.smv demo/simple.hq 1 pes -single
+./hyperqb.sh demo/mini.smv demo/mini.hq 1 pes -single
 
 [run bakery algorithm with symmetry property]
-  ./hyperqube.sh demo/bakery.smv demo/symmetry.hq 10 pes -single
+  ./hyperqb.sh demo/bakery.smv demo/symmetry.hq 10 pes -single
 
 [run SNARK algorithm with linearizability propoerty]
-  ./hyperqube.sh demo/SNARK_conc.smv demo/SNARK_seq.smv demo/linearizability 18 pes -multi
+  ./hyperqb.sh demo/SNARK_conc.smv demo/SNARK_seq.smv demo/linearizability 18 pes -multi
 
 
 Experiments in the tool paper:
 [run simple_krip with simple_krip_formula]
-  ./hyperqube.sh cases_bmc/simple_krip.smv  cases_bmc/simple_krip_formula.hq 5 pes
+  ./hyperqb.sh cases_bmc/simple_krip.smv  cases_bmc/simple_krip_formula.hq 5 pes
 
 
 [BAKERY]
 -- 1.1 BAKERY 3PROC SYM1 --
-  ./hyperqube.sh cases_bmc/bakery_3procs.smv cases_bmc/bakery_formula_sym1_3proc.hq 10 pes
+  ./hyperqb.sh cases_bmc/bakery_3procs.smv cases_bmc/bakery_formula_sym1_3proc.hq 10 pes
 
 -- 1.2 BAKERY 3PROC SYM2  --
-  ./hyperqube.sh cases_bmc/bakery_3procs.smv cases_bmc/bakery_formula_sym2_3proc.hq 10 pes
+  ./hyperqb.sh cases_bmc/bakery_3procs.smv cases_bmc/bakery_formula_sym2_3proc.hq 10 pes
 
 -- 1.3 BAKERY 5PROC SYM1 --
-  ./hyperqube.sh cases_bmc/bakery_5procs.smv cases_bmc/bakery_formula_sym1_5proc.hq 10 pes
+  ./hyperqb.sh cases_bmc/bakery_5procs.smv cases_bmc/bakery_formula_sym1_5proc.hq 10 pes
 
 -- 1.4 BAKERY 5PROC SYM2 --
-  ./hyperqube.sh cases_bmc/bakery_5procs.smv cases_bmc/bakery_formula_sym2_5proc.hq 10 pes
+  ./hyperqb.sh cases_bmc/bakery_5procs.smv cases_bmc/bakery_formula_sym2_5proc.hq 10 pes
 
 
 
 [SNARK]
 
 -- 2.1 SNARK_BUG 1 --
-  ./hyperqube.sh cases_bmc/snark1_M1_concurrent.smv cases_bmc/snark1_M2_sequential.smv  cases_bmc/snark1_formula.hq 18 pes
+  ./hyperqb.sh cases_bmc/snark1_M1_concurrent.smv cases_bmc/snark1_M2_sequential.smv  cases_bmc/snark1_formula.hq 18 pes
 
 -- 2.2 SNARK_BUG 2 --
-  ./hyperqube.sh cases_bmc/snark2_new_M1_concurrent.smv  cases_bmc/snark2_new_M2_sequential.smv cases_bmc/snark2_formula.hq 30 pes
+  ./hyperqb.sh cases_bmc/snark2_new_M1_concurrent.smv  cases_bmc/snark2_new_M2_sequential.smv cases_bmc/snark2_formula.hq 30 pes
 
 
 
 [3-thread]
 -- 3.1 3-thread incorrect --
-  ./hyperqube.sh cases_bmc/NI_incorrect.smv cases_bmc/NI_formula.hq 50 hpes
+  ./hyperqb.sh cases_bmc/NI_incorrect.smv cases_bmc/NI_formula.hq 50 hpes
 
 -- 3.2 3-thread correct --
-  ./hyperqube.sh cases_bmc/NI_correct.smv cases_bmc/NI_formula.hq 50 hopt
+  ./hyperqb.sh cases_bmc/NI_correct.smv cases_bmc/NI_formula.hq 50 hopt
 
 [Non-repudiation Protocol]
 
 -- 4.1 NRP incorrect
-  ./hyperqube.sh cases_bmc/NRP_incorrect.smv cases_bmc/NRP_formula.hq 15 hpes
+  ./hyperqb.sh cases_bmc/NRP_incorrect.smv cases_bmc/NRP_formula.hq 15 hpes
 
 -- 4.2 NRP_correct --
-  ./hyperqube.sh cases_bmc/NRP_correct.smv cases_bmc/NRP_formula.hq 15 hopt
+  ./hyperqb.sh cases_bmc/NRP_correct.smv cases_bmc/NRP_formula.hq 15 hopt
 
 
 
 
 
 [Shortest Path]
 -- Shortest Path 10x10 --
-  ./hyperqube.sh cases_bmc/robotic_sp_100.smv  cases_bmc/robotic_sp_formula.hq 20 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_sp_100.smv  cases_bmc/robotic_sp_formula.hq 20 hpes -find
 
 -- Shortest Path 20x20 --
-  ./hyperqube.sh cases_bmc/robotic_sp_400.smv cases_bmc/robotic_sp_formula.hq 40 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_sp_400.smv cases_bmc/robotic_sp_formula.hq 40 hpes -find
 
 -- Shortest Path 40x40 --
-  ./hyperqube.sh cases_bmc/robotic_sp_1600.smv cases_bmc/robotic_sp_formula.hq 80 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_sp_1600.smv cases_bmc/robotic_sp_formula.hq 80 hpes -find
 
 -- Shortest Path 60x60 --
-  ./hyperqube.sh cases_bmc/robotic_sp_3600.smv cases_bmc/robotic_sp_formula.hq 120 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_sp_3600.smv cases_bmc/robotic_sp_formula.hq 120 hpes -find
 
 
 
 [Initial State Robustness]
 
 -- Robustness 10x10 --
-  ./hyperqube.sh cases_bmc/robotic_robustness_100.smv cases_bmc/robotic_robustness_formula.hq 20 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_robustness_100.smv cases_bmc/robotic_robustness_formula.hq 20 hpes -find
 
 -- Robustness 20x20 --
-  ./hyperqube.sh cases_bmc/robotic_robustness_400.smv cases_bmc/robotic_robustness_formula.hq 40 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_robustness_400.smv cases_bmc/robotic_robustness_formula.hq 40 hpes -find
 
 -- Robustness 40x40 --
-  ./hyperqube.sh cases_bmc/robotic_robustness_1600.smv cases_bmc/robotic_robustness_formula.hq 80 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_robustness_1600.smv cases_bmc/robotic_robustness_formula.hq 80 hpes -find
 
 -- Robustness 60x60 --
-  ./hyperqube.sh cases_bmc/robotic_robustness_3600.smv cases_bmc/robotic_robustness_formula.hq 120 hpes -find
+  ./hyperqb.sh cases_bmc/robotic_robustness_3600.smv cases_bmc/robotic_robustness_formula.hq 120 hpes -find
 
 
 
 [Mutation Testing]
 
-  ./hyperqube.sh cases_bmc/mutation_testing.smv cases_bmc/mutation_testing.hq 10 hpes -find
+  ./hyperqb.sh cases_bmc/mutation_testing.smv cases_bmc/mutation_testing.hq 10 hpes -find