Linking the Meaning of Programs to What the Compiler Can Verify

We formulate some research and development challenges that relate what a verifying compiler can verify to the definition and analysis of the application-content of programs, where the analysis comprises both experimental validation and mathematical verification. We also point to a practical framework to deal with theses challenges, namely the Abstract State Machines (ASM) method for high-level system design and analysis. We explain how it allows one to bridge the gap between informal requirements and detailed code by combining application-centric experimentally validatable system modeling with mathematically verifi

• Type: Conference
• Year: 2005
• Where: VSTTE
• Authors: Egon Börger
• Keywords: Software Engineering, VSTTE 2005