Khurshid, Sarfraz2010-09-212010-09-212017-05-112010-09-212010-09-212017-05-112009-12December 2http://hdl.handle.net/2152/ETD-UT-2009-12-700textAdvances in constraint solving and increases in processing power have enabled new approaches for automating specification-based testing. However, writing specifications and scaling techniques that utilize them remain challenging. We introduce Milao -- a novel framework for mixed imperative and declarative formulation and solving of structural constraints -- which addresses both these challenges. One, Milao introduces a mixed style for writing specifications using a combination of declarative and imperative styles, which provides flexibility in specification formulation and reduces its burden on the user. Two, it introduces a mixed technique for solving constraints using a combination of solvers in synergy. As enabling technologies, the Alloy tool-set and the Java PathFinder model checker are used. Initial experiments witness the benefits of our framework.application/pdfengSpecification-based testingConstraint solvingthesis2010-09-21