Publications

Almeida JB, Frade MJ, Pinto JS, Sousa SM.  2011.  Rigorous Software Development: an introduction to program verification. AbstractWebsite

The use of mathematical methods in the development of software is essential when reliable systems are sought; in particular they are now strongly recommended by the official norms adopted in the production of critical software. Program Verification is the area of computer science that studies mathematical methods for checking that a program conforms to its specification. This text is a self-contained introduction to program verification using logic-based methods, presented in the broader context of formal methods for software engineering. The idea of specifying the behaviour of individual software components by attaching contracts to them is now a widely followed approach in program development, which has given rise notably to the development of a number of behavioural interface specification languages and program verification tools. A foundation for the static verification of programs based on contract-annotated routines is laid out in the book. These can be independently verified, which provides a modular approach to the verification of software. The text assumes only basic knowledge of standard mathematical concepts that should be familiar to any computer science student. It includes a self-contained introduction to propositional logic and first-order reasoning with theories, followed by a study of program verification that combines theoretical and practical aspects -- from a program logic (a variant of Hoare logic for programs containing user-provided annotations) to the use of a realistic tool for the verification of C programs (annotated using the ACSL specification language), through the generation of verification conditions and the static verification of runtime errors.

Lourenço CB, Frade MJ, Pinto JS.  2016.  Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. Programming Languages and Systems - 25th European Symposium on Programming, {ESOP} 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 9632:41–67. Abstractesop2016.pdf

Deductive verification tools typically rely on the conversion of code to a single-assignment (SA) form. In this paper we formalize pro- gram verification based on the translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct, and the subsequent generation of compact, indeed linear-size, verification conditions. Soundness and completeness proofs are given for the entire workflow, including the translation of an- notated programs to SA form. The formalization is based on a program logic that we show to be adaptation-complete. Although this important property has not, as far as we know, been established for any existing program verification tool, we believe that adaptation-completeness is one of the major motivations for the use of SA form as an intermediate lan- guage. Our results here show that indeed this allows for the tools to achieve the maximum degree of adaptation when handling subprograms.

Lourenço CB, Frade MJ, Pinto JS.  2014.  A Bounded Model Checker for SPARK Programs. Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis. Abstracttool-paper-atva2014.pdf

This paper discusses the design and implementation of a bounded model checker for SPARK code, and provides a proof of concept of the utility and practicality of bounded verification for SPARK.

Miraldo VC, Frade MJ, Lourenço CB, Pinto JS.  2013.  Experimenting with Predicate Abstraction. Proceedings of Simpósio de Informática - Inforum. Abstractpredabs-final.pdf

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 generate the model. In this paper we explain how we have implemented and optimized one such technique, that produces the most precise existential abstraction of a program, and give the first steps towards establishing a common framework for both this direct technique and a second one, based on cartesian abstraction by weakest precondition calculations.

Lourenço CB, Miraldo VC, Frade MJ, Pinto JS.  2013.  SPARK-BMC: Checking SPARK Code for Bugs. Proceedings of Simpósio de Informática - Inforum (SETR track) . Abstractpaper-short-final.pdf

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.

Cruz D, Frade MJ, Pinto JS.  2012.  Verification conditions for single-assignment programs. Proceedings of the 27th Annual Symposium on Applied Computing - SAC. :1264–1270. Abstractverification-conditions-revised.pdf

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 conditions. Our study is carried on in the context of a While language. Important extensions to this language are considered toward the end of the paper. We also briefly survey modern program verification tools and their approaches to the generation of verification conditions.

Frade MJ, Saabas A, Uustalu T.  2009.  Bidirectional data-flow analyses, type-systematically. PEPM. :141-150. Abstractpepm09-revised.pdf

