American University of Beirut

Automated Reasoning for Program Correctness (ARPC)

​​At ARPC 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.​​

Fadi Zaraket​, Paul Attie​

Contact Us

For various questions, please try contacting us via social media first!
read more

Privacy Statement

We take data privacy seriously and adhere to all applicable data privacy laws and regulations.
read more

Copyright and Disclaimer

Written permission is needed to copy or disseminate all or part of the materials on the AUB website.
read more

Title IX, Non-Discrimination, and Anti-Discriminatory Harassment

AUB is committed to providing a safe, respectful, and inclusive environment to all members of its community.
read more