Mattias Ulbrich

icon indicating a website link http://formal.iti.kit.edu/~ulbrich/

icon company Karlsruhe Institute of Technology, Inst. of Theoretical Informatics icon location Karlsruhe, DE

Results 13 issues of Mattias Ulbrich

Solving the FP completeness issues in #1723

9 comment

## Related Issue This pull request answers to issue #1723. ## Intended Change Floats and doubles are currently incorrectly insufficiently handled when they appear in one expression. Casts need to...

Calculus
Completeness

KeY proofs cannot be replayed if certain labels are present

5 comment

## Description If certain labels are present on a term and a find-and-add taclet is applied, stored proofs cannot be replayed/loaded. The problem is that the recomputation of the labels...

Proof Loading/Saving

Improved treatment of final fields

2 comment

## Intended Change Final fields cannot change their value after a single assignment in the constructor. In the current KeY logic, final fields are treated like normal fields stored on...