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.  2019.  A generalized program verification workflow based on loop elimination and {SA} form. Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019.. :75–84. Abstractmain.pdf

This paper presents a minimal model of the func- tioning of program verification and property checking tools based on (i) the encoding of loops as non-iterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediate single-assignment (SA) form. The model captures the basic workflow of tools like Boogie, Why3, or CBMC, building on a clear distinction between operational and axiomatic semantics. This allows us to consider separately the soundness of program annotation, loop encoding, translation into SA form, and verification condition (VC) generation, as well as appropriate notions of completeness for each of these processes.
To the best of our knowledge, this is the first formalization of a bounded model checking of software technique, including soundness and completeness proofs using Hoare logic; we also give the first completeness proof of a deductive verification tech- nique based on a conservative encoding of invariant-annotated loops with assume/assert in SA form, as well as the first soundness proof based on a program logic.

Lourenço CB, Frade MJ, Nakajima S, Pinto JS.  2018.  A Generalized Approach to Verification Condition Generation. 2018 {IEEE} 42nd Annual Computer Software and Applications Conference, {COMPSAC} 2018, Tokyo, Japan, 23-27 July 2018, Volume 1. :194–203. Abstractmain.pdf

In a world where many human lives depend on the correct behavior of software systems, program verification as- sumes a crucial role. Many verification tools rely on an algorithm that generates verification conditions (VCs) from code annotated with properties to be checked. In this paper, we revisit two major methods that are widely used to produce VCs: predicate transformers (used mostly by deductive verification tools) and the conditional normal form transformation (used in bounded model checking of software). We identify three different aspects in which the methods differ (logical encoding of control flow, use of contexts, and semantics of asserts), and show that, since they are orthogonal, they can be freely combined. This results in six new hybrid verification condition generators (VCGens), which together with the fundamental methods constitute what we call the VCGen cube. We consider two optimizations implemented in major program verification tools and show that each of them can in fact be applied to an entire face of the cube, resulting in optimized versions of the six hybrid VCGens. Finally, we compare all VCGens empirically using a number of benchmarks. Although the results do not indicate absolute superiority of any given method, they do allow us to identify interesting patterns.

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.

Santo JE, Frade MJ, Pinto L.  2016.  Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. 22nd International Conference on Types for Proofs and Programs, {TYPES} 2016, May 23-26, 2016, Novi Sad, Serbia. 97:10:1–10:27. Abstractlipics-types-2016-10thepublishedversion.pdf

This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computation-as-proof-normalization and the computation-as-proof-search paradigms. The vehicle of the study is a λ-calculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cut-free. Natural proofs form a subsystem with a transparent Curry- Howard interpretation (a kind of formal vector notation for λ-terms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cut-free, normal, and focused proofs.

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.