| Popis: |
Because of our increasing dependence on software in every aspect of our lives, it is crucial that our software systems are reliable, safe, and correct --- they must not crash, must be safe from attack, and must consistently compute the results we expect from them. As testing is insufficient to show the absence of errors and manual code review is tedious, costly, and error-prone, the only clear path to efficiently and reliably ensuring software quality is to develop automatic verification tools which require as little intervention from the programmer as possible. In this dissertation, we present Liquid Types, an automated approach to software verification based on inferring and checking expressive refinement types, data types which are augmented with logical predicates, which can be used to express and verify sophisticated program invariants. We show how Liquid Types divides the task of program verification between type-based and logic-based reasoning to infer precise invariants of unboundedly-large data structures. Further, we show how the Liquid Types technique is suited both to high-level, pure functional languages and low-level, imperative languages with mutable state, allowing for the verification of programmings running the full range from applications to systems programs. The Liquid Types technique has been implemented in type checkers for both the OCaml and C languages and applied to a number of challenging programs taken from the literature and from the wild. We highlight experimental results that show that the refinement type inference performed by Liquid Types can be used to verify crucial safety properties of real-world programs without imposing an undue verification-related overhead on the programmer |
