---
_id: '4562'
abstract:
- lang: eng
  text: We present interface models that describe both the input assumptions of a
    component, and its output behavior. By enabling us to check that the input assumptions
    of a component are met in a design, interface models provide a compatibility check
    for component-based design. When refining a design into an implementation, interface
    models require that the output behavior of a component satisfies the design specification
    only when the input assumptions of the specification are satisfied, yielding greater
    flexibility in the choice of implementations. Technically, our interface models
    are games between two players, Input and Output; the duality of the players accounts
    for the dual roles of inputs and outputs in composition and refinement. We present
    two interface models in detail, one for a simple synchronous form of interaction
    between components typical in hardware, and the other for more complex synchronous
    interactions on bidirectional connections. As an example, we specify the interface
    of a bidirectional bus, with the input assumption that at any time at most one
    component has write access to the bus. For these interface models, we present
    algorithms for compatibility and refinement checking, and we describe efficient
    symbolic implementations.
acknowledgement: This research was supported in part by the AFOSR grant F49620-00-1-0327,
  the DARPA grant F33615-00-C-1693, the MARCO grant 98-DT-660, the NSF grant CCR-9988172,
  the SRC grant 99-TJ-683.003, and the NSF CAREER award CCR-0132780.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Arindam
  full_name: Chakrabarti, Arindam
  last_name: Chakrabarti
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- 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: Freddy
  full_name: Mang, Freddy
  last_name: Mang
citation:
  ama: 'Chakrabarti A, De Alfaro L, Henzinger TA, Mang F. Synchronous and bidirectional
    component interfaces. In: <i>Proceedings of the 14th International Conference
    on Computer Aided Verification</i>. Vol 2404. Springer; 2002:414-427. doi:<a href="https://doi.org/10.1007/3-540-45657-0_34">10.1007/3-540-45657-0_34</a>'
  apa: 'Chakrabarti, A., De Alfaro, L., Henzinger, T. A., &#38; Mang, F. (2002). Synchronous
    and bidirectional component interfaces. In <i>Proceedings of the 14th International
    Conference on Computer Aided Verification</i> (Vol. 2404, pp. 414–427). Copenhagen,
    Denmark: Springer. <a href="https://doi.org/10.1007/3-540-45657-0_34">https://doi.org/10.1007/3-540-45657-0_34</a>'
  chicago: Chakrabarti, Arindam, Luca De Alfaro, Thomas A Henzinger, and Freddy Mang.
    “Synchronous and Bidirectional Component Interfaces.” In <i>Proceedings of the
    14th International Conference on Computer Aided Verification</i>, 2404:414–27.
    Springer, 2002. <a href="https://doi.org/10.1007/3-540-45657-0_34">https://doi.org/10.1007/3-540-45657-0_34</a>.
  ieee: A. Chakrabarti, L. De Alfaro, T. A. Henzinger, and F. Mang, “Synchronous and
    bidirectional component interfaces,” in <i>Proceedings of the 14th International
    Conference on Computer Aided Verification</i>, Copenhagen, Denmark, 2002, vol.
    2404, pp. 414–427.
  ista: 'Chakrabarti A, De Alfaro L, Henzinger TA, Mang F. 2002. Synchronous and bidirectional
    component interfaces. Proceedings of the 14th International Conference on Computer
    Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404, 414–427.'
  mla: Chakrabarti, Arindam, et al. “Synchronous and Bidirectional Component Interfaces.”
    <i>Proceedings of the 14th International Conference on Computer Aided Verification</i>,
    vol. 2404, Springer, 2002, pp. 414–27, doi:<a href="https://doi.org/10.1007/3-540-45657-0_34">10.1007/3-540-45657-0_34</a>.
  short: A. Chakrabarti, L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of
    the 14th International Conference on Computer Aided Verification, Springer, 2002,
    pp. 414–427.
conference:
  end_date: 2002-07-31
  location: Copenhagen, Denmark
  name: 'CAV: Computer Aided Verification'
  start_date: 2002-07-27
