University of Minnesota
Software Engineering Center
/

You are here

Automatic Abstraction for Model Checking Software Systems with Interrelated Numeric Constraints

Date of Publication: 
September 2001
Associated Research Groups: 
Publication Files: 
Abstract: 
Model checking techniques have not been effective in important classes of software systems characterized by large (or infinite) input domains with interrelated linear and non-linear constraints over the input variables. Various model abstraction techniques have been proposed to address this problem. In this paper, we wish to propose domain abstraction based on data equivalence and trajectory reduction as an alternative and complement to other abstraction techniques. Our technique applies the abstraction to the input domain (environment) instead of the model and is applicable to constraint-free and deterministic constrained data transition system. Our technique is automatable with some minor restrictions.
Venue: 
Proceedings of the Ninth ACM/SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2001)}, Vienna, Austria, September 2001.
bibtex: 
@InProceedings{CRH01, author = {Yunja Choi and Sanjai Rayadurgam and Mats Heimdahl}, title = {Automatic Abstraction for Model Checking Software Systems with Interrelated Numeric Constraints}, booktitle = {Proceedings of the 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE-9)}, pages = {164-174}, year = 2001, number = {}, series = {}, month = {September}, address = {}, annote = {\commentyunja{}} }