Abstraction and Automation for Reasoning about Complex Software

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

Modern software development is a complex and messy business. Requirements are likely incomplete. New development uses complex existing libraries, tools and components that can fail. Multiple development teams proceed on different schedules, making it difficult to assure that their artifacts will “talk to each other” as intended. Every time a change is made, expensive quality assurance needs to be performed to ensure that software still does what it was supposed to. Such problems are made even more dire because many companies, especially in automotive, electronics, aerospace and defense domains, need to maintain families of software product variants with similar yet not identical functionality (e.g., supporting different types of customers and/or software platforms).