date_created: 2018-12-11T12:09:29Z
date_published: 2002-06-19T00:00:00Z
date_updated: 2023-06-02T12:01:22Z
day: '19'
doi: 10.1007/3-540-45657-0_34
extern: '1'
intvolume: '      2404'
language:
- iso: eng
month: '06'
oa_version: None
page: 414 - 427
publication: Proceedings of the 14th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540439974'
publication_status: published
publisher: Springer
publist_id: '146'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synchronous and bidirectional component interfaces
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2404
year: '2002'
...
---
_id: '4472'
abstract:
- lang: eng
  text: 'We present a methodology and tool for verifying and certifying systems code.
    The verification is based on the lazy-abstraction paradigm for intertwining the
    following three logical steps: construct a predicate abstraction from the code,
    model check the abstraction, and automatically refine the abstraction based on
    counterexample analysis. The certification is based on the proof-carrying code
    paradigm. Lazy abstraction enables the automatic construction of small proof certificates.
    The methodology is implemented in Blast, the Berkeley Lazy Abstraction Software
    verification Tool. We describe our experience applying Blast to Linux and Windows
    device drivers. Given the C code for a driver and for a temporal-safety monitor,
    Blast automatically generates an easily checkable correctness certificate if the
    driver satisfies the specification, and an error trace otherwise.'
acknowledgement: This work was supported in part by the NSF ITR grants CCR-0085949,
  CCR-0081588, the NSF Career grant CCR-9875171, the DARPA PCES grant F33615-00-C-1693,
  the MARCO GSRC grant 98-DT-660, the SRC contract 99-TJ-683, a Microsoft fellowship,
  and gifts from AT&T Research and Microsoft Research.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: George
  full_name: Necula, George
  last_name: Necula
- first_name: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Grégoire
  full_name: Sutre, Grégoire
  last_name: Sutre
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Westley
  full_name: Weimer, Westley
  last_name: Weimer
citation:
  ama: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. Temporal safety
    proofs for systems code. In: <i>Proceedings of the 14th International Conference
    on Computer Aided Verification</i>. Vol 2404. Springer; 2002:526-538. doi:<a href="https://doi.org/10.1007/3-540-45657-0_45">10.1007/3-540-45657-0_45</a>'
  apa: 'Henzinger, T. A., Necula, G., Jhala, R., Sutre, G., Majumdar, R., &#38; Weimer,
    W. (2002). Temporal safety proofs for systems code. In <i>Proceedings of the 14th
    International Conference on Computer Aided Verification</i> (Vol. 2404, pp. 526–538).
    Copenhagen, Denmark: Springer. <a href="https://doi.org/10.1007/3-540-45657-0_45">https://doi.org/10.1007/3-540-45657-0_45</a>'
  chicago: Henzinger, Thomas A, George Necula, Ranjit Jhala, Grégoire Sutre, Ritankar
    Majumdar, and Westley Weimer. “Temporal Safety Proofs for Systems Code.” In <i>Proceedings
    of the 14th International Conference on Computer Aided Verification</i>, 2404:526–38.
    Springer, 2002. <a href="https://doi.org/10.1007/3-540-45657-0_45">https://doi.org/10.1007/3-540-45657-0_45</a>.
  ieee: T. A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, and W. Weimer,
    “Temporal safety proofs for systems code,” in <i>Proceedings of the 14th International
    Conference on Computer Aided Verification</i>, Copenhagen, Denmark, 2002, vol.
    2404, pp. 526–538.
  ista: 'Henzinger TA, Necula G, Jhala R, Sutre G, Majumdar R, Weimer W. 2002. Temporal
    safety proofs for systems code. Proceedings of the 14th International Conference
    on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 2404,
    526–538.'
  mla: Henzinger, Thomas A., et al. “Temporal Safety Proofs for Systems Code.” <i>Proceedings
    of the 14th International Conference on Computer Aided Verification</i>, vol.
    2404, Springer, 2002, pp. 526–38, doi:<a href="https://doi.org/10.1007/3-540-45657-0_45">10.1007/3-540-45657-0_45</a>.
  short: T.A. Henzinger, G. Necula, R. Jhala, G. Sutre, R. Majumdar, W. Weimer, in:,
    Proceedings of the 14th International Conference on Computer Aided Verification,
    Springer, 2002, pp. 526–538.
conference:
  end_date: 2002-07-31
  location: Copenhagen, Denmark
  name: 'CAV: Computer Aided Verification'
  start_date: 2002-07-27
date_created: 2018-12-11T12:09:01Z
date_published: 2002-06-19T00:00:00Z
date_updated: 2023-06-05T08:11:32Z
day: '19'
doi: 10.1007/3-540-45657-0_45
extern: '1'
intvolume: '      2404'
language:
- iso: eng
month: '06'
oa_version: None
page: 526 - 538
publication: Proceedings of the 14th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540439974'
publication_status: published
publisher: Springer
publist_id: '258'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal safety proofs for systems code
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2404
year: '2002'
...