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).