Program Correctness Automation Lab

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

Graduating students

Kassem Fawaz,

Mohamad Fawaz

Mohamad Noureddine, Masters student

Mohamad Sakr, Masters student

Joan Farjo, Masters student

Farah Hariri, Senior student

Join the team


Specification Construction

Coverage Specifications

Concern Separation for Design For Testing Logic

Deadlock Analysis of Distributed Behavior, Interaction, Port Distributed Computing systems

Program Analysis with Decision and Transformation Algorithms

Synthesis of LTL SERE Formulae

Visualization of Dependency Chains

Property Based Coverage

Automated GUI Testing

Code Repositories

Code of Conduct

start.txt · Last modified: 2020/07/13 12:31 (external edit)
Except where otherwise noted, content on this wiki is licensed under the following license:CC Attribution-Noncommercial-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki