Showing 1–20 of 20 results for author: Vazou, N

Mechanizing Refinement Types (extended)

Authors: Michael Borkowski, Niki Vazou, Ranjit Jhala

Abstract: Practical checkers based on refinement types use the combination of implicit semantic sub-ty** and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal meta-theoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ_RF a core refinement calculus… ▽ More Practical checkers based on refinement types use the combination of implicit semantic sub-ty** and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal meta-theoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ_RF a core refinement calculus that combines semantic sub-ty** and parametric polymorphism. We develop a meta-theory for this calculus and prove soundness of the type system. Finally, we give a full mechanization of our meta-theory using the refinement-type based LiquidHaskell as a proof checker, showing how refinements can be used for mechanization. △ Less

Submitted 12 July, 2022; originally announced July 2022.

Comments: 32 pages, under review

ACM Class: F.3.1; D.3.1

Flux: Liquid Types for Rust

Authors: Nico Lehmann, Adam Geller, Niki Vazou, Ranjit Jhala

Abstract: We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust that indexes mutable locations, with pure (immutable) values that can appear in refinements, and then exploits Rust's ownership mechanisms to abstra… ▽ More We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust that indexes mutable locations, with pure (immutable) values that can appear in refinements, and then exploits Rust's ownership mechanisms to abstract sub-structural reasoning about locations within Rust's polymorphic type constructors, while supporting strong updates. We formalize the crucial dependency upon Rust's strong aliasing guarantees by exploiting the stacked borrows aliasing model to prove that ``well-borrowed evaluations of well-typed programs do not get stuck''. Second, we implement our type system in Flux, a plug-in to the Rust compiler that exploits the factoring of complex invariants into types and refinements to efficiently synthesize loop annotations -- including complex quantified invariants describing the contents of containers -- via liquid inference. Third, we evaluate Flux with a benchmark suite of vector manipulating programs and parts of a previously verified secure sandboxing library to demonstrate the advantages of refinement types over program logics as implemented in the state-of-the-art Prusti verifier. While Prusti's more expressive program logic can, in general, verify deep functional correctness specifications, for the lightweight but ubiquitous and important verification use-cases covered by our benchmarks, liquid ty** makes verification ergonomic by slashing specification lines by a factor of two, verification time by an order of magnitude, and annotation overhead from up to 24% of code size (average 9%) to nothing at all. △ Less

Submitted 14 November, 2022; v1 submitted 8 July, 2022; originally announced July 2022.

ACM Class: F.3.1; D.2.4

Verified Causal Broadcast with Liquid Haskell

Authors: Patrick Redmond, Gan Shen, Niki Vazou, Lindsey Kuper

Abstract: Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. A causal delivery protocol ensures that w… ▽ More Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causally ordered message delivery to ensure causal consistency, and CRDTs can rely on the existence of an underlying causally-ordered messaging layer to simplify their implementation. A causal delivery protocol ensures that when a message is delivered to a process, any causally preceding messages sent to the same process have already been delivered to it. While causal delivery protocols are widely used, verification of their correctness is less common, much less machine-checked proofs about executable implementations. We implemented a standard causal broadcast protocol in Haskell and used the Liquid Haskell solver-aided verification system to express and mechanically prove that messages will never be delivered to a process in an order that violates causality. We express this property using refinement types and prove that it holds of our implementation, taking advantage of Liquid Haskell's underlying SMT solver to automate parts of the proof and using its manual theorem-proving features for the rest. We then put our verified causal broadcast implementation to work as the foundation of a distributed key-value store. △ Less

Submitted 15 March, 2023; v1 submitted 29 June, 2022; originally announced June 2022.

Comments: Appeared at IFL 2022

ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

Authors: Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker

Abstract: Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but breaks non-interference. We present ANOSY, an approximate knowledge synthesizer for quantitative declassification policies. ANOSY uses refinement types to automatically construct machine checked over- and under-approximatio… ▽ More Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but breaks non-interference. We present ANOSY, an approximate knowledge synthesizer for quantitative declassification policies. ANOSY uses refinement types to automatically construct machine checked over- and under-approximations of attacker knowledge for boolean queries on multi-integer secrets. It also provides an AnosyT monad to track the attacker knowledge over multiple declassification queries and checks for violations against user-specified policies in information flow control applications. We implement a prototype of ANOSY and show that it is precise and permissive: up to 14 declassification queries are permitted before a policy violation occurs using the powerset of intervals domain. △ Less

