Symbolic analysis by using folding narrowing with irreducibility and SMT constra...
summary
Claims a new symbolic reachability engine that uses folding SMT canonical narrowing in Maude to turn some infinite narrowing trees into finite graphs, combining irreducibility constraints and SMT conditions on rules. Prototype plus textual UI implements graph-folding, calls the SMT solver used by Maude, and models an extended parametric timed-automaton vending machine (money and counters). Results show termination where standard narrowing diverges and answer existential and fully parametric reachability queries (e.g., “>=3 coffees and $2 left”) successfully; code on GitHub.
AI-written summary · about
chapters (15)
- 0:00Symbolic analysis with narrowing
- 1:10Parametric timed automata basics
- 2:31Folding narrowing with SMT
- 5:49Folding narrowing for state space
- 6:11Narrowing coffee machine example
- 11:14Coffee machine parametric automaton
- 14:54Enhanced coffee machine model
- 17:01Encoding quarters vs integers
- 18:05Data structures for folding narrowing
- 20:54Execution with folding narrowing
- 24:11Conclusions on narrowing techniques
- 25:56Q&A: Parametric automaton model
- 27:20Q&A: Folding narrowing soundness
- 28:03Q&A: Global rules in narrowing
- 30:28Q&A: Mixing narrowing and SMT
related talks
25mCertified Symbolic Finite Transducers: Formalization and Applications to String Analysis
58mAutomating Relational Verification of Infinite-State Programs
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...
19mMechanized Logical Relations for Termination-Insensitive Noninterference
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
19mInference of Robust Reachability Constraints
23mSecurity Reasoning via Substructural Dependency Tracking