各位電機系的師長，同學，與同仁們，大家好！我是李念澤，很榮幸自2025年2月起回到母校任教。

我的研究專長是形式方法 (Formal Methods)，主要應用於計算系統的驗證，包括軟體工程中的程式驗證與電子設計自動化 (EDA) 中的電路驗證。在軟體與硬體開發過程中，為了確保系統的正確性與可靠性，我們經常透過測試來檢查其行為是否符合預期。例如輸入不同的測試數據，觀察結果是否正確。 然而，測試只能涵蓋有限的情境，仍可能遺漏潛在錯誤。相比之下，形式方法是一種更為嚴謹的驗證技術。 它透過數學邏輯與演算法來完整分析系統的行為，甚至可以自動證明某些錯誤永遠不會發生。雖然形式方法的計算複雜度極高（某些問題甚至是不可判定 (undecidable)），但科學家們已發展出許多實用的方法與工具，使其能夠應用於現實世界的工程挑戰。 這項技術對於高安全性應用 (Safety-Critical Applications) 尤為關鍵，例如飛航控制系統，金融交易系統，醫療設備等。 我目前的研究專注於開發高效的形式驗證技術，並將其應用於複雜計算系統的工程，確保這些關鍵系統的安全與可靠性。

我於2009年進入臺大電機系就讀，畢業後服完兵役，繼續在電子所江介宏教授的指導下攻讀博士，並於2021年取得博士學位。在博士班期間，我曾前往美國 IBM Thomas J. Watson 研究中心實習，並參與電資學院與日本國立情報學研究所 (NII) 的國際實習計畫。此外，我也獲得國科會與德國學術交流總署 (DAAD) 的獎學金，前往德國慕尼黑大學 (LMU Munich) 進行研究訪問。這些經驗不僅拓展了我的視野，也讓我深刻體會到跨文化學術合作的價值。

博士畢業後，我前往德國慕尼黑大學擔任博士後研究員，加入Dirk Beyer 教授的研究團隊。在德國的三年間，我除了持續研究軟體驗證，也開始將 EDA 的技術應用於程式分析。基於這個發想，我撰寫了一份研究計畫，並有幸獲得德國研究基金會 (German Research Foundation, DFG) 的研究獎助。我與 Dirk Beyer 教授的團隊在軟硬體驗證的交叉應用上取得了重要成果，進而引起Intel 的關注，主動邀請我們合作開發自動化的韌體分析方法。這段博士後的經驗讓我培養了跨領域與跨國團隊合作的能力，也讓我更注重學術研究的實用價值。

回到臺大電機系任教，我希望能夠激發同學對形式方法的興趣，並持續推動形式驗證技術的發展，讓我們日常倚賴的計算系統更加安全可靠。此外，我期許自己能鼓勵系上同學積極爭取出國交換及研究訪問的機會，探索不同的文化與價值觀，尋找適合自己的職涯成長之路。