UTFacultiesEEMCSDisciplines & departmentsFormal Methods and ToolsGroup colloquiumIntelliJML - JML support in IntelliJ IDEA for the Software Systems module, GUI for parity game research, Interactive solver for polynomial inequations using interval arithmetics

IntelliJML - JML support in IntelliJ IDEA for the Software Systems module, GUI for parity game research, Interactive solver for polynomial inequations using interval arithmetics by various students

Abstract 
The Java Modeling Language (JML) is a specification language that is used to specify intended behavior of Java programs. Up to the academic year 2018-2019, JML was included in the curriculum of the Software Systems module as part of the Technical Computer Science bachelor. As a result of incompatible changes to software used within the module, a decision was reluctantly made to halt the teaching of JML. This project aims to allow JML to be reintroduced to Software Systems by creating an easy-to-use plugin for IntelliJ IDEA that provides support for modern Java versions. Features such as syntax, type, and semantic checking, as well as syntax highlighting and autocompletion are provided to aid students in writing JML specifications in a convenient manner.

Abstract 
Our project is aimed at building a GUI interface that helps with parity game research. In particular, the project intends to help parity game researchers to see the dynamics of their algorithms reflected on a graph, to adjust the configurations of the parity game, and to export parity games. The framework will also be extendable such that other types of graph research can also make use of it.

Abstract 
A big issue in mathematics is uncertainty, a quantitative estimation of errors. Interval arithmetic is one of the mathematical tools to eliminate uncertainty and to draw mathematically sound conclusions. The project focuses on the visual support of solving polynomial inequations using interval arithmetic.
In interval arithmetic, the variables of polynomial inequations are representative for intervals with well-defined boundaries. The parameter space is then divided into regions, which can be split into finer subregions. The inequation can be evaluated for the boundaries of the subregions to determine whether a given inequation holds true, false or undecided for specific boundaries.
The software we worked on is an interactive solver for polynomial ineqations using interval arithmetic. To increase the usability, the program also supports boolean operations with ternary logic. The software can be used to visualize specific refinement strategies or even develop new ones. Moreover, it helps to understand interval arithmetic.