Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

JConstraints: A Library for Working with Logic Expressions in Java

: Howar, Falk; Jabbour, Fadi; Mues, Malte


Margaria-Steffen, 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: 978-3-030-22347-2 (Print)
ISBN: 978-3-030-22348-9 (Online)
ISBN: 3-030-22347-7
International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA) <8, 2018, Limassol>
Fraunhofer ISST ()

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 floating-point arithmetic that combines an approximating analysis over the reals with a proper floating-point 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.