Skip to main content
SpringerLink
Log in

JConstraints: A Library for Working with Logic Expressions in Java

  • Chapter
  • First Online:
Models, Mindsets, Meta: The What, the How, and the Why Not?

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11200))

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 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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/psycopaths/jconstraints.

  2. 2.

    https://github.com/sosy-lab/java-smt.

  3. 3.

    https://github.com/ArduPilot/ardupilot.

References

  1. Aharoni, M., Asaf, S., Fournier, L., Koifman, A., Nagel, R.: FPgen-a test generation framework for datapath floating-point verification. In: Eighth IEEE International High-Level Design Validation and Test Workshop, 2003, pp. 17–22. IEEE (2003)

    Google Scholar 

  2. Bagnara, R., Carlier, M., Gori, R., Gotlieb, A.: Symbolic path-oriented test data generation for floating-point programs. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation (ICST), pp. 1–10. IEEE (2013)

    Google Scholar 

  3. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org

  4. Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885 (2009)

    Google Scholar 

  5. Botella, B., Gotlieb, A., Michel, C.: Symbolic execution of floating-point computations. Softw. Test. Verif. Reliab. 16(2), 97–121 (2006)

    Article  Google Scholar 

  6. Cadar, C., Dunbar, D., Engler, D.R., et al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol. 8, pp. 209–224 (2008)

    Google Scholar 

  7. Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Learning extended finite state machines. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 250–264. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_18

    Chapter  Google Scholar 

  8. Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31759-0_19

    Chapter  Google Scholar 

  9. Cousot, P., et al.: Combination of abstractions in the ASTRÉE static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77505-8_23

    Chapter  Google Scholar 

  10. Damiani, F., Hähnle, R., Lienhardt, M.: Abstraction refinement for the analysis of software product lines. In: Gabmeyer, S., Johnsen, E.B. (eds.) TAP 2017. LNCS, vol. 10375, pp. 3–20. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61467-0_1

    Chapter  Google Scholar 

  11. Darulova, E., Kuncak, V.: Sound compilation of reals. In: ACM SIGPLAN Notices, vol. 49, pp. 235–248. ACM (2014)

    Google Scholar 

  12. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  13. Dinges, P., Agha, G.: Solving complex path conditions through heuristic search on induced polytopes. In: Proceedings of the 22nd ACM SIGSOFT Symposium on Foundations of Software Engineering, Hong Kong, 16–21 November 2014. ACM (2014)

    Google Scholar 

  14. Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_14

    Chapter  Google Scholar 

  15. Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop 2015 (2015)

    Google Scholar 

  16. Giannakopoulou, D., Rakamarić, Z., Raman, V.: Symbolic learning of component interfaces. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 248–264. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_18

    Chapter  Google Scholar 

  17. Goubault, E., Putot, S.: Static analysis of numerical algorithms. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 18–34. Springer, Heidelberg (2006). https://doi.org/10.1007/11823230_3

    Chapter  MATH  Google Scholar 

  18. Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232–247. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_17

    Chapter  Google Scholar 

  19. Howar, F., Steffen, B., Jonsson, B., Cassel, S.: Inferring canonical register automata. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 251–266. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_17

    Chapter  Google Scholar 

  20. Ireland, C., Bowers, D., Newton, M., Waugh, K.: A classification of object-relational impedance mismatch. In: First International Conference on Advances in Databases, Knowledge, and Data Applications, DBKDA 2009, pp. 36–43. IEEE (2009)

    Google Scholar 

  21. Isberner, M., Howar, F., Steffen, B.: The open-source LearnLib. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 487–495. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_32

    Chapter  Google Scholar 

  22. Liew, D., Schemmel, D., Cadar, C., Donaldson, A.F., Zahl, R., Wehrle, K.: Floating-point symbolic execution: a case study in N-version programming. In: 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 601–612. IEEE (2017)

    Google Scholar 

  23. Luckow, K., et al.: JDart: a dynamic symbolic analysis framework. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 442–459. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_26

    Chapter  Google Scholar 

  24. Margaria, T., Nagel, R., Steffen, B.: Remote integration and coordination of verification tools in JETI. In: 12th IEEE International Conference on the Engineering of Computer-Based Systems (ECBS 2005), Greenbelt, MD, USA, 4–7 April 2005, pp. 431–436 (2005)

    Google Scholar 

  25. Martel, M.: Propagation of roundoff errors in finite precision computations: a semantics approach. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 194–208. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45927-8_14

    Chapter  Google Scholar 

  26. Pasareanu, C., d’Amorim, M., Borges, M., Souza, M.: Coral: solving complex constraints for symbolic pathfinder (2010)

    Google Scholar 

  27. Putot, S., Goubault, E., Martel, M.: Static analysis-based validation of floating-point computations. In: Alt, R., Frommer, A., Kearfott, R.B., Luther, W. (eds.) Numerical Software with Result Verification. LNCS, vol. 2991, pp. 306–313. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24738-8_18

    Chapter  Google Scholar 

  28. Richly, K., Lorenz, M., Oergel, S.: S4J - integrating SQL into Java at compiler-level. In: Dregvaite, G., Damasevicius, R. (eds.) ICIST 2016. CCIS, vol. 639, pp. 300–315. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46254-7_24

    Chapter  Google Scholar 

  29. Schumann, J., Schneider, S.-A.: Automated testcase generation for numerical support functions in embedded systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 252–257. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_20

    Chapter  Google Scholar 

  30. Sherman, E., Dwyer, M.B.: Exploiting domain and program structure to synthesize efficient and precise data flow analyses (t). In: 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 608–618. IEEE (2015)

    Google Scholar 

  31. Souza, M., Borges, M., d’Amorim, M., Păsăreanu, C.S.: CORAL: solving complex constraints for symbolic pathfinder. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 359–374. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_26

    Chapter  Google Scholar 

  32. Steffen, B., Gossen, F., Naujokat, S., Margaria, T.: Language-driven engineering: from general purpose to purpose-specific languages. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 311–344 (2019)

    Google Scholar 

  33. Steffen, B., Margaria, T., Braun, V.: The electronic tool integration platform: concepts and design. STTT 1(1–2), 9–30 (1997)

    Article  Google Scholar 

  34. Visser, W., Geldenhuys, J., Dwyer, M.B.: Green: reducing, reusing and recycling constraints in program analysis. In: 20th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-20), SIGSOFT/FSE 2012, Cary, NC, USA, 11–16 November 2012, p. 58 (2012)

    Google Scholar 

