• English only

# Differences

This shows you the differences between two versions of the page.

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 ToolGuest 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]]
+
+
+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)]]