[2017-04-19] 黃敬群先生,NCKU," Formal Verification in practice: system software perspective "
Title: Formal Verification in practice: system software perspective
Date: 2017-04-19 9:00 am-11: 00 am
Location: R101, CSIE
Speaker: 黃敬群 (Jim Huang),NCKU
Hosted by: Prof. Shih-Wei Liao
Recent system software development is executed with various verification techniques. seL4 is one of the typical models, where large-scale formal software verification projects runs successfully. In this talk, we would report on the development process about formulating a detailed descriptive model of its middle-out development process, and analyze the evolution and dependencies of code and proofs. Formal verifications in industry are becoming common. Microsoft uses formal tools such as Boogie and SLAM to verify programs and drivers, so does Airbus and Toyota.
黃敬群 (Jim Huang)，網路慣用暱稱為 "jserv"。參與過若干世界級的開放原始碼專案，如 Android Open Source Project, GCC, LXDE。過去耕耘於消費性電子產品、IC 設計與工業自動化等領域，近來和一群「火箭大叔」合作，在原 ARRC (前瞻火箭研究中心) 的基礎下，強化火箭控制系統的軟體架構。