• 中欧班列让开放之路越走越宽 2019-04-13
  • “电商定制”价廉未必物美 成为“低价劣质”代名词 2019-04-13
  • 菜鸟世界杯送出50吨包裹-热门标签-华商网数码 2019-04-12
  • 曾祖父、曾祖母、祖父、祖母、父亲、母亲、重孙。一家7人,如果两家联姻,两家共十四人,请问:“看着就想笑”你那15人是咋算出来的? 2019-04-12
  • 权威解读!养老保险基金 中央怎么调剂? 2019-04-10
  • 欢乐“粽”情过端午 尽情放“粽”嗨起来 2019-04-05
  • 南昌重拳整治酒驾毒驾 2019-04-04
  • 德国:网上发布不当言论最高可获刑5年 2019-04-04
  • 哭泣的是鸿茅药酒,受伤的是中华医药!(原创首发) 2019-04-01
  • 不动产登记全国联网 名下多少套房一查就知道 2019-04-01
  • 重庆市南川区:社区“法律诊所”推进普法依法治理 2019-03-29
  • 国家税务总局天津市税务局正式对外挂牌 2019-03-29
  • 新华保险荆州中支助力首届荆楚文化旅游节开幕 2019-03-24
  • 英媒美国父母诉诸法院赶走"啃老"子女 中英均有类似问题 2019-03-24
  • 吕梁:女子被贴罚单心怀不满 朋友圈恶意辱警被查 2019-01-10
  • [09-13] A Verified Implementation of the Bounded List Container

    文章来源:  |  发布时间:2018-09-13  |  【打印】 【关闭

      

    全程打闲一年100万 www.edria.net Title: A Verified Implementation of the Bounded List Container

    Speaker: Mihaela Sighireanu, IRIF, University of Paris Diderot (Paris7), France.

    Time: 3:00 pm, September 13th (Thursday), 2018.

    Venue: Lecture room (334), 3rd Floor, Building 5, Software Park, Chinese Academy of Sciences.

    Abstract:

      I will present a work that contributes to the trend of providing fully verified container libraries. We consider an implementation of the bounded doubly linked list container which manages the list in a fixed size, heap allocated array. The container provides constant time methods to update the list by adding, deleting, and changing elements, as well as cursors for list traversal and access to elements. The library is implemented in C, but we wrote the code and its specification by imitating the ones provided by GNAT for the standard library of Ada 2012. The proof of functional correctness is done using VeriFast, which provides an auto-active verification environment for Separation Logic extended with algebraic data types. The specifications proved entail the contracts of the Ada library and include new features. The verification method we used employs a precise algebraic model of the data structure and we show that it facilitates the verification and captures entirely the library contracts. This case study may be of interest for other verification platforms, thus we highlight the intricate points of its proof.

      This is a joint work with R. Cauderlier, published at TACAS 2018.

    Short biography:

      Mihaela Sighireanu is associate professor at University of Paris Diderot and member of the IRIF. She did a PHD on the definition of formal modelling language based on timed process algebras at INRIA Rhone-Alpes. She obtained an habilitation on directed research on automated verification (by static analysis or deductive verification) of programs manipulating the heap. She developed several tools for analysing C programs and for solving entailment problems in separation logic.

  • 中欧班列让开放之路越走越宽 2019-04-13
  • “电商定制”价廉未必物美 成为“低价劣质”代名词 2019-04-13
  • 菜鸟世界杯送出50吨包裹-热门标签-华商网数码 2019-04-12
  • 曾祖父、曾祖母、祖父、祖母、父亲、母亲、重孙。一家7人,如果两家联姻,两家共十四人,请问:“看着就想笑”你那15人是咋算出来的? 2019-04-12
  • 权威解读!养老保险基金 中央怎么调剂? 2019-04-10
  • 欢乐“粽”情过端午 尽情放“粽”嗨起来 2019-04-05
  • 南昌重拳整治酒驾毒驾 2019-04-04
  • 德国:网上发布不当言论最高可获刑5年 2019-04-04
  • 哭泣的是鸿茅药酒,受伤的是中华医药!(原创首发) 2019-04-01
  • 不动产登记全国联网 名下多少套房一查就知道 2019-04-01
  • 重庆市南川区:社区“法律诊所”推进普法依法治理 2019-03-29
  • 国家税务总局天津市税务局正式对外挂牌 2019-03-29
  • 新华保险荆州中支助力首届荆楚文化旅游节开幕 2019-03-24
  • 英媒美国父母诉诸法院赶走"啃老"子女 中英均有类似问题 2019-03-24
  • 吕梁:女子被贴罚单心怀不满 朋友圈恶意辱警被查 2019-01-10