You are here: Home › … › Student Projects and … › In progress › [B.Sc. Thesis] Simplificaton of …

[B.Sc. Thesis] Simplificaton of Formulas

Course type Bachelor Thesis
Instructors Matthias Heizmann1
Credits 12
Course Catalog
Extend the simplification algorithm presented by Işıl Dillig2,Thomas Dillig3 and Alex Aiken4 in the paper Small Formulas for Large Programs: On-line Constraint Simplification in Scalable Static Analysis 5to all kinds of Boolean terms allowed in the SMT-lib6 format. Implement your algorithm in our SMT solver SmtInterpol7 and prove the correctness of our algorithm.

 

 

Links

  1. https://swt.informatik.uni-freiburg.de/staff/heizmann
  2. http://www.cs.wm.edu/%7Eidillig/
  3. http://www.cs.wm.edu/%7Etdillig/
  4. http://theory.stanford.edu/%7Eaiken/
  5. http://www.cs.wm.edu/%7Etdillig/sas2010.pdf
  6. http://www.smtlib.org/
  7. https://swt.informatik.uni-freiburg.de/tool/smtinterpol