We show that a wide class of bidirectional data-flow analyses and program optimizations based on them admit declarative descriptions in the form of type systems. The salient feature is a clear separation between what constitutes a valid analysis and how the strongest one can be computed (via the type checking versus principal type inference distinction). The approach also facilitates elegant relational semantic soundness definitions and proofs for analyses and optimizations, with an application to mechanical transformation of program proofs, useful in proof-carrying code. Unidirectional forward and backward analyses are covered as special cases; the technicalities in the general bidirectional case arise from more subtle notions of valid and principal types. To demonstrate the viability of the approach we consider two examples that are inherently bidirectional: type inference (seen as a data-flow problem) for a structured language where the type of a variable may change over a program's run and the analysis underlying a stack usage optimization for a stack-based low-level language.

Frade MJ, Saabas A, Uustalu T.  2007.  Foundational certification of data-flow analyses. 1st IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering - TASE . :107-116. Abstracttase-final.pdf

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 variables analysis, we show that analysis type systems are applied versions of more foundational Hoare logics describing either the same abstract property semantics as the type system (liveness states) or a more concrete natural semantics on transition traces of a suitable kind (future defs and uses). The rules of the type system are derivable in the Hoare logic for the abstract property semantics and those in turn in the Hoare logic for the transition trace semantics. This reduction of the burden of trusting the certification vehicle can be compared to foundational proof-carrying code, where general-purpose program logics are preferred to special-purpose type systems and universal logic to program logics.

We also look at conditional liveness analysis to see that the same foundational development is also possible for conditional data-flow analyses proceeding from type systems for combined “standard state and abstract property” semantics.

Santo JE, Frade MJ, Pinto L.  2006.  Structural Proof Theory as Rewriting. Proceedings of 17th International Conference on Term Rewriting and Applications - RTA. :197-211. Abstractstrproofthrewrtcameraready.pdf

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 a suitable tool for doing structural proof theory as rewriting. As an illustration, we investigate combinations of reduction and permutation rules and whether these combinations induce rewriting systems which are confluent and terminating. In some cases, the combination allows the simulation of non-terminating reduction sequences known from explicit substitution calculi. In other cases, we succeed in capturing interesting classes of derivations as the normal forms w.r.t. well-behaved combinations of rules. We identify six of these "combined'' normal forms, among which are two classes, due to Herbelin and Mints, in bijection with normal, ordinary natural deductions. A computational explanation for the variety of ``combined'' normal forms is the existence of three ways of expressing multiple application in the calculus.

Barthe G, Frade MJ.  1999.  Constructor Subtyping. Proceedings of 8th European Symposium on Programming Languages and Systems - ESOP. 1576:109-127. Abstractesop99.pdf

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 constructor subtyping. In the first part of the paper, we show that the calculus is confluent and strongly normalizing. In the second part of the paper, we show that the calculus admits a well-behaved theory of canonical inhabitants, provided one adopts expansive extensionality rules, including eta-expansion, surjective pairing, and a suitable expansion rule for datatypes. Finally, in the third part of the paper, we extend our calculus with unbounded recursion and show that confluence is preserved.

Lourenço CB, Frade MJ, Pinto JS.  2016.  A Single-Assignment Translation for Annotated Programs. CoRR. abs/1601.00584 Abstractsatranslation.pdfWebsite

We present a translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct. We prove that the translation is sound and complete. This is a companion report to our paper Formalizing Single-assignment Program Verification: an Adaptation-complete Approach.

Frade MJ, Pinto JS.  2011.  Verification conditions for source-level imperative programs. Computer Science Review. 5(3):252–277. Abstractverification-conditions-revised_2.pdf

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 conditions. Our study is carried on in the context of a While language. Important extensions to this language are considered toward the end of the paper. We also briefly survey modern program verification tools and their approaches to the generation of verification conditions.

Barthe G, Frade MJ, Giménez E, Pinto L, Uustalu T.  2004.  Type-based termination of recursive definitions. Mathematical Structures in Computer Science. 14:97-141. Abstracttbterm.pdf

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 also support coinductive types and corecursive function definitions.

