Formal Methods of Computation: Program Verification

Researchers (from FMC  and LCC groups)

    Simão Melo de Sousa, David Pereira and Nelma Moreira

Proof-carrying code (PCC) aims in providing static security enforcement mechanisms based on the notion of safety certificate. Every PCC architecture defines a  balance between the expressiveness of the safety and security requirements and the complexity of its formal enforcement.

Our approach is twofold:
1) Modern PCC architecture advocate the proof/certificate construction at the source (programming language) level. In the context of building an innovative proof carrying code platform for embedded systems we plan to investigate and design a proof contruction system that includes an annotation system, a verification conditions generator, an adequate proof system and the design of compilers that are able to cope with source program that come with safety proofs (a.k.a. proof tranforming compilers).
2) In the same lines, temporal logics have been successfully applied to hardware verification and more recently to formal verification of software, mainly in the context of model checking. Kleene algebras with tests subsume Hoare logics and have been used for program static analysis. Both approaches have decidable decision problems and we plan to investigate their feasibility to the automatic production of certificates (instead of relying in a proof assistant) in the context of PCC.

Researchers (from FMC and  APS groups)

    Mário Florido, Hugo Simões and Pedro Vasconcelos

Resource analysis: Definition of type-and-effect systems based to derive costs of programs for polymorphic, higher-order functional languages. Work in colaboration with the Advanced Programming Systems Group. More
information here.
 

[Go back]