会议名称(中文)： 6th International Conference on Interactive Theorem Proving (ITP 2015)
会议名称(英文)： 6th International Conference on Interactive Theorem Proving (ITP 2015)
所属学科： 计算机科学理论,计算机系统结构与硬件
开始日期： 2015-08-24
结束日期： 2015-08-27
所在国家： 中华人民共和国
所在城市： 江苏省 南京市
主办单位： 中国科技大学、King's College London、Microsoft Research Cambridge, United Kingdom
[ 重要日期 ]
全文截稿日期： 2015-03-13
[ 会务组联系方式 ]
联系人： Christian Urban
会议背景介绍：
The 6th conference on Interactive Theorem Proving will be held in Nanjing, China. Nanjing is situated in the heart of China — close to Shanghai and roughly equidistant between Beijing and Hong Kong. It is a former capital during the Ming Dynasty with a rich cultural heritage. We expect to have more information about travelling and a detailed programme nearer the time. The proceedings will be published as usual in the LNCS Series.
征文范围及要求：
The programme committee welcomes submissions on all aspects of interactive theorem proving and its applications. The topics include, but are not limited to, the following:
Specification and verification of hardware: microprocessors, memory systems, pipelines, etc; formal semantics of hardware design languages; synthesis; formal design flows.
Specification and verification of software: program verification, refine- ment, and synthesis for functional, declarative and imperative languages; formal semantics of programming languages; proof carrying code.
Industrial application of theorem provers.
Formalization of mathematical theories.
Advances in theorem prover technology: proof automation and deci- sion procedures, induction, combination of deductive and algorithmic approaches, incorporation of theorem provers into larger systems, com- bination of theorem provers with other provers and tools.
Other topics, including formal verification of security policies and con- figurations (formal analysis, verification of security algorithms, etc); specification and requirements analysis of systems; user interfaces for theorem provers; development and extension of higher order logics.
Proof Pearls: concise and elegant presentations of interesting examples. |
