Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification

Maximiliano Cristiá, Gianfranco Rossi

TL;DR

We address the automation gap in automated software verification by combining prescriptive type checking with set constraint solving in the CLP language {log}. The approach defines a Hindley-Milner–style type system for {log}, implements a typechecker, and integrates it with the existing {log} solver so programs can be typed, executed, and proven automatically. The authors prove type safety in this typed CLP setting and demonstrate practicality with two industrial-strength case studies (Landing Gear System and Android permission model) where many verification conditions are discharged automatically. The results indicate that the hybrid approach yields substantial automation and reduces manual proof effort, suggesting a viable path for typed, set-based verification systems.

Abstract

In this paper we show how prescritive type checking and constraint solving can be combined to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read `setlog'), a Constraint Logic Programming (CLP) language and satisfiability solver based on set theory. Hence, we proceed as follows: a) a type system for {log} is defined; b) the constraint solver is proved to be safe w.r.t. the type system; c) the implementation of a concrete typechecker is presented; d) the integration of type checking and set constraint solving to increase automation during software verification is discussed; and f) two industrial-strength case studies are presented where this combination is used with very good results. Under consideration in Theory and Practice of Logic Programming (TPLP)

Combining Type Checking and Set Constraint Solving to Improve Automated Software Verification

TL;DR

We address the automation gap in automated software verification by combining prescriptive type checking with set constraint solving in the CLP language {log}. The approach defines a Hindley-Milner–style type system for {log}, implements a typechecker, and integrates it with the existing {log} solver so programs can be typed, executed, and proven automatically. The authors prove type safety in this typed CLP setting and demonstrate practicality with two industrial-strength case studies (Landing Gear System and Android permission model) where many verification conditions are discharged automatically. The results indicate that the hybrid approach yields substantial automation and reduces manual proof effort, suggesting a viable path for typed, set-based verification systems.

Abstract

In this paper we show how prescritive type checking and constraint solving can be combined to increase automation during software verification. We do so by defining a type system and implementing a typechecker for {log} (read `setlog'), a Constraint Logic Programming (CLP) language and satisfiability solver based on set theory. Hence, we proceed as follows: a) a type system for {log} is defined; b) the constraint solver is proved to be safe w.r.t. the type system; c) the implementation of a concrete typechecker is presented; d) the integration of type checking and set constraint solving to increase automation during software verification is discussed; and f) two industrial-strength case studies are presented where this combination is used with very good results. Under consideration in Theory and Practice of Logic Programming (TPLP)
Paper Structure (16 sections, 1 theorem, 12 equations, 4 figures)

This paper contains 16 sections, 1 theorem, 12 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Combining type checking and constraint solving
  3. Typechecking and formally verifying a simple library system
  4. A type system for $\{log\}$
  5. Expressiveness.
  6. Type safety
  7. The $\{log\}$ constraint solver
  8. Proving type safety
  9. Implementation
  10. Introducing parametric polymorphism
  11. Dealing with finite types
  12. Case studies
  13. The Landing Gear System.
  14. Android Permission System.
  15. Discussion and related work
  16. ...and 1 more sections

Key Result

Theorem 1

Consider any $\{log\}$ constraint $\pi$. Let $t_1:\tau_1, \dots, t_k:\tau_k$ be such that $\pi(t_1,\dots,t_k)$ is a well-typed constraint. Then ($\longrightarrow$ denotes any $\{log\}$ rewrite rule):

Figures (4)

  • Figure 1: Type rules for function symbols
  • Figure 2: Type rules for predicate symbols in $\Pi_C$
  • Figure 3: Some rewrite rules implemented by $\mathit{SAT}_{\{\cdot\}}$
  • Figure 4: Graphical depiction of the four phases implemented by the typechecker

Theorems & Definitions (6)

  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Example 5
  • Theorem 1: $\{log\}$ is type safe