A system for SMT based constraint programming in Java
dc.contributor.author | Funk, Maurice | |
dc.contributor.editor | Eibl, Maximilian | |
dc.contributor.editor | Gaedke, Martin | |
dc.date.accessioned | 2017-08-28T23:48:14Z | |
dc.date.available | 2017-08-28T23:48:14Z | |
dc.date.issued | 2017 | |
dc.description.abstract | This paper presents a system for constraint programming in Java using translation of JVM bytecode into SMT. This allows the constraints to be written in normal Java, to being interoperable with the rest of the program and lowers the entry barrier to using specialised solvers in applications. Due to the nature of the performed translation, variable assignments for other runtime properties than constraint satisfaction can be found. These include variable assignments that lead to runtime exceptions during normal code execution. We demonstrate that the implemented approach is able to find variable assignments for non-trivial constraints such as a Sudoku puzzle. | en |
dc.identifier.doi | 10.18420/in2017_260 | |
dc.identifier.isbn | 978-3-88579-669-5 | |
dc.identifier.pissn | 1617-5468 | |
dc.language.iso | en | |
dc.publisher | Gesellschaft für Informatik, Bonn | |
dc.relation.ispartof | INFORMATIK 2017 | |
dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Proceedings, Volume P-275 | |
dc.subject | Constraint Programming | |
dc.subject | SMT | |
dc.subject | Java | |
dc.subject | Program Analysis | |
dc.subject | Symbolic Execution | |
dc.title | A system for SMT based constraint programming in Java | en |
gi.citation.endPage | 2580 | |
gi.citation.startPage | 2575 | |
gi.conference.date | 25.-29. September 2017 | |
gi.conference.location | Chemnitz | |
gi.conference.sessiontitle | Studierendenkonferenz Informatik 2017 (SKILL 2017) |
Dateien
Originalbündel
1 - 1 von 1