ARIA
Contents:
Getting Started
Logic and Solving
Proofs and Explanations
Quantified Reasoning
Automata and Languages
Verification
Abstraction
Symbolic Abstraction
Predicate Abstraction
Predicate Abstraction and CEGAR
Monadic Predicate Abstraction
Abstract Interpretation
Counting, Sampling, and Probability
Program Synthesis
Logic Programming
LLM and ML
CLI and Tools
Global Parameters
ARIA
Abstraction
View page source
Abstraction
Symbolic Abstraction
Overview
EFMC Symbolic Abstraction Prover
Core Concepts
Abstract Interpretation (ai_symabs)
OMT-based Symbolic Abstraction (omt_symabs)
Predicate Abstraction (predicate_abstraction)
Additional Components
Usage Examples
Applications
Performance Considerations
Future Directions
References
Predicate Abstraction
Introduction to Predicate Abstraction
Implementation in aria
Example Usage
Advanced Topics
References
Predicate Abstraction and CEGAR
Current engine surface
Programmatic usage
Relationship to other docs
Monadic Predicate Abstraction
Package layout
Current API note
Example imports
Overview
Abstract Interpretation
Current codebase note
Related package areas
Concepts
References