HASLab  Indexed Articles in Conferences
Permanent URI for this collection
Browse
Browsing HASLab  Indexed Articles in Conferences by Author "5605"
Results Per Page
Sort Options

ItemA Generalized Program Verification Workflow Based on Loop Elimination and SA Form( 2019) Belo Lourenco,C ; Maria João Frade ; Jorge Sousa Pinto ; 5605 ; 5595This paper presents a minimal model of the functioning of program verification and property checking tools based on (i) the encoding of loops as noniterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediate singleassignment (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 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 technique based on a conservative encoding of invariantannotated loops with assume/assert in SA form, as well as the first soundness proof based on a program logic. © 2019 IEEE.

ItemPermutability in proof terms for intuitionistic sequent calculus with cuts( 2018) Maria João Frade ; Santo,JE ; Pinto,L ; 5605This 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 computationasproofnormalization and the computationasproofsearch 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 cutfree. 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 cutfree, normal, and focused proofs. © José Espírito Santo, Maria João Frade, and Luís Pinto; licensed under Creative Commons License CCBY 22nd International Conference on Types for Proofs and Programs (TYPES 2016).