Abstract
This entry provides a formalization of the abstract theory of ample
set partial order reduction. The formalization includes transition
systems with actions, trace theory, as well as basics on finite,
infinite, and lazy sequences. We also provide a basic framework for
static analysis on concurrent systems with respect to the ample set
condition.
License
Topics
Session Partial_Order_Reduction
- List_Prefixes
- List_Extensions
- Word_Prefixes
- Set_Extensions
- Basic_Extensions
- Relation_Extensions
- Transition_System_Extensions
- Traces
- Transition_System_Traces
- Functions
- ENat_Extensions
- CCPO_Extensions
- ESet_Extensions
- Coinductive_List_Extensions
- LList_Prefixes
- Stuttering
- Transition_System_Interpreted_Traces
- Ample_Abstract
- Formula
- Ample_Correctness
- Ample_Analysis