Download references

Acknowledgments

JConstraints has been developed as part of JDart and several people who worked on JDart have contributed ideas and code to JConstraints. Notable contributions to JConstraints have been made by Marko Dimjašević, Malte Isberner, and Kasper Luckow.

Author information

Authors and Affiliations

  1. Dortmund University of Technology and Fraunhofer ISST, Dortmund, Germany

    Falk Howar

  2. Dortmund University of Technology, Dortmund, Germany

    Fadi Jabbour & Malte Mues

Authors
  1. Falk Howar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fadi Jabbour
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Malte Mues
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Malte Mues .

Editor information

Editors and Affiliations

  1. Lero–The Irish Software Research Center, University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. Verimag Laboratory, Grenoble, France

    Susanne Graf

  3. Aalborg University, Aalborg, Denmark

    Kim G. Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Howar, F., Jabbour, F., Mues, M. (2019). JConstraints: A Library for Working with Logic Expressions in Java. In: Margaria, T., Graf, S., Larsen, K. (eds) Models, Mindsets, Meta: The What, the How, and the Why Not?. Lecture Notes in Computer Science(), vol 11200. Springer, Cham. https://doi.org/10.1007/978-3-030-22348-9_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-22348-9_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-22347-2

  • Online ISBN: 978-3-030-22348-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation