At PCA-Lab we build theories and supporting tools to enhance program correctness automation. The theories define (1) program data elements such as types, operations and relations, (2) program control elements such as conditionals, loops and functions, and (3) program correctness elements such as test cases, oracles, coverage criteria, assertions, pre-conditions, post-conditions and invariants. The aim is to establish that the program data and control elements satisfy the program correctness elements either by (i) analysis (static and dynamic) or by (ii) synthesis (construction). The supporting tools use structural analysis, logic solvers and model checkers to automate the process.
Maya Safieddine, PhD student
Kassem Fawaz,
Mohamad Fawaz
Mohamad Noureddine, Masters student
Mohamad Sakr, Masters student
Joan Farjo, Masters student
Farah Hariri, Senior student