The SMT-LIB language and the B language are both based on predicate logic and share the definition of several operators. However, B supports data types not available in SMT-LIB and vice versa. In this article we suggest a straightforward translation …
Software is notoriously hard to test. Some of the difficulties stem from the test data available for data-intensive applications such as data warehouses. Existing test data might not be diverse enough to enable desired test cases, while at the same …
Employing formal methods for software development usually involves using a multitude of tools such as model checkers and provers. Most of them again feature different backends and configuration options. Selecting an appropriate configuration for a …
Testing is an important aspect in professional software development, both to avoid and identify bugs as well as to increase maintainability. However, increasing the number of tests beyond a reasonable amount hinders development progress. To decide on …
Non-deterministic specifications play a central role in the use of formal methods for software development. Such specifications can be more readable, but hard to execute efficiently due to the usually large search space. Constraint programming offers …
In this paper, we introduce a translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar, each construct is translated into a semantically equivalent component of the B language. In addition to …
Constraint solving technology for declarative formal models has made considerable progress in recent years, and has many applications such as animation of high-level specifications, test case generation, or symbolic model checking. In this article we …
The idea of verifying the correctness of software has been brought up in the early days of computing, for example by Alan Turing in 1949 or Robert W. Floyd in 1967. James C. King extended upon the idea of manual verification by suggesting and working …