跳到主要內容區塊
:::
開啟
:::
資訊科學研究所

博士後研究員,專任研究助理,獎助生

  • 職務說明
    1. 單位

      資訊科學研究所

    2. 職務名稱

      博士後研究員,專任研究助理,獎助生

    3. 工作內容

      從事 形式化驗證(formal verification)在
      1. 量子軟體系統
      2. 儲存系統
      的相關研究。

      形式化驗證是一個開發高品質軟體的方法。

      這方法會要求使用者提供他程式碼的"規格"。一個常見的方式,是用前置-後置條件來描述此規格,對一個排序的程式而言,我們會要求其前置條件是"輸入為一個整數序列",而其後置條件為"回傳值回輸入序列經過由小到大重新排列的結果"。當然,是用電腦能看懂的語言表示。

      之後,形式化驗證會用嚴謹的數學方法和電腦工具,"證明"一個該程式是否滿足該規格。這方法已經被很多歐美頂尖企業採用,例如微軟使用它來檢驗協力廠商所撰寫的驅動程式,AWS也大量採用他來驗證其雲端系統。AWS的CTO甚至在AWS 2020的開發者會議上,花了他整個演講1/3的時間,來解釋AWS如何用形式化驗證提高其服務品質。

      本實驗室從事形式化驗證已經研究已經有十多年的時間,在全世界同行中也有相當的知名度。目前我們研究主軸在兩個方向:

      [量子軟體系統驗證]
      隨著量子電腦硬體的逐漸成熟,對應的量子軟體開發技術也日益受到重視。可以預見的,軟體的規模會不斷地增加,確保設計出來的程式正確無誤的難度也會高速提升。這現象在傳統軟體已經很普遍,任何有一定規模的軟體程式,無可避免的都會有大大小小的錯誤,最後只能和這些錯誤共存。我們相信如果沒有引入新的技術,很快量子軟體也會走向這條路。

      形式化驗證在量子程式的發展也已經有十數年。目前主流的技術有兩大缺點,基於霍爾邏輯的技術有強大的能力,能處理十分複雜的量子程式分析,但是他的使用需要大量人力介入,需要的工作量常常是寫程式本身的數倍。這樣的技術比較適合用在確保關鍵系統的品質上(如核電廠的控制程式)。基於抽象解釋的技術則是另一個極端。他是全自動的,但是有著常常誤報程式錯誤的缺點。這大大減低的該類工具的可用性。

      最近中研院的團隊開發了一個基於樹自動機(tree automata)的全新量子電路驗證技術。他克服了上述兩個問題。這是一個全自動的技術,使用者只需要提供電路和預期的答案,該技術就能自動檢查,對所有允許的起始量子狀態,有沒有任何的可能,在執行完電路後產生和預期不同的結果。同時這樣技術是精確的,他完全不會誤報錯誤,大大的增加了可用性。

      有關於這個方向,還可以參考Quantum Computer Systems: Research for Noisy Intermediate-Scale Quantum Computers一書 的Ch 5,6,9來得到大概輪廓(連結:https://www.morganclaypool.com/doi/abs/10.2200/S01014ED1V01Y202005CAC051)。
      下面是一些和我們近期研究題目相關的參考文獻:
      [1] Yuan-Hung Tsai, Jie-Hong R. Jiang, Chiao-Shan Jhang: Bit-Slicing the Hilbert Space: Scaling Up Accurate Quantum Circuit Simulation. DAC 2021: 439-444
      [2] Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, Julien d'Orso: Regular Tree Model Checking. CAV 2002: 555-568
      [3]https://zxcalculus.com
      [4]Miller, D. Michael, and Mitchell A. Thornton. "QMDD: A decision diagram structure for reversible and quantum circuits." 36th International Symposium on Multiple-Valued Logic (ISMVL'06). IEEE, 2006.
      [5]Mingsheng Ying. 2012. Floyd--hoare logic for quantum programs. ACM Trans. Programming Language System

      [儲存系統驗證]
      可參考我們發表在OSDI的論文:
      [1] Yun-Sheng Chang, Yao Hsiao, Tzu-Chi Lin, Che-Wei Tsao, Chun-Feng Wu, Yuan-Hao Chang, Hsiang-Shang Ko, Yu-Fang Chen:
      Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer. OSDI 2020: 81-97

      和下面相關文獻:
      [2] Abdulla, P.A., Haziza, F., Holík, L. et al. An integrated specification and verification technique for highly concurrent data structures. Int J Softw. Tools. Technol. Transfer. 19, 549–563 (2017).
      [3] Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang:
      Scaling symbolic evaluation for automated verification of systems code with Serval. SOSP 2019: 225-242
      [4] Frama-c WP tutorial (https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf)
      [5] Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich:
      Verifying concurrent, crash-safe systems with Perennial. SOSP 2019: 243-258

    4. 應徵資格

      1. 具電機、資訊、資管、數學或相關科系畢業之博士/碩士/學士/在學學生
      2. 曾修過下列課程者加分: 計算理論, 自動機理論, 模型驗證, 自動化驗證,台大Flolac暑期課程
      3. 具有程式撰寫能力(C, C++, or JAVA)也是加分項目

  • 工作環境
    1. 工作時間

      依中研院規定

    2. 工作地點

      中研院資訊所

    3. 待遇

      專任薪資:學士37240元起薪,碩士43624元起薪,博士62776元起薪,該職缺係「適用勞動基準法」;獎助生依本院獎助學金支給要點發放獎助學金

    4. 福利

    5. 參考網站 http://iis.sinica.edu.tw/~yfc
  • 受理方式
    1. 聯絡人

      陳老師

    2. 聯絡地址

      北市南港區研究院路二段128號資訊所

    3. 聯絡電話

      27883799 分機1514

    4. 電子信箱 yfc@iis.sinica.edu.tw
    5. 應備文件

      將個人詳細履歷,大學及以上成績單、發表過之論文、及任何有助審查資料 Email至 陳郁方研究員 yfc@iis.sinica.edu.tw。如通過初審將會另行通知面試。

    6. 應徵注意事項

  • 日期
    1. 刊登日期

      2022-08-12

    2. 截止日期

      2025-12-15

回頂端