---
OA_type: closed access
_id: '4574'
abstract:
- lang: eng
  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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Grégory
  full_name: Théoduloz, Grégory
  last_name: Théoduloz
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  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.
conference:
  end_date: 2006-08-20
  location: Seattle, WA, United States
  name: 'CAV: Computer Aided Verification'
  start_date: 2006-08-17
date_created: 2018-12-11T12:09:33Z
date_published: 2006-08-08T00:00:00Z
date_updated: 2026-08-21T09:37:53Z
day: '08'
doi: 10.1007/11817963_48
extern: '1'
intvolume: '      4144'
language:
- iso: eng
month: '08'
oa_version: None
page: 532 - 546
publication: Proceedings of the 18th international conference on Computer Aided Verification
publication_identifier:
  eisbn:
  - '9783540374114'
  isbn:
  - '9783540374060'
publication_status: published
publisher: Springer
publist_id: '133'
status: public
title: Lazy shape analysis
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4144
year: '2006'
...
---
OA_type: closed access
_id: '4406'
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.
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.”
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Martin
  full_name: De Wulf, Martin
  last_name: De Wulf
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jean
  full_name: Raskin, Jean
  last_name: Raskin
citation:
  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>'
  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>'
  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>.'
  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.'
  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.'
  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>.'
  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.
conference:
  end_date: 2006-08-20
  location: Seattle, WA, United States
  name: 'CAV: Computer Aided Verification'
  start_date: 2006-08-17
date_created: 2018-12-11T12:08:41Z
date_published: 2006-08-08T00:00:00Z
date_updated: 2026-08-21T11:47:59Z
day: '08'
doi: 10.1007/11817963_5
extern: '1'
intvolume: '      4144'
language:
- iso: eng
month: '08'
oa_version: None
page: 17 - 30
publication: Proceedings of the 18th international conference on Computer Aided Verification
publication_identifier:
  eisbn:
  - '9783540374114'
  eissn:
  - 1611-3349
  isbn:
  - '9783540374060'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
publist_id: '326'
status: public
title: 'Antichains: A new algorithm for checking universality of finite automata'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4144
year: '2006'
...