Presburger Automata
From MaRDI portal
Software:40317
swMATH28603MaRDI QIDQ40317FDOQ40317
Author name not available (Why is that?)
Cited In (8)
- A formalisation of the Myhill-Nerode theorem based on regular expressions
- Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments
- Regular language representations in the constructive type theory of Coq
- Verified decision procedures for MSO on words based on derivatives of regular expressions
- Partial and nested recursive function definitions in higher-order logic
- Two-Way Automata in Coq
- A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
- Automatic refinement to efficient data structures: a comparison of two approaches
This page was built for software: Presburger Automata
