中央研究院 Logo

從事 形式化驗證(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

從事深度學習於電腦視覺相關研究。詳細內容包含人臉辨識、動作識別、物體偵測和追蹤、基於生成模型(Diffusion model, GAN, etc)之圖片影片及3D生成和檢測等多模態生成式AI、視覺與語言之多模態模型、對抗樣本、或其他電腦視覺與人工智慧安全(AI Security)相關研究，視應徵者背景及能力而定。

全球氣候變遷所帶來的氣候暖化已成為人類發展面臨的迫切挑戰。為了達成國際社會所訂定的2050年碳零排放共同目標，我們的研究團隊專注於生質催化裂解技術和鋰離子電池領域。生質裂解是一種將生物質轉化為碳氫化合物的技術，對於碳中和及能源轉型至關重要。我們目前已有初步的研究結果，隨著研發技術的成熟，將朝創新產業發展，使這項技術達成商業化或自動化運作。我們正在網羅相關領域的博士、碩士、學士級人才及大學實習生加入。

1.資訊安全相關領域的實務及學術性研究
2.資訊安全相關系統開發與實作
3.計畫管理與研究報告論文撰寫
4.其他交辦事項

培養新世紀資料科學與智慧醫療人才

計畫介紹：結合資料科學與人工智慧，並與生物醫學與智慧醫療領域的專家密切合作，以科學化方法將數據轉化成知識並產品落地。

工作內容：資料科學與人工智慧之智慧醫療研究與應用
(1) 學習各式大數據與分析（各式體學、醫療影像、文字探勘、行為環境、人體生物資料庫等）
(2) 程式撰寫與軟體系統開發
(3) 生物資料庫之資訊探勘與建置

參考網站：http://sites.stat.sinica.edu.tw/SH/ & https://www.stat.sinica.edu.tw/hsinchou/

從事 Wireless Communications (e.g., MIMO communication, RIS communication, integrated sensing and communication, satellite communication, semantic communication), Machine Learning in Communications and Networking (e.g., wireless-empowered federated learning) 等相關領域之研究及論文發表。

從事深度學習於電腦視覺相關研究。詳細內容包含人臉辨識、動作識別、物體偵測和追蹤、基於生成模型(Diffusion model, GAN, etc)之圖片影片及3D生成和檢測等多模態生成式AI、視覺與語言之多模態模型、對抗樣本、或其他電腦視覺與人工智慧安全(AI Security)相關研究，視應徵者背景及能力而定。

從事 Wireless Communications (e.g., MIMO communication, RIS communication, integrated sensing and communication, satellite communication, semantic communication), Machine Learning in Communications and Networking (e.g., wireless-empowered federated learning) 等相關領域之研究及論文發表。

從事 Wireless Communications (e.g., MIMO communication, RIS communication, integrated sensing and communication, satellite communication, semantic communication), Machine Learning in Communications and Networking (e.g., wireless-empowered federated learning) 等相關領域之研究及論文發表。

- 在教授指導下進行統計大數據分析的專題研究
- 可選擇研究主題: 實驗設計和分析, 網絡結構和資料分析, 最佳化方法應用, 大數據分析, 深度學習方法和應用, 分子優化, 等等.
- 撰寫和發表研究論文, 編寫程式和電腦模擬, 參加國際會議.
- 臨時交辦事項

利用統計、機器學習、與深度學習，解析國內外大型資料庫資訊，並與醫學中心跨領域專家密切合作，實際應用於精準醫療與智慧健康，創造資料價值。

(1) 巨量資料分析（基因體等各式體學、行為環境、電子病歷、文字資料、人體生物資料庫等）
(2) 醫學影像分析、電腦視覺處理、生醫訊號處理
(3) 統計方法、理論與軟體研發、資訊系統及產品開發

參考網站：
(1) https://sites.stat.sinica.edu.tw/SH/
(2) https://sites.stat.sinica.edu.tw/SARS-CoV-2/
(3) http://gap.stat.sinica.edu.tw/
(4) https://www.stat.sinica.edu.tw/hsinchou/

1. 資料分析與文獻收集
2. 程式撰寫及開發
3. 臨時交辦事項