Machine-assisted theorem proving: Proof techniques and applications

点击翻译按钮获取中文摘要

The principle objective of the proposed research is to advance techniques in formal proof of properties of programs, programming languages, and policies. For individual programs, proving that they meet certain properties contributes to a very high level of assurance that they will behave as expected. For properties of programming languages, it is well-known that those that are formally proven to be sound can better provide a solid basis for building software systems that are reliable and secure. Examples where policies play an increasingly important role include assuring that software that processes health or other personal data respects privacy requirements, and assuring that software that is used in the administration of businesses respects government financial and security regulations.