Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. JConstraints: A Library for Working with Logic Expressions in Java
 MargariaSteffen, T.: Models, mindsets, meta. The what, the how, and the why not? : Essays dedicated to Bernhard Steffen on the occasion of his 60th birthday Cham: Springer Nature, 2019 (Lecture Notes in Computer Science 11200) ISBN: 9783030223472 (Print) ISBN: 9783030223489 (Online) ISBN: 3030223477 S.310325 
 International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) <8, 2018, Limassol> 

 Englisch 
 Konferenzbeitrag 
 Fraunhofer ISST () 
Abstract
In this paper we present JConstraints, a constraint solver abstraction layer for Java. JConstraints provides an object representation for logic expressions, unified access to different SMT and interpolation solvers, and useful tools and algorithms for working with logic formulas. The object representation enables implementation of algorithms on constraints by users. For deciding satisfiability of formulas, JConstraints translates from its internal object representation to the format expected by constraint solvers or a format suitable for different analysis goals. We demonstrate the capabilities of JConstraints by implementing a custom meta decision procedure for floatingpoint arithmetic that combines an approximating analysis over the reals with a proper floatingpoint analysis. The performance of the combined analysis is encouraging on a set of benchmarks: overall, a total reduction of time spent for constraint solving by 56% is achieved.