---
_id: '631'
abstract:
- lang: eng
  text: Template polyhedra generalize intervals and octagons to polyhedra whose facets
    are orthogonal to a given set of arbitrary directions. They have been employed
    in the abstract interpretation of programs and, with particular success, in the
    reachability analysis of hybrid automata. While previously, the choice of directions
    has been left to the user or a heuristic, we present a method for the automatic
    discovery of directions that generalize and eliminate spurious counterexamples.
    We show that for the class of convex hybrid automata, i.e., hybrid automata with
    (possibly nonlinear) convex constraints on derivatives, such directions always
    exist and can be found using convex optimization. We embed our method inside a
    CEGAR loop, thus enabling the time-unbounded reachability analysis of an important
    and richer class of hybrid automata than was previously possible. We evaluate
    our method on several benchmarks, demonstrating also its superior efficiency for
    the special case of linear hybrid automata.
acknowledgement: This research was supported in part by the Austrian Science Fund
  (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), by
  the European Commission under grant 643921 (UnCoVerCPS), and by the ARC project
  DP140104219 (Robust AI Planning for Hybrid Systems).
alternative_title:
- LNCS
author:
- first_name: Sergiy
  full_name: Bogomolov, Sergiy
  id: 369D9A44-F248-11E8-B48F-1D18A9856A87
  last_name: Bogomolov
  orcid: 0000-0002-0686-0365
- first_name: Goran
  full_name: Frehse, Goran
  last_name: Frehse
- first_name: Mirco
  full_name: Giacobbe, Mirco
  id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
  last_name: Giacobbe
  orcid: 0000-0001-8180-0904
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement
    of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:<a href="https://doi.org/10.1007/978-3-662-54577-5_34">10.1007/978-3-662-54577-5_34</a>'
  apa: 'Bogomolov, S., Frehse, G., Giacobbe, M., &#38; Henzinger, T. A. (2017). Counterexample
    guided refinement of template polyhedra (Vol. 10205, pp. 589–606). Presented at
    the TACAS: Tools and Algorithms for the Construction and Analysis of Systems,
    Uppsala, Sweden: Springer. <a href="https://doi.org/10.1007/978-3-662-54577-5_34">https://doi.org/10.1007/978-3-662-54577-5_34</a>'
  chicago: Bogomolov, Sergiy, Goran Frehse, Mirco Giacobbe, and Thomas A Henzinger.
    “Counterexample Guided Refinement of Template Polyhedra,” 10205:589–606. Springer,
    2017. <a href="https://doi.org/10.1007/978-3-662-54577-5_34">https://doi.org/10.1007/978-3-662-54577-5_34</a>.
  ieee: 'S. Bogomolov, G. Frehse, M. Giacobbe, and T. A. Henzinger, “Counterexample
    guided refinement of template polyhedra,” presented at the TACAS: Tools and Algorithms
    for the Construction and Analysis of Systems, Uppsala, Sweden, 2017, vol. 10205,
    pp. 589–606.'
  ista: 'Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. 2017. Counterexample guided
    refinement of template polyhedra. TACAS: Tools and Algorithms for the Construction
    and Analysis of Systems, LNCS, vol. 10205, 589–606.'
  mla: Bogomolov, Sergiy, et al. <i>Counterexample Guided Refinement of Template Polyhedra</i>.
    Vol. 10205, Springer, 2017, pp. 589–606, doi:<a href="https://doi.org/10.1007/978-3-662-54577-5_34">10.1007/978-3-662-54577-5_34</a>.
  short: S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017,
    pp. 589–606.
conference:
  end_date: 2017-04-29
  location: Uppsala, Sweden
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2017-04-22
date_created: 2018-12-11T11:47:36Z
date_published: 2017-03-31T00:00:00Z
date_updated: 2023-09-07T12:53:00Z
day: '31'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-662-54577-5_34
file:
- access_level: open_access
  checksum: f395d0d20102b89aeaad8b4ef4f18f4f
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:11:41Z
  date_updated: 2020-07-14T12:47:27Z
  file_id: '4897'
  file_name: IST-2017-741-v1+1_main.pdf
  file_size: 569863
  relation: main_file
- access_level: open_access
  checksum: f416ee1ae4497b23ecdf28b1f18bb8df
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:11:42Z
  date_updated: 2020-07-14T12:47:27Z
  file_id: '4898'
  file_name: IST-2018-741-v2+2_main.pdf
  file_size: 563276
  relation: main_file
file_date_updated: 2020-07-14T12:47:27Z
has_accepted_license: '1'
intvolume: '     10205'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 589 - 606
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication_identifier:
  isbn:
  - 978-366254576-8
publication_status: published
publisher: Springer
publist_id: '7162'
pubrep_id: '966'
quality_controlled: '1'
related_material:
  record:
  - id: '6894'
    relation: dissertation_contains
    status: public
scopus_import: 1
status: public
title: Counterexample guided refinement of template polyhedra
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10205
year: '2017'
...