Scaladays '15: Yoyak
Yoyak: Static data analysis
Author is a programming language theorist.
The result of abstract interpretation is inaccurate, but not incorrect. Roughly, but soundly execute the program.
- symbolic execution
- data flow analysis
- syntactic analysis
- model checking, abstract interpretatio, type system
- The analysis result should contain all possibilities which can happen in the runtime
- if the analysis uses an over-approximation, it is sound
- The analysis result should not contain any possibility which cannot happen at runtime
- Over-approximation semantics is a superset of
- program semantics is a superset of
- approximation semantics
Illustrating Semantics with several tiny languages called Javar.
Key Elements of Abstract Interpretation
- Galois Connection: pair of functions: abstraction and concretination function
- CPO: three constraints: there exists a partial order…Lattice of Interval Domain…
- Continuous function: a function is continuous when it reserves the upper bounds
Concrete and Abstract Semantics are connected with a Galois connection.
Yoyak enables to reuse components
- CFG data types: construction, optimizatoin visualization
- Graph algorithms
- Intermediate language data types
- common abstract domains
- comman abstract semantics
It’s perfect to be a framework: The theory of abstract interpretation guarantees soundness and termination of the analysis if a user supplies valid operators.
- Abstract Domain
- Fixed-point Computation (using a work-list algorithm)
- Built-in Standard Object Model