Encontrados 15 documentos, a visualizar página 1 de 2

Experimenting with predicate abstraction

Predicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may differ based on (i) the set of predicates used; or (ii) the algorithmic technique employed to gen- erate the model. In this paper we explain how we have implemented...

SPARK-BMC : checking SPARK code for bugs

The standard SPARK deductive verification tools, based on contracts, are not practical in early stages when the idea is only bug catching. We discuss the implementation of a bounded model checker for SPARK, focusing on specific challenges of this language. Our tool is fully automatic, complementing the existing tools for SPARK.

Verification conditions for source-level imperative programs

This paper is a systematic study of verification conditions and their use in the context of program verification. We take Hoare logic as a starting point and study in detail how a verification conditions generator can be obtained from it. The notion of program annotation is essential in this process. Weakest preconditions and the use of updates are also studied as alternative approaches to verification conditio...

Foundational certification of data-flow analyses

Data-flow analyses, such as live variables analysis, available expressions analysis etc., are usefully specifiable as type systems. These are sound and, in the case of distributive analysis frameworks, complete wrt. appropriate natural semantics on abstract properties. Applications include certification of analyses and "optimization" of functional correctness proofs alongside programs. On the example of live v...

Structural proof theory as rewriting

The multiary version of the $\lambda$-calculus with generalized applications integrates smoothly both a fragment of sequent calculus and the system of natural deduction of von Plato. It is equipped with reduction rules (corresponding to cut-elimination/normalisation rules) and permutation rules, typical of sequent calculus and of natural deduction with generalised elimination rules. We argue that this system is...

Type-based termination of recursive definitions

This paper introduces "lambda-hat", a simply typed lambda calculus supporting inductive types and recursive function definitions with termination ensured by types. The system is shown to enjoy subject reduction, strong normalisation of typable terms and to be stronger than a related system "lambda-G" in which termination is ensured by a syntactic guard condition. The system can, at will, be extended to ...

Type-based termination of recursive definitions and constructor subtyping in ty...

Tese de doutoramento em Informática, ramo de Fundamentos da Computação. ; In type systems, a combination of subtyping and overloading is a way to achieve more precise typings. This thesis explores how to use these mechanisms in two directions: (i) as a way to ensure termination of recursive functions; (ii) as a way to capture in a type-theoretic context the use of subtyping as inclusion between inductively def...

Constructor subtyping

Constructor subtyping is a form of subtyping in which an inductive type A is viewed as a subtype of another inductive type B if B has more constructors than A. Its (potential) uses include proof assistants and functional programming languages. In this paper, we introduce and study the properties of a simply typed lambda-calculus with record types and datatypes, and which supports record subtyping and construct...

Constructor subtyping : extended version

Constructor subtyping is a form of subtyping in which an inductive type $\sigma$ is viewed as a subtype of another inductive type $\tau$ if $\tau$ has more elements than $\sigma$. Its (potential) uses include proof assistants and functional programming languages. In this report, we introduce and study the properties of a simply typed $\lambda$-calculus which supports constructor subtyping. We show that the ca...

Sebenta prática de elementos lógicos da programação I : guiões das sessões labo...