@inproceedings{4562,
  abstract     = {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.},
  author       = {Chakrabarti, Arindam and De Alfaro, Luca and Henzinger, Thomas A and Mang, Freddy},
  booktitle    = {Proceedings of the 14th International Conference on Computer Aided Verification},
  isbn         = {9783540439974},
  location     = {Copenhagen, Denmark},
  pages        = {414 -- 427},
  publisher    = {Springer},
  title        = {{Synchronous and bidirectional component interfaces}},
  doi          = {10.1007/3-540-45657-0_34},
  volume       = {2404},
  year         = {2002},
}

@inproceedings{4472,
  abstract     = {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.},
  author       = {Henzinger, Thomas A and Necula, George and Jhala, Ranjit and Sutre, Grégoire and Majumdar, Ritankar and Weimer, Westley},
  booktitle    = {Proceedings of the 14th International Conference on Computer Aided Verification},
  isbn         = {9783540439974},
  location     = {Copenhagen, Denmark},
  pages        = {526 -- 538},
  publisher    = {Springer},
  title        = {{Temporal safety proofs for systems code}},
  doi          = {10.1007/3-540-45657-0_45},
  volume       = {2404},
  year         = {2002},
}