Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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]] 
 + 
 +===== 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)]] 
  
 
sav08/lecture22.txt · Last modified: 2008/05/14 20:21 by vkuncak
 
© EPFL 2018 - Legal notice