402
S. Akshay et al.
Name Locations Transitions Stacks Clocks cmax Aged(Y/N) Holes Time Empty(mili sec) Time Witness (mili sec) Memory(KB)
Bluetooth
45
89
2
0
2
Y
0
152.8
0.119
5568
L
crit
6
10
2
2
8
Y
2
9965.2
3.7
203396
Maze
9
12
2
2
5
Y
2
349.3
0.31
11604
Table 2. Experimental results of timed examples. The column cmax is defined as the
maximum constant in the automaton, and Aged denotes if the stack is timed or not
Results and Discussion. The performance of BHIM is presented in Table 1
for untimed examples and in Table 2 for timed examples.
Apart from the results in the tables, to check the robustness of BHIM wrt
parameters like the number of locations, transitions, stacks, holes and clocks (for
TMPDA), we looked at examples with an empty language, by making accepting
states non-accepting in the examples considered so far. This forces BHIM to
explore all possible paths in the BFS tree, generating the lists at all nodes. The
scalability of BHIM wrt all these parameters are in [4].
BHIM Vs. State of the art. What makes BHIM stand apart wrt the existing
state of the art tools is that (i) none of the existing tools handle underapproximations captured by bounded holes, (ii) none of the existing tools work with
multiple stacks in the timed setting (even closed guards!). The state of the art
research in underapproximations wrt untimed multistack pushdown systems has
produced some robust tools like GetaFix which handles multi-threaded programs
with bounded context switches. While we have adapted some of the examples
from GetaFix, the latest available version of GetaFix has some issues in handling
those examples
3 . Likewise, SPADE, MAGIC and the counter implementation [16]
are currently not maintained, resulting in a non-comparison of BHIM and these
tools. Most examples handled by BHIM correspond to non-context bounded, or
non-scope bounded, or timed languages which are beyond GetaFix : the 2-hole
bounded witness found by BHIM for the language L 9,5 for the multi producer
consumer case cannot be found by GetaFix/MAGIC/SPADE with less than 90
context switches. In the timed setting, the Maze example which has a 2 holebounded witness where the robot visits certain locations equal number of times
is beyond [6], which can handle only single stack.
7 Future Work
As immediate future work, we are working on BHIM v2 to be symbolic, inspired from GetaFix. The current avatar of BHIM showcases the efficiency of
fix-point techniques extended to larger bounded underapproximations; indeed
going symbolic will make BHIM much more robust and scalable. This version
will also include a parser to handle boolean programs, allowing us to evaluate
larger repositories of available benchmarks.
Acknowledgements. We would like to thank Gennaro Parlato for the discussions
on GetaFix and for providing us benchmarks and anonymous reviewers for more
pointers.
3 we did get in touch with one of the authors, who confirmed this.
S. Akshay et al.
Name Locations Transitions Stacks Clocks cmax Aged(Y/N) Holes Time Empty(mili sec) Time Witness (mili sec) Memory(KB)
Bluetooth
45
89
2
0
2
Y
0
152.8
0.119
5568
L
crit
6
10
2
2
8
Y
2
9965.2
3.7
203396
Maze
9
12
2
2
5
Y
2
349.3
0.31
11604
Table 2. Experimental results of timed examples. The column cmax is defined as the
maximum constant in the automaton, and Aged denotes if the stack is timed or not
Results and Discussion. The performance of BHIM is presented in Table 1
for untimed examples and in Table 2 for timed examples.
Apart from the results in the tables, to check the robustness of BHIM wrt
parameters like the number of locations, transitions, stacks, holes and clocks (for
TMPDA), we looked at examples with an empty language, by making accepting
states non-accepting in the examples considered so far. This forces BHIM to
explore all possible paths in the BFS tree, generating the lists at all nodes. The
scalability of BHIM wrt all these parameters are in [4].
BHIM Vs. State of the art. What makes BHIM stand apart wrt the existing
state of the art tools is that (i) none of the existing tools handle underapproximations captured by bounded holes, (ii) none of the existing tools work with
multiple stacks in the timed setting (even closed guards!). The state of the art
research in underapproximations wrt untimed multistack pushdown systems has
produced some robust tools like GetaFix which handles multi-threaded programs
with bounded context switches. While we have adapted some of the examples
from GetaFix, the latest available version of GetaFix has some issues in handling
those examples
3 . Likewise, SPADE, MAGIC and the counter implementation [16]
are currently not maintained, resulting in a non-comparison of BHIM and these
tools. Most examples handled by BHIM correspond to non-context bounded, or
non-scope bounded, or timed languages which are beyond GetaFix : the 2-hole
bounded witness found by BHIM for the language L 9,5 for the multi producer
consumer case cannot be found by GetaFix/MAGIC/SPADE with less than 90
context switches. In the timed setting, the Maze example which has a 2 holebounded witness where the robot visits certain locations equal number of times
is beyond [6], which can handle only single stack.
7 Future Work
As immediate future work, we are working on BHIM v2 to be symbolic, inspired from GetaFix. The current avatar of BHIM showcases the efficiency of
fix-point techniques extended to larger bounded underapproximations; indeed
going symbolic will make BHIM much more robust and scalable. This version
will also include a parser to handle boolean programs, allowing us to evaluate
larger repositories of available benchmarks.
Acknowledgements. We would like to thank Gennaro Parlato for the discussions
on GetaFix and for providing us benchmarks and anonymous reviewers for more
pointers.
3 we did get in touch with one of the authors, who confirmed this.