Frade MJ.  2004.  Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi. Abstractthesis.pdf

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 defined sets.
The first part of the thesis presents a mechanism that ensures termination through types and defines a system that incorporates it. More precisely, we formalize the notion of type-based termination using a restricted form of type dependency (also known as indexed types). Every datatype is replaced by a family of approximations indexed over a set of stages; then being in a certain approximation means that a term can be seen as having a certain bound on constructor usage. We introduce λˆ, a simply typed λ-calculus à la Curry, supporting parametric inductive datatypes, case-expressions and letrec-expressions with termination ensured by types. We show that λˆ enjoys important meta-theoretical properties, including confluence, subject reduction and strong normalization. We also show that the calculus is powerful enough to encode many recursive definitions rejected by existing type systems, and give some examples. We prove that this system encompasses in a strict way Giménez' λς, a system in which termination of typable expressions is ensured by a syntactical condition constraining the uses of recursive calls in the body of definitions.
The second part of the thesis studies properties of a type system featuring constructor subtyping. Constructor subtyping is a form of subtyping in which an inductive type σ is viewed as a subtype of another inductive type τ if each constructor c of σ is also a constructor of τ (but τ may have more constructors), and whenever c : θ'→σ is a declaration for τ, then c : θ'→τ is a declaration for τ with θ'→≤θ'. In this thesis we allow for this form of subtyping in the system λcs, which is a simply typed λ-calculus à la Curry, supporting mutually recursive parametric datatypes, case-expressions and letrec-expressions. We establish the properties of confluence, subject reduction and decidability of type checking for this calculus. As the system features general recursion, the reduction calculus is obviously non-terminating. However, we sketch two ways of achieving strong normalization. One way is to constrain the system to guard-by-destructors recursion, following what is done for λς. The other way is to enrich the type system with stages (following the ideas presented for λˆ) and enforcing termination through typing. Potential uses of constructor subtyping include proof assistants and functional programming languages. In particular, constructor subtyping provides a suitable foundation for extensible datatypes, and is specially adequate to re-usability. The combination of subtyping between datatypes and overloading of constructors allows the definition of new datatypes by restricting or by expanding the set of constructors of an already defined datatype. This flexibility in the definition of datatypes induces a convenient form of code reuse for recursive functions, allowing the definition of new functions by restricting or by expanding already defined ones. We enrich a calculus featuring constructor subtyping with a mechanism to define extensible overloaded recursive functions by pattern-matching, obtaining the system λcs+fun. We formalize the concept of well-formed environment of function declarations and establish that under such environments the properties of confluence, subject reduction and decidability of type-checking hold. Moreover, we prove that the requirements imposed for the well-formed environments are decidable and show how standard techniques can still be used for compiling pattern-matching into case-expressions.

Frade MJ.  1995.  Comportamento e Estado. Abstractcompest.pdf

In this work we introduce a formalism for specifying the behaviour of computational systems, based on logic.
Our basic unit of software specification is called agent and is nothing more than a particular logical system. The agent logical language allow us to express the relationship between the occurrence of events and the properties an agent exhibits. The events are seen as logical connectives and the logical assertions reflect the causality between events and properties - the essential cause of a property in face of an event.
Because we are interested in knowing which sequence of events “justify” a property, we have traces coming from the past to the present. Our perspective is that of knowing which behaviour could justify the characteristics of au agent in some instant. Obviously, these characteristics will condition the future behaviour of the agent. This dependency is expressed in a deduction system that reflects the notion of causality.
For the purpose of characterizing the agents semantically a connection is made between the logical system and its topological models. The Stone duality provides a junction between the logical system and its semantics and it provides two alternative perspectives:
the algebraic or logical perspective and the topological perspective.
We present two types of models for the agents: the trace model, a denotational model intimately connected to the notion of event and trace, and the state model, au operational model based on the notions of state and state transitions.
We establish a relation between these two types of models: we see how a state model may be obtained from a trace model. The states arise as equivalence classes of past behaviours. We also study the properties of the state models which result from the conversion of trace models. We see how topological properties — such as separation conditions, soberty and coherence — characterize the state space of these modeis, and how from behaviour we can generate a minimal state space.