OPPAS

Operator-Precedence Program Analysis Suite

OPPAS includes two tools: POMC and POPACheck.

POMC is a model checker for recursive programs. POMC models procedural programs as pushdown automata, and checks them against requirements expressed as Linear Temporal Logic (LTL) and Precedence-Oriented Temporal Logic (POTL) formulas.

POPACheck is an extension of POMC towards probabilistic programs with nested queries. It automatically models programs as probabilistic Operator Precedence Automata (pOPA). It supports model checking of LTL and a fragment of POTL, called POTLf\(\chi\). Given a probabilistic program and a formula in either LTL or POTLf\(\chi\), POPACheck can solve both qualitative and quantitative model checking queries. Additionally, it can compute (approximately) the program’s termination probability. Computing termination probabilities is a central problem in probabilistic pushdown model checking and amounts to computing the Least Fixed Point solution of a Positive Polynomial System (PPS).

This is a reference guide to POMC’s and POPACheck’s usage and describes their architecture at a high level.

Contents:

• Introduction and Context
  • POTL
  • POMC
  • POPACheck
• Installation
  • Binary Files
  • Compile from Sources
• Input Programs
  • Common syntax
  • MiniProc Syntax
  • MiniProb Syntax
• Writing Requirements
• Using POMC
  • Usage
  • Input Format
  • Benchmarks
• Using POPACheck
  • Usage
  • Input Format
  • Interpreting the output
• Development Information
  • Source Code
  • Test Suite
  • Credits
• Bibliography