Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:lecture22 [2008/05/08 11:59] vkuncak removed |
sav08:lecture22 [2008/05/14 20:21] (current) vkuncak created |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Examples of Abstract Interpretation ====== | + | ====== Deciding Presburger Arithmetic Using Automata ====== |
- | Examples: | + | [[Logic and Automata Introduction]] |
- | * [[Conjunctions of Predicates]] - example of finite lattice. two different orders | + | |
- | * [[Constant Propagation]] - infinite lattice with finite ascending chain property | + | |
- | * Bitwidth analysis | + | |
- | * Interval analysis | + | |
- | * Polyhedra - linear inequalities | + | |
- | * [[Converging in Infinite-Height Lattice]] - dropping conjuncts | + | |
- | [[Designing Abstract Domains]] | + | ===== Review ===== |
- | [[:sav07_lecture_7|Approximation Expressed Using Formulas]] | + | [[:Strings and languages]] |
+ | [[:Finite state machine]] | ||
- | ===== Predicate Abstraction and Blast Tool: Guest Lecture by Prof. Dirk Beyer ===== | + | [[:Determinization of finite state machine]] |
- | ===== References ===== | + | [[:Finite state machine with epsilon transitions]] |
- | * [[http://www.di.ens.fr/~cousot/COUSOTtalks/VMCAI05_TOOLS.shtml|A Tutorial on Abstract Interpretation by Patrick Cousot]], also {{sav08:cousot-vmcai05industrialday_1-1.pdf|local pdf copy}} | + | [[:Closure properties of finite state machines]] |
- | * [[Calculus of Computation Textbook]] Chapter 12, including Section 12.4 | + | |
- | * [[http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml|Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints]] (original abstract interpretation paper) | + | [[:Regular expression]] |
- | * [[http://www.brics.dk/~mis/static.pdf|Lecture notes on static analysis by Michael Schwartzbach]] (sections 4,5,6,7 in particular) | + | |
- | * [[http://www.math.tau.ac.il/~sagiv/courses/pa/notes.ps|Notes on program analysis]], by Alex Aiken | + | [[:Equivalence of finite state machine and regular expression languages]] |
- | * [[http://web.mit.edu/16.399/|Patrick Cousot's MIT Class]] | + | |
- | * [[http://www.cs.tau.ac.il/~msagiv/courses/pa05.html|PA 2005]] at Tel-Aviv University | + | ===== Recognizing Relations using Automata ===== |
- | * [[:sav07_lecture_11|Lecture on ASTREE]] | + | |
+ | [[:Regular expressions for automata with parallel inputs]] | ||
+ | |||
+ | [[:Using automata to decide Presburger arithmetic]] | ||
+ | |||
+ | [[:MSOL over strings]] | ||
+ | |||
+ | ===== Additional material ===== | ||
+ | |||
+ | Automata and languages: | ||
+ | * [[http://www-math.mit.edu/~sipser/book.html|Introduction to the Theory of Computation]] | ||
+ | * [[http://infolab.stanford.edu/~ullman/ialc.html|Introduction to Automata Theory, Languages, and Computation]] | ||
+ | |||
+ | MSOL: | ||
+ | * [[http://www.brics.dk/mona/|The MONA Project]] | ||
+ | |||
+ | More | ||
+ | * [[http://www.montefiore.ulg.ac.be/~boigelot/research/lash/|LASH Toolset]] | ||
+ | * [[http://www.lsv.ens-cachan.fr/~treinen/publi/constraints.ps.gz|Constraint solving and decision problems of first-order theories of concrete domains]], by Ralf Treinen | ||
+ | |||
+ | Verification of linked structures using automata or MSOL: | ||
+ | * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL06FieldConstraintAnalysis.html|Field constraint analysis]] | ||
+ | * [[http://www.brics.dk/PALE|Pointer Assertion Logic Engine]] | ||
+ | |||
+ | MSOL: | ||
+ | * [[http://www.grappa.univ-lille3.fr/tata/|Tree Automata Techniques and Applications (Tata book)]] | ||
+ | * [[http://www.brics.dk/mona/|The MONA Project]] | ||
+ | * [[http://www.irisa.fr/lande/genet/timbuk/|Timbook for Reachability Analysis and Tree Automata Calculations]] | ||
+ | |||
+ | Last year: | ||
+ | * [[:sav07_lecture_15]] | ||
+ | * [[:sav07_lecture_16]] | ||
+ | * [[:sav07_lecture_17]] | ||
- | Conferences: | ||
- | * [[http://www.informatik.uni-trier.de/~ley/db/conf/popl/index.html|Symposium on Principles of Programming Languages (POPL)]] | ||
- | * [[http://www.informatik.uni-trier.de/~ley/db/conf/pldi/index.html|SIGPLAN Conference on Programming Language Design and Implementation (PLDI)]] | ||
- | * [[http://www.informatik.uni-trier.de/~ley/db/conf/sas/|Static Analysis Symposium (SAS)]] | ||
- | * [[http://www.informatik.uni-trier.de/~ley/db/conf/vmcai/index.html|Verification, Model Checking and Abstract Interpretation (VMCAI)]] | ||