Algebraic formal methods for program verification

• Grant number: 13/04734-9
• Support Opportunities: Scholarships abroad - Research Internship - Post-doctor
• Start date: April 30, 2013
• End date: April 29, 2014
• Field of knowledge: Physical Sciences and Mathematics - Computer Science - Theory of Computation
• Principal Investigator: Arnaldo Vieira Moura
• Grantee: Rachid Rebiha
• Supervisor: Nadir Matringe
• Host Institution: Instituto de Computação (IC). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brazil
• Institution abroad: Université de Poitiers, France
• Associated to the scholarship: 11/08947-1 - Algebraic Formal Methods for Invariant Generation., BP.PD

Abstract

This proposal aims at, primarely, to investigate the reductions from program static analysis problems (like invariant generation, automatic program termination analysis, etc) to Linear Algebra problems. In the research direction of new formal methods for static analysis our research agenda will focus on the development of associated efficient algorithms for these problems. We will strive to build the foundations for new and efficient techniques that will support new algorithms to automate deductive processes, and will allow for new algorithms for the verification of complex systems, in order to check for safety and liveness properties.We will be able to implement new computational methods capable of automating the discovery of relationships between program variables whose programs can exhibit loops, as well as systems and function calls. The generalization of theoretical results nowadays in use in techniques for automatic proof of termination, and the development of efficient computational methods for static analysis of program termination would be one of the main goals of our project. (AU)

Scientific publications

(References retrieved automatically from Web of Science and SciELO through information on FAPESP grants and their corresponding numbers as mentioned in the publications by the authors)

REBIHA, RACHID; MOURA, ARNALDO V.; MATRINGE, NADIR. Generating invariants for non-linear hybrid systems. THEORETICAL COMPUTER SCIENCE, v. 594, p. 180-200, AUG 23 2015. (11/08947-1, 13/04734-9)

REBIHA, RACHID; MOURA, ARNALDO VIEIRA; MATRINGE, NADIR. Generating invariants for non-linear loops by linear algebraic methods. FORMAL ASPECTS OF COMPUTING, v. 27, n. 5-6, p. 805-829, NOV 2015. (11/08947-1, 13/04734-9)