Rigorous Modularity: formalizing and verifying software constructions

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

Software development is undergoing another paradigm shift: certified programming. Previously, small changes to significant code bases would require time-consuming and unreliable testing before deployment. For example, altering the space shuttle software to enable missions to fly over New Year's day was estimated at millions of dollars, and hence not implemented. But, similar systems are being deployed to control airliners, automobiles, and life-support systems.