Submitted 22 March, 2022; originally announced March 2022.

Comments: 16 pages, 6 figures, this is a preprint of a paper to appear in Programming Language Design and Implementation (PLDI) 2022

REST: Integrating Term Rewriting with Program Verification (Extended Version)

Authors: Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers

Abstract: We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively select… ▽ More We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell's evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs. △ Less

Submitted 16 February, 2022; v1 submitted 11 February, 2022; originally announced February 2022.

How to Safely Use Extensionality in Liquid Haskell

Authors: Niki Vazou, Michael Greenberg

Abstract: Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation, porting the proofs to an optimized implementation that behaves the same. Without functional extensionality, proofs must relate functions that are fully applied. When data itself has a higher-order representation, fully applied proofs face s… ▽ More Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation, porting the proofs to an optimized implementation that behaves the same. Without functional extensionality, proofs must relate functions that are fully applied. When data itself has a higher-order representation, fully applied proofs face serious impediments! When working with first-order data, fully applied proofs lead to noisome duplication when using higher-order functions. While dependent type theories are typically consistent with functional extensionality axioms, refinement type systems with semantic subty** treat naive phrasings of functional extensionality inconsistently, leading to unsoundness. We demonstrate this unsoundness and develop a new approach to equality in Liquid Haskell: we define a propositional equality in a library we call PEq. Using PEq avoids the unsoundness while still proving useful equalities at higher types; we demonstrate its use in several case studies. We validate PEq by building a small model and develo** its metatheory. Additionally, we prove metaproperties of PEq inside Liquid Haskell itself using an unnamed folklore technique, which we dub `classy induction'. △ Less

Submitted 19 July, 2022; v1 submitted 2 March, 2021; originally announced March 2021.

Comments: This is the extended version of the Haskell Symposium 2022 paper with the same title

Refinement Types: A Tutorial

Authors: Ranjit Jhala, Niki Vazou

Abstract: Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code. In this article, we distill the ideas developed in the substantial literature on refinement type… ▽ More Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what invariants and correctness properties should be checked on their code. In this article, we distill the ideas developed in the substantial literature on refinement types into a unified tutorial that explains the key ingredients of modern refinement type systems. In particular, we show how to implement a refinement type checker via a progression of languages that incrementally add features to the language or type system. △ Less

Submitted 15 October, 2020; originally announced October 2020.

LIO*: Low Level Information Flow Control in F*

Authors: Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin, Niki Vazou

Abstract: We present Labeled Input Output in F* (LIO*), a verified framework that enforces information flow control (IFC) policies developed in F* and automatically extracted to C. Inspired by LIO, we encapsulated IFC policies into effects, but using F* we derived efficient, low level, and provably correct code. Concretely, runtime checks are lifted to static proof obligations, the developed code is automat… ▽ More We present Labeled Input Output in F* (LIO*), a verified framework that enforces information flow control (IFC) policies developed in F* and automatically extracted to C. Inspired by LIO, we encapsulated IFC policies into effects, but using F* we derived efficient, low level, and provably correct code. Concretely, runtime checks are lifted to static proof obligations, the developed code is automatically extracted to C and proved non-interferent using metaprogramming. We benchmarked our framework on three clients and observed up to 54% speedup when IFC runtime checks are proved statically. Our framework is designed to aid development of embedded devices where both enforcement of security policies and low level efficient code is critical. △ Less

Submitted 27 April, 2020; originally announced April 2020.

Comments: Submitted to ICFP

Type-Level Computations for Ruby Libraries

Authors: Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn

Abstract: Many researchers have explored ways to bring static ty** to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often arises when using certain Ruby libraries. For example, the type safety of a database query in Ruby on Rails depends on the table and column names used in the query. To address this issue, we introduce CompRDL, a type system… ▽ More Many researchers have explored ways to bring static ty** to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often arises when using certain Ruby libraries. For example, the type safety of a database query in Ruby on Rails depends on the table and column names used in the query. To address this issue, we introduce CompRDL, a type system for Ruby that allows library method type signatures to include type-level computations (or comp types for short). Combined with singleton types for table and column names, comp types let us give database query methods type signatures that compute a table's schema to yield very precise type information. Comp types for hash, array, and string libraries can also increase precision and thereby reduce the need for type casts. We formalize CompRDL and prove its type system sound. Rather than type check the bodies of library methods with comp types---those methods may include native code or be complex---CompRDL inserts run-time checks to ensure library methods abide by their computed types. We evaluated CompRDL by writing annotations with type-level computations for several Ruby core libraries and database query APIs. We then used those annotations to type check two popular Ruby libraries and four Ruby on Rails web apps. We found the annotations were relatively compact and could successfully type check 132 methods across our subject programs. Moreover, the use of type-level computations allowed us to check more expressive properties, with fewer manually inserted casts, than was possible without type-level computations. In the process, we found two type errors and a documentation error that were confirmed by the developers. Thus, we believe CompRDL is an important step forward in bringing precise static type checking to dynamic languages. △ Less

Submitted 6 April, 2019; originally announced April 2019.

Comments: 22 pages, this is a technical report (with appendix) of a paper to appear in Programming Language Design and Implementation (PLDI 2019)

LWeb: Information Flow Security for Multi-tier Web Applications

Authors: James Parker, Niki Vazou, Michael Hicks

Abstract: This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod's core monad. Second, we extend Ye… ▽ More This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enforcement library with the Yesod web programming framework. The implementation has two parts. First, we extract the core of LIO into a monad transformer (LMonad) and then apply it to Yesod's core monad. Second, we extend Yesod's table definition DSL and query functionality to permit defining and enforcing label-based policies on tables and enforcing them during query processing. LWeb's policy language is expressive, permitting dynamic per-table and per-row policies. We formalize the essence of LWeb in the $λ_{LWeb}$ calculus and mechanize the proof of noninterference in Liquid Haskell. This mechanization constitutes the first metatheoretic proof carried out in Liquid Haskell. We also used LWeb to build a substantial web site hosting the Build it, Break it, Fix it security-oriented programming contest. The site involves 40 data tables and sophisticated policies. Compared to manually checking security policies, LWeb imposes a modest runtime overhead of between 2% to 21%. It reduces the trusted code base from the whole application to just 1% of the application code, and 21% of the code overall (when counting LWeb too). △ Less

Submitted 22 January, 2019; originally announced January 2019.

Journal ref: Proc. ACM Program. Lang., Vol. 3, No. POPL, Article 75 (January 2019)

Gradual Liquid Type Inference

Authors: Niki Vazou, Éric Tanter, David Van Horn

Abstract: Liquid ty** provides a decidable refinement inference mechanism that is convenient but subject to two major issues: (1) inference is global and requires top-level annotations, making it unsuitable for inference of modular code components and prohibiting its applicability to library code, and (2) inference failure results in obscure error messages. These difficulties seriously hamper the migratio… ▽ More Liquid ty** provides a decidable refinement inference mechanism that is convenient but subject to two major issues: (1) inference is global and requires top-level annotations, making it unsuitable for inference of modular code components and prohibiting its applicability to library code, and (2) inference failure results in obscure error messages. These difficulties seriously hamper the migration of existing code to use refinements. This paper shows that gradual liquid type inference---a novel combination of liquid inference and gradual refinement types---addresses both issues. Gradual refinement types, which support imprecise predicates that are optimistically interpreted, can be used in argument positions to constrain liquid inference so that the global inference process e effectively infers modular specifications usable for library components. Dually, when gradual refinements appear as the result of inference, they signal an inconsistency in the use of static refinements. Because liquid refinements are drawn from a nite set of predicates, in gradual liquid type inference we can enumerate the safe concretizations of each imprecise refinement, i.e. the static refinements that justify why a program is gradually well-typed. This enumeration is useful for static liquid type error explanation, since the safe concretizations exhibit all the potential inconsistencies that lead to static type errors. We develop the theory of gradual liquid type inference and explore its pragmatics in the setting of Liquid Haskell. △ Less

Submitted 30 October, 2019; v1 submitted 5 July, 2018; originally announced July 2018.

Comments: To appear at OOPSLA 2018

Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell)

Authors: Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton

Abstract: Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how equational reasoning can be performed directly and seamlessly within Haskell itself, and be checked using Liquid Haskell. In particular, language le… ▽ More Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manually on paper, or mechanised in a theorem prover. This article shows how equational reasoning can be performed directly and seamlessly within Haskell itself, and be checked using Liquid Haskell. In particular, language learners --- to whom external theorem provers are out of reach --- can benefit from having their proofs mechanically checked. Concretely, we show how the equational proofs and derivations from Graham's textbook can be recast as proofs in Haskell (spoiler: they look essentially the same). △ Less

Submitted 9 June, 2018; originally announced June 2018.

Comments: Submitted to Haskell'18

Refinement Types for Ruby

Authors: Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak

Abstract: Refinement types are a popular way to specify and reason about key program properties. In this paper, we introduce RTR, a new system that adds refinement types to Ruby. RTR is built on top of RDL, a Ruby type checker that provides basic type information for the verification process. RTR works by encoding its verification problems into Rosette, a solver-aided host language. RTR handles mixins throu… ▽ More Refinement types are a popular way to specify and reason about key program properties. In this paper, we introduce RTR, a new system that adds refinement types to Ruby. RTR is built on top of RDL, a Ruby type checker that provides basic type information for the verification process. RTR works by encoding its verification problems into Rosette, a solver-aided host language. RTR handles mixins through assume-guarantee reasoning and uses just-in-time verification for metaprogramming. We formalize RTR by showing a translation from a core, Ruby-like language with refinement types into Rosette. We apply RTR to check a range of functional correctness properties on six Ruby programs. We find that RTR can successfully verify key methods in these programs, taking only a few minutes to perform verification. △ Less

Submitted 25 November, 2017; originally announced November 2017.

Refinement Reflection: Complete Verification with SMT

Authors: Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala

Abstract: We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is instantiated in the SMT logic in a precise fashion that permits decidable verification. Reflection allows the user… ▽ More We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is instantiated in the SMT logic in a precise fashion that permits decidable verification. Reflection allows the user to write equational proofs of programs just by writing other programs using pattern-matching and recursion to perform case-splitting and induction. Thus, via the propositions-as-types principle, we show that reflection permits the specification of arbitrary functional correctness properties. Finally, we introduce a proof-search algorithm called Proof by Logical Evaluation that uses techniques from model checking and abstract interpretation, to completely automate equational reasoning. We have implemented reflection in Liquid Haskell and used it to verify that the widely used instances of the Monoid, Applicative, Functor, and Monad typeclasses actually satisfy key algebraic laws required to make the clients safe, and have used reflection to build the first library that actually verifies assumptions about associativity and ordering that are crucial for safe deterministic parallelism. △ Less

Submitted 9 November, 2017; originally announced November 2017.

Comments: 29 pages plus appendices, to appear in POPL 2018. arXiv admin note: text overlap with arXiv:1610.04641

Deriving Law-Abiding Instances

Authors: Ryan Scott, Vikraman Choudhury, Ryan Newton, Niki Vazou, Ranjit Jhala

Abstract: Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. But many of these proofs require routine, boilerplate code that is tedious to write. Moreover, many such proofs do not scale well, as the size of proof terms can grow superlinearly with the size of the datatypes involved i… ▽ More Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. But many of these proofs require routine, boilerplate code that is tedious to write. Moreover, many such proofs do not scale well, as the size of proof terms can grow superlinearly with the size of the datatypes involved in the proofs. We present a technique for programming with refinement reflection which solves this problem by leveraging datatype-generic programming. Our observation is that we can take any algebraic datatype, generate an equivalent representation type, and have Liquid Haskell automatically construct (and prove) an isomorphism between the original type and the representation type. This reduces many proofs down to easy theorems over simple algebraic "building block" types, allowing programmers to write generic proofs cheaply and cheerfully. △ Less

Submitted 7 August, 2017; originally announced August 2017.

ACM Class: D.3.2; D.1.1

Verified Parallel String Matching in Haskell

Authors: Niki Vazou, Jeff Polakow

Abstract: In this paper, we prove correctness of parallelizing a string matcher using Haskell as a theorem prover. We use refinement types to specify correctness properties, Haskell terms to express proofs and Liquid Haskell to check correctness of proofs. First, we specify and prove that a class of monoid morphisms can be parallelized via parallel monoid concatenation. Then, we encode string matching as a… ▽ More In this paper, we prove correctness of parallelizing a string matcher using Haskell as a theorem prover. We use refinement types to specify correctness properties, Haskell terms to express proofs and Liquid Haskell to check correctness of proofs. First, we specify and prove that a class of monoid morphisms can be parallelized via parallel monoid concatenation. Then, we encode string matching as a morphism to get a provably correct parallel transformation. Our 1839LoC prototype proof shows that Liquid Haskell can be used as a fully expressive theorem prover on realistic Haskell implementations. △ Less

Submitted 22 October, 2016; originally announced October 2016.

Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT)

Authors: Niki Vazou, Ranjit Jhala

Abstract: Refinement Reflection turns your favorite programming language into a proof assistant by reflecting the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is unfolded into the refinement logic in a precise, predictable and most importantly, programmer controllable way. In the logic, we encode fu… ▽ More Refinement Reflection turns your favorite programming language into a proof assistant by reflecting the code implementing a user-defined function into the function's (output) refinement type. As a consequence, at uses of the function, the function definition is unfolded into the refinement logic in a precise, predictable and most importantly, programmer controllable way. In the logic, we encode functions and lambdas using uninterpreted symbols preserving SMT-based decidable verification. In the language, we provide a library of combinators that lets programmers compose proofs from basic refinements and function definitions. We have implemented our approach in the Liquid Haskell system, thereby converting Haskell into an interactive proof assistant, that we used to verify a variety of properties ranging from arithmetic properties of higher order, recursive functions to the Monoid, Applicative, Functor and Monad type class laws for a variety of instances. △ Less

Submitted 14 October, 2016; originally announced October 2016.

Bounded Refinement Types

Authors: Niki Vazou, Alexander Bakst, Ranjit Jhala

Abstract: We present a notion of bounded quantification for refinement types and show how it expands the expressiveness of refinement ty** by using it to develop typed combinators for: (1) relational algebra and safe database access, (2) Floyd-Hoare logic within a state transformer monad equipped with combinators for branching and loo**, and (3) using the above to implement a refined IO monad that track… ▽ More We present a notion of bounded quantification for refinement types and show how it expands the expressiveness of refinement ty** by using it to develop typed combinators for: (1) relational algebra and safe database access, (2) Floyd-Hoare logic within a state transformer monad equipped with combinators for branching and loo**, and (3) using the above to implement a refined IO monad that tracks capabilities and resource usage. This leap in expressiveness comes via a translation to "ghost" functions, which lets us retain the automated and decidable SMT based checking and inference that makes refinement ty** effective in practice. △ Less

Submitted 1 July, 2015; originally announced July 2015.

Comments: 14 pages, International Conference on Functional Programming, ICFP 2015

ACM Class: D.2.4; D.3.3; F.3.1

Type Targeted Testing

Authors: Eric L. Seidel, Niki Vazou, Ranjit Jhala

Abstract: We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be viewed as a high-level, declarative, test generation technique, wherein types are converted to SMT queries whose models can be decoded into concrete program inputs… ▽ More We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that through the lens of SMT solvers, refinement types can also be viewed as a high-level, declarative, test generation technique, wherein types are converted to SMT queries whose models can be decoded into concrete program inputs. Our approach enables the systematic and exhaustive testing of implementations from high-level declarative specifications, and furthermore, provides a gradual path from testing to full verification. We have implemented our approach as a Haskell testing tool called TARGET, and present an evaluation that shows how TARGET can be used to test a wide variety of properties and how it compares against state-of-the-art testing approaches. △ Less

Submitted 15 January, 2015; v1 submitted 20 October, 2014; originally announced October 2014.

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages

Authors: Niki Vazou, Eric L. Seidel, Ranjit Jhala

Abstract: SMT-based verifiers have long been an effective means of ensuring safety properties of programs. While these techniques are well understood, we show that they implicitly require eager semantics; directly applying them to a lazy language is unsound due to the presence of divergent sub-computations. We recover soundness by composing the safety analysis with a termination analysis. Of course, termina… ▽ More SMT-based verifiers have long been an effective means of ensuring safety properties of programs. While these techniques are well understood, we show that they implicitly require eager semantics; directly applying them to a lazy language is unsound due to the presence of divergent sub-computations. We recover soundness by composing the safety analysis with a termination analysis. Of course, termination is itself a challenging problem, but we show how the safety analysis can be used to ensure termination, thereby bootstrap** soundness for the entire system. Thus, while safety invariants have long been required to prove termination, we show how termination proofs can be to soundly establish safety. We have implemented our approach in liquidHaskell, a Refinement Type-based verifier for Haskell. We demonstrate its effectiveness via an experimental evaluation using liquidHaskell to verify safety, functional correctness and termination properties of real-world Haskell libraries, totaling over 10,000 lines of code. △ Less

Submitted 23 January, 2014; originally announced January 2014.