Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


ucin1066407869.pdf (386.32 KB)

ETD Abstract Container

Abstract Header

AN APPROACH TO FACILITATING VERIFICATION OF LINEAR CONSTRAINTS

SABNIS, SUDEEP SUHAS
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1066407869

Abstract Details

2003, MS, University of Cincinnati, Engineering : Computer Science.
The notion of dependent types has been around for more than three decades, but a major complication resulting from introducing such a type discipline is that pure type inference for the enriched system is no longer possible. However, in the late nineties, a restricted form of dependent types was introduced in practical programming to capture more program properties through types and thereby detect more program errors at compile-time than effected by the strong type discipline in Standard ML or Java. Xanadu, a dependently typed imperative programming language, was the result of enriching the type system of imperative programming paradigm with a restricted form of dependent types. For the effective compilation of Xanadu program, it is crucial to successfully solve the linear constraints generated during its type-checking. This study is focussed on solving and verifying the linear integer constraints generated during the type-checking of Xanadu program. We present a two-tier constraint solver, based on the well-known linear programming algorithm, the Simplex method. The first tier uses the two-phase Simplex method to find a rational solution for a given set of constraints. If no rational solution exists, then no integer solution could be found. However, if a rational solution exists, the second tier uses branch and bound method, an integer programming algorithm, to seek an integer solution. As a significant application, we also study the use of our solver in eliminating the need for array bounds checking at runtime. The solver also generates a data structure, which we designate as history matrix, that records the operations of the Simplex algorithm. We claim that verifying the constraints using this data structure is faster than verifying them through the solver. Several constraints, gathered from the type-checking of Xanadu programs are solved and verified using the history matrix. The results presented, validate our claim. Moreover, we regard this matrix as a representation of a proof, which along with the compiled code would form an effort aimed towards producing a certifying code or a proof carrying code for Xanadu.
Dr. Karen Tomko (Advisor)
96 p.
Computer Science
simplex algorithm; verification; linear constraints; Xanadu; dependent types

Recommended Citations

Citations

  • SABNIS, S. S. (2003). AN APPROACH TO FACILITATING VERIFICATION OF LINEAR CONSTRAINTS [Master's thesis, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1066407869

    APA Style (7th edition)

  • SABNIS, SUDEEP. AN APPROACH TO FACILITATING VERIFICATION OF LINEAR CONSTRAINTS. 2003. University of Cincinnati, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1066407869.

    MLA Style (8th edition)

  • SABNIS, SUDEEP. "AN APPROACH TO FACILITATING VERIFICATION OF LINEAR CONSTRAINTS." Master's thesis, University of Cincinnati, 2003. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1066407869

    Chicago Manual of Style (17th edition)

ucin1066407869
702
© 2003, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.