[{"date_created":"2018-12-11T12:09:33Z","title":"Lazy shape analysis","_id":"4574","author":[{"first_name":"Dirk","full_name":"Beyer, Dirk","last_name":"Beyer"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"last_name":"Théoduloz","full_name":"Théoduloz, Grégory","first_name":"Grégory"}],"date_updated":"2026-08-21T09:37:53Z","OA_type":"closed access","alternative_title":["LNCS"],"publist_id":"133","extern":"1","publication_identifier":{"isbn":["9783540374060"],"eisbn":["9783540374114"]},"page":"532 - 546","volume":4144,"intvolume":"      4144","month":"08","date_published":"2006-08-08T00:00:00Z","abstract":[{"text":"Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker Blast. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending Blast with calls to Tvla.","lang":"eng"}],"day":"08","publisher":"Springer","type":"conference","doi":"10.1007/11817963_48","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","language":[{"iso":"eng"}],"article_processing_charge":"No","citation":{"apa":"Beyer, D., Henzinger, T. A., &#38; Théoduloz, G. (2006). Lazy shape analysis. In <i>Proceedings of the 18th international conference on Computer Aided Verification</i> (Vol. 4144, pp. 532–546). Seattle, WA, United States: Springer. <a href=\"https://doi.org/10.1007/11817963_48\">https://doi.org/10.1007/11817963_48</a>","ieee":"D. Beyer, T. A. Henzinger, and G. Théoduloz, “Lazy shape analysis,” in <i>Proceedings of the 18th international conference on Computer Aided Verification</i>, Seattle, WA, United States, 2006, vol. 4144, pp. 532–546.","chicago":"Beyer, Dirk, Thomas A Henzinger, and Grégory Théoduloz. “Lazy Shape Analysis.” In <i>Proceedings of the 18th International Conference on Computer Aided Verification</i>, 4144:532–46. Springer, 2006. <a href=\"https://doi.org/10.1007/11817963_48\">https://doi.org/10.1007/11817963_48</a>.","short":"D. Beyer, T.A. Henzinger, G. Théoduloz, in:, Proceedings of the 18th International Conference on Computer Aided Verification, Springer, 2006, pp. 532–546.","ama":"Beyer D, Henzinger TA, Théoduloz G. Lazy shape analysis. In: <i>Proceedings of the 18th International Conference on Computer Aided Verification</i>. Vol 4144. Springer; 2006:532-546. doi:<a href=\"https://doi.org/10.1007/11817963_48\">10.1007/11817963_48</a>","mla":"Beyer, Dirk, et al. “Lazy Shape Analysis.” <i>Proceedings of the 18th International Conference on Computer Aided Verification</i>, vol. 4144, Springer, 2006, pp. 532–46, doi:<a href=\"https://doi.org/10.1007/11817963_48\">10.1007/11817963_48</a>.","ista":"Beyer D, Henzinger TA, Théoduloz G. 2006. Lazy shape analysis. Proceedings of the 18th international conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 4144, 532–546."},"year":"2006","status":"public","publication_status":"published","oa_version":"None","conference":{"start_date":"2006-08-17","name":"CAV: Computer Aided Verification","end_date":"2006-08-20","location":"Seattle, WA, United States"},"publication":"Proceedings of the 18th international conference on Computer Aided Verification"},{"abstract":[{"lang":"eng","text":"We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata."}],"intvolume":"      4144","month":"08","volume":4144,"page":"17 - 30","OA_type":"closed access","title":"Antichains: A new algorithm for checking universality of finite automata","_id":"4406","date_updated":"2026-08-21T11:47:59Z","oa_version":"None","acknowledgement":"This research was supported in part by the NSF grants CCR-0234690 and CCR-0225610, and the Belgian FNRS grant 2.4530.02 of the FRFC project “Centre Fédéré en Vérification.”","year":"2006","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publisher":"Springer Nature","day":"08","date_published":"2006-08-08T00:00:00Z","publist_id":"326","extern":"1","publication_identifier":{"eisbn":["9783540374114"],"isbn":["9783540374060"],"eissn":["1611-3349"],"issn":["0302-9743"]},"alternative_title":["LNCS"],"author":[{"last_name":"De Wulf","full_name":"De Wulf, Martin","first_name":"Martin"},{"last_name":"Doyen","full_name":"Doyen, Laurent","first_name":"Laurent"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"}],"date_created":"2018-12-11T12:08:41Z","conference":{"start_date":"2006-08-17","end_date":"2006-08-20","name":"CAV: Computer Aided Verification","location":"Seattle, WA, United States"},"publication":"Proceedings of the 18th international conference on Computer Aided Verification","publication_status":"published","status":"public","article_processing_charge":"No","citation":{"chicago":"De Wulf, Martin, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Antichains: A New Algorithm for Checking Universality of Finite Automata.” In <i>Proceedings of the 18th International Conference on Computer Aided Verification</i>, 4144:17–30. Springer Nature, 2006. <a href=\"https://doi.org/10.1007/11817963_5\">https://doi.org/10.1007/11817963_5</a>.","short":"M. De Wulf, L. Doyen, T.A. Henzinger, J. Raskin, in:, Proceedings of the 18th International Conference on Computer Aided Verification, Springer Nature, 2006, pp. 17–30.","apa":"De Wulf, M., Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2006). Antichains: A new algorithm for checking universality of finite automata. In <i>Proceedings of the 18th international conference on Computer Aided Verification</i> (Vol. 4144, pp. 17–30). Seattle, WA, United States: Springer Nature. <a href=\"https://doi.org/10.1007/11817963_5\">https://doi.org/10.1007/11817963_5</a>","ieee":"M. De Wulf, L. Doyen, T. A. Henzinger, and J. Raskin, “Antichains: A new algorithm for checking universality of finite automata,” in <i>Proceedings of the 18th international conference on Computer Aided Verification</i>, Seattle, WA, United States, 2006, vol. 4144, pp. 17–30.","mla":"De Wulf, Martin, et al. “Antichains: A New Algorithm for Checking Universality of Finite Automata.” <i>Proceedings of the 18th International Conference on Computer Aided Verification</i>, vol. 4144, Springer Nature, 2006, pp. 17–30, doi:<a href=\"https://doi.org/10.1007/11817963_5\">10.1007/11817963_5</a>.","ista":"De Wulf M, Doyen L, Henzinger TA, Raskin J. 2006. Antichains: A new algorithm for checking universality of finite automata. Proceedings of the 18th international conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 4144, 17–30.","ama":"De Wulf M, Doyen L, Henzinger TA, Raskin J. Antichains: A new algorithm for checking universality of finite automata. In: <i>Proceedings of the 18th International Conference on Computer Aided Verification</i>. Vol 4144. Springer Nature; 2006:17-30. doi:<a href=\"https://doi.org/10.1007/11817963_5\">10.1007/11817963_5</a>"},"language":[{"iso":"eng"}],"type":"conference","doi":"10.1007/11817963_5"}]