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
Abstraction Interpretation
Widening
Making Abstraction Interpretation Complete
Counting, Sampling, and Probability
Program Synthesis
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
Predicate Abstraction
Abstraction Refinement
References
Monadic Predicate Abstraction
Introduction to Monadic Predicate Abstraction
Monadic Predicate Abstraction in Aria
Usage Example
Performance Comparison
References
Abstraction Interpretation
Chaotic Iteration
Widening
Systematic Abstraction
Making Abstraction Interpretation Complete
Abstract Interpretation Tools
References