Choi, YunjaHeimdahl, Mats2020-12-102020-12-102003Proceedings of the 18th IEEE International Conference on Automated Software Engineering - Short paper session. Montreal, Canada, October 2003.https://hdl.handle.net/11299/217334Associated research group: Critical Systems Research GroupAs an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice. To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time---a feature suitable for regression verification.Report