Contents

Click a page name

Tamir Heyman1,2, Shoham Ben-David2, Orna Grumberg1, Assaf Schuster1 Technion I 
Model checking Gets a model and verifies that it obeys a given specification S 
Distributed Symbolic Reachability Analysis Heyman et al.CAV 2000 On-The-Fly Sy 
Novel Elements in our approach 
What is On-The-Fly Symbolic Model Checking? 
Specify what should never hold Temporal-logic describes what should hold Desc 
Translate an RE specification r to an automaton Ar Hopcroft and Ullman 79 M sa 
Starting BFS by a single process Until reaching a threshold  
Dividing the work Dividing the state space into slices owned by process. 
BFS on the slices Exchange nonowned states.  
Dynamic balance Re-partition the biggest slice with the smallest one 
Storing the doughnuts Each process Pj stores, for each doughnut i the slice S(i 
Counter example generation Choose bad state, compute predecessors, cut with pro 
Peak size 
Distributed On-The-Fly Model Checking None of the process has the entire sets  
Improve memory balancing scheme Get better reduction during step computation M 
Dividing one set of states into two smaller sets Many options, heuristic approa 
Slice f into two sets using variable v A "good" slicing reduces size without  
Boolean Function Slicing: Cost function [Cabodi et.al. 96, Narayan et.al. 97] 
Boolean Function Slicing: Cost function [Cabodi et.al. 96, Narayan et.al. 97] 
Slicing Algorithm with Adaptive alpha  
Reduction is (original size) / (largest slice size) Good example: ARB 5th step 
Memory utilization by BIQ, Using 32 processors