Содержание
- 2. Software Analysis Analysis tool Model checking Static analysis Deductive reasoning Testing Runtime monitoring Product M Specification
- 3. do { KeAcquireSpinLock(); nPacketsOld = nPackets; if(request){ request = request->Next; KeReleaseSpinLock(); nPackets++; } } while (nPackets
- 4. Appeal of Regular Languages Well-understood expressiveness: multiple characterizations Deterministic/nondeterministic/alternating finite automata Regular expressions Monadic second order
- 5. Checking Structured Programs Control-flow requires stack, so (abstracted) program P defines a context-free language Algorithms exist
- 6. Are Context-free Specs Interesting? Classical Hoare-style pre/post conditions If p holds when procedure A is invoked,
- 7. Checking Context-free Specs Many tools exist for checking specific properties Security research on stack inspection properties
- 8. Program Executions as Nested Words Program global int x; main() { x = 3; if P
- 9. Words: Data with linear order (Unordered) Trees: Data with hierarchical order Ordered Trees/Hedges: Data with hierarchical
- 10. Document Processing HTML Document CSR 2007 Ekaterinburg Park Inn Google Microsoft Query 1: Find documents that
- 11. Talk Overview Introduction to Nested Words Regular Languages of Nested Words Relation to Pushdown Automata and
- 12. Nested Shape: Linear sequence + Non-crossing nesting edges Nesting edges can be pending, Sequence can be
- 13. Linguistic Annotated Data Linguistic data stored as annotated sentences (eg. Penn Treebank) Sample query: Find nouns
- 14. RNA as a Nested Word Primary structure: Linear sequence of nucleotides (A, C, G, U) Secondary
- 15. Word operations: Prefixes, suffixes, concatenation, reverse
- 16. Tree operations: Inserting/deleting well-matched words Well-matched: no pending calls/returns
- 17. Nested Word Automata (NWA) a1 a2 a3 a4 a5 a6 a7 a8 a9 States Q, initial
- 18. Regular Languages of Nested Words A set of nested words is regular if there is a
- 19. Determinization Goal: Given a nondeterministic automaton A with states Q, construct an equivalent deterministic automaton B
- 20. Closure Properties The class of regular languages of nested words is effectively closed under many operations
- 21. Decision Problems Membership: Is a given nested word w accepted by NWA A? Solvable in polynomial
- 22. MSO-based Characterization Monadic Second Order Logic of Nested Words First order variables: x,y,z; Set variables: X,Y,Z…
- 23. Application: Software Analysis A program P with stack-based control is modeled by a set L of
- 24. Writing Program Specifications Intuition: Keeping track of context is easy; just skip using a summary edge
- 25. Temporal Logic of Nested Time: CaRet Global paths, Local paths, Caller paths Three versions of every
- 26. So far: Nested words have appealing theoretical properties with possible applications Common framework: linear encoding using
- 27. Linear Encoding of Nested Words Nested word over Σ is encoded as a word over tagged
- 28. Encoding Ordered Trees/Hedges b> a> An ordered tree/hedge over Σ is encoded as a word over
- 29. Relating to Word languages a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
- 30. Deterministic Context-free Languages over Regular Languages over Regular Languages of trees/hedges over Σ = Balanced grammars
- 31. Comparing NWAs with Tree Automata Over hedge words same expressiveness Same complexity of analysis problems (e.g.
- 32. Flat Automata Flat NWAs: no information flows across summary edges Syntactic special case: if δc(q,a)=(p,r) then
- 33. Bottom-up Automata Bottom-up NWAs: Processing of a nested subword does not depend on the current state
- 34. Expressing Linear Queries with Tree Automata Tree Automata can naturally express constraints on sequence of labels
- 35. Top-down Automata Only information flowing across a return edge: whether inside subword is accepted or not
- 36. Processing Paths For a language L of words, let path(L) be language of unary trees such
- 37. Pushdown Automata over Nested Words Nondeterministic joinless transition relation Finite-state control augmented with stack Expressiveness: Contains
- 38. Related Work Restricted context-free languages Parantheses languages, Dyck languages Input-driven languages Logical characterization of context-free languages
- 39. Conclusions Nested words for modeling data with linear + hierarchical structure Words are special cases; ordered
- 41. Скачать презентацию