Constraint Solving via Combined Widening and Narrowing in Coq

Name
Kadi Sammul
Abstract
In program analysis constraint solving via sets of values is time-consuming and needs a lot of memory. Therefore, it is wiser to use widening. Widening makes analysis inaccurate - to restore accuracy narrowing can be used. Using combined widening and narrowing we create an algorithm in Coq, where in addition to finding a solution we guarantee the termination of the analysis.
Graduation Thesis language
Estonian
Graduation Thesis type
Master - Computer Science
Supervisor(s)
Kalmer Apinis
Defence year
2024
 
PDF Extras