當前位置:首頁  科學研究  科研動态

【安全關鍵軟件系列講座3】Introduction to the proof assistant Coq

時間:2016-04-13作者:來源:伟德victory點擊:242

報告題目:Introduction to the proof assistant Coq

報 告 人:Prof. Jean-Paul Bodeveix , Mr. Mamoun Filali

報告地點: 伟德victory實驗樓102多媒體教室

報告時間:2016年4月26上午9:00-12:00

報告簡介:
In this talk, we introduce the basic concepts of the proof assistant Coq. After a brief overview of the main features assistant theorem provers, we present the basic objects of Coq. We distinguish two family of objects: propositions and data types. We insist of the rich typing theory of Coq: inductive types, dependent types. We illustrate them on the definition of logical connectors and basic data types.

報告人簡介:

Dr. Prof. Jean-Paul Bodeveix received a PhD of Computer Science from the University of Paris-Sud 11 in 1989. He has been assistant professor at University of Toulouse III since 1989 and is now Professor of computer science since 2003. His main research interests concern formal specifications, automated and assisted verification of protocols as well as of proof environments. He has participated in European and national projects related to these domains. His current activities are linked to real time modeling and verification via model checking techniques, assisted development of correct by construction models using refined-based development methods and meta-level reasoning using set theory-based tools or type theory-based tools (Coq).

Dr. Mamoun Filali is a full time researcher at CNRS (Centre National de la Recherche Scientifique). His main research interests concern the certified development of distributed and embedded systems. He is concerned by development methods through formally verified refinements (B, Event B). He has also studies real-time model checking and theorem proving. During the last years, he has been mainly involved in the French nationwide TOPCASED project where he was concerned by the verification topic. He has also participated to the proposal of the AADL behavioral annex which has been adopted as part of the AADL SAE standard.

伟德victory(&國際合作交流處)

地址:江蘇省南京市江甯區将軍大道29号

郵政編碼: 211106

版權所有:伟德victory - 伟德网站是多少 後台管理 書記信箱 院長信箱

友情鍊接

校外導航鍊接

Baidu
sogou