BEGIN:VCALENDAR PRODID:-//eluceo/ical//2.0/EN VERSION:2.0 CALSCALE:GREGORIAN BEGIN:VEVENT UID:8064249678d923da622ff4137f181ef3 DTSTAMP:20260609T085708Z SUMMARY:Andy Oertel's Licentiate Seminar DESCRIPTION:Kontakt: andy.oertel@cs.lth.se\n\nThesis title: \;Certifyin g Combinatorial Optimization Using Pseudo-Boolean ReasoningAuthor: \;A ndy Oertel\, Department of Computer Science\, Lund UniversityFaculty oppon ent: Associate Professor Marco Chiarandini\, University of Southern Denmar kExaminer: \;Professor Jacek Malec\, LTHSupervisor: Professor Jakob No rdström\, LTHCo-supervisor: \;Assistant Professor Susanna de Rezende\ , LTHDate and time: Friday 28 November at 13:30Location: \;E:1406\, E- huset\, LTH\, Klas Anshelms väg 10/Ole Römers väg 3\, LundA link to dow nload the thesis will be added later \;AbstractCombinatorial optimizat ion provides a powerful framework for solving complex optimization problem s with general-purpose solvers by modelling the problem in an abstract lan guage. Due to breakthroughs in algorithms to solve combinatorial optimizat ion problems in last decades\, combinatorial optimization has become a val id approach to solve many real world problems efficiently. Key application areas are planning\, scheduling\, computer-aided design\, verification\, and even theorem proving. However\, the efficiency of the tools to solve t hese problems comes at the cost of increased complexity of the solvers. Th is makes it difficult to trust that the result computed by a combinatorial optimization solver is correct\, which especially becomes a concern if th e correctness of the result is mission-critical.The main approach to addre ss this issue is certifying algorithms\, where an algorithm has to also ge nerate a certificate that its result is correct\, which can then be checke d independently. This thesis demonstrates how pseudo-Boolean reasoning can be used to provide efficient certification of results returned by differe nt kinds of combinatorial optimization solvers. We present a unified multi purpose certification system with a formally verified end-to-end verificat ion toolchain\, which guarantees that the combinatorial optimization probl em was solved correctly. Developing a multipurpose certification system di stinguishes this work from any prior work\, which predominantly focused on very specialized approaches. We also present certification for many algor ithms which\, prior to our work\, lacked any approach for certifying their result. \;\n\nMer information om händelsen: https://www.cs.lth.se/ev enemang/andy-oertels-licentiate-seminar DTSTART;TZID=GMT:20251128T123000 DTEND;TZID=GMT:20251128T123000 LOCATION:E:1406\, E-huset\, LTH\, Ole Römers väg 3\, Lund END:VEVENT END:VCALENDAR