A Constraint Solver: Finding Models and Cores of Large Relational Specifications

Опубликовано 6 сентября 2016, 17:12

Relational logic is an attractive candidate for a software description language, because both the design and implementation of software often involve reasoning about relational structures, whether in the problem domain (organizational structure, for example), in the high level design (architectural configurations, for example) or in low level code (graphs and linked lists). Until recently, however, frameworks for solving relational constraints (such as Alloy3) have had limited applicability. While powerful enough to analyze relatively small, hand-crafted models of software systems, current frameworks perform poorly on large and automatically generated specifications. In this talk, I will describe Kodkod, an efficient constraint solver for relational logic, with recent applications to design analysis, code checking, test-case generation, and declarative configuration. The Kodkod system includes a finite model finder and a minimal unsatisfiable core extractor, both based on SAT solving technology. I will present the key ideas and contributions behind these analyses, discuss how they compare to existing approaches, and conclude with an overview of future work.