[{"extern":"1","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.","volume":2404,"date_updated":"2023-06-02T12:01:22Z","year":"2002","citation":{"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.","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>.","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>","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>","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.","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.","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>."},"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."}],"doi":"10.1007/3-540-45657-0_34","day":"19","page":"414 - 427","quality_controlled":"1","publisher":"Springer","author":[{"last_name":"Chakrabarti","first_name":"Arindam","full_name":"Chakrabarti, Arindam"},{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"full_name":"Mang, Freddy","last_name":"Mang","first_name":"Freddy"}],"_id":"4562","scopus_import":"1","title":"Synchronous and bidirectional component interfaces","alternative_title":["LNCS"],"intvolume":"      2404","publication_status":"published","article_processing_charge":"No","date_created":"2018-12-11T12:09:29Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","date_published":"2002-06-19T00:00:00Z","type":"conference","publist_id":"146","publication_identifier":{"isbn":["9783540439974"]},"language":[{"iso":"eng"}],"conference":{"start_date":"2002-07-27","name":"CAV: Computer Aided Verification","end_date":"2002-07-31","location":"Copenhagen, Denmark"},"publication":"Proceedings of the 14th International Conference on Computer Aided Verification","month":"06","oa_version":"None"},{"abstract":[{"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.","lang":"eng"}],"day":"19","doi":"10.1007/3-540-45657-0_45","year":"2002","citation":{"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.","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>.","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.","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."},"date_updated":"2023-06-05T08:11:32Z","extern":"1","volume":2404,"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.","intvolume":"      2404","alternative_title":["LNCS"],"title":"Temporal safety proofs for systems code","date_created":"2018-12-11T12:09:01Z","article_processing_charge":"No","publication_status":"published","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Necula, George","first_name":"George","last_name":"Necula"},{"full_name":"Jhala, Ranjit","last_name":"Jhala","first_name":"Ranjit"},{"first_name":"Grégoire","last_name":"Sutre","full_name":"Sutre, Grégoire"},{"last_name":"Majumdar","first_name":"Ritankar","full_name":"Majumdar, Ritankar"},{"last_name":"Weimer","first_name":"Westley","full_name":"Weimer, Westley"}],"scopus_import":"1","_id":"4472","publisher":"Springer","quality_controlled":"1","page":"526 - 538","publist_id":"258","publication_identifier":{"isbn":["9783540439974"]},"type":"conference","date_published":"2002-06-19T00:00:00Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","month":"06","oa_version":"None","publication":"Proceedings of the 14th International Conference on Computer Aided Verification","conference":{"start_date":"2002-07-27","name":"CAV: Computer Aided Verification","end_date":"2002-07-31","location":"Copenhagen, Denmark"},"language":[{"iso":"eng"}]}]