Friday, March 29, 2013
Thursday, March 28, 2013
Willing To See Real-World Formal Verification Tools
1. Why Project: http://why.lri.fr/
A general purpose Verification Condition Generator.
2. Pylint: http://www.logilab.org/857
Static Checker for Python programs.
3. Code Analyzer for Visual Studio 2012
A general purpose Verification Condition Generator.
2. Pylint: http://www.logilab.org/857
Static Checker for Python programs.
3. Code Analyzer for Visual Studio 2012
Wednesday, March 27, 2013
Question Regarding Groebner Basis
1. Can an ideal other than \( \{0\} \) be a finite set?
Answer: Yes. It's obvious to prove this conclusion.
2. What is monomial ideal?
Answer: Yes. It's obvious to prove this conclusion.
2. What is monomial ideal?
Saturday, March 23, 2013
Thursday, March 21, 2013
Improvement on Octogonal Method
In Deepak's method[1], when there is some constraint present at the verification condition (VC) generating position, the algorithm takes that constraint into consideration eagerly. This may result in a problem that the constraint might not be hit, like an infinite loop for instance. However, this constraint still enlarges the feasible domain of the octagon, which makes the generated VC weaker than the optimal one.
In order to address this problem, I make such a consideration lazy, which means that first apply the quantifier elimination method without constraints, and then compare the result with the constraints. Let U be the generated VC without constraints, and P be the set of constraints (it can be test conditions or conditionals), if we can achieve that
\[ U \rightarrow P. \]
Then we can know that P will not be hit, which implies that we can ignore these constraints and U is right the final VC we want.
The original method is in P. If we consider to apply the two possible branches, i.e. either involve the constraints or not, at each position, then the method will be exponential. With my improvement, it's still exponential in worst case. But if I'm able to reduce the process of add constraints P back into U if necessary in constant time, then we can achieve an algorithm which can generate stronger program invariants but still in polynomial time.
---------------------------------
References:
In order to address this problem, I make such a consideration lazy, which means that first apply the quantifier elimination method without constraints, and then compare the result with the constraints. Let U be the generated VC without constraints, and P be the set of constraints (it can be test conditions or conditionals), if we can achieve that
\[ U \rightarrow P. \]
Then we can know that P will not be hit, which implies that we can ignore these constraints and U is right the final VC we want.
The original method is in P. If we consider to apply the two possible branches, i.e. either involve the constraints or not, at each position, then the method will be exponential. With my improvement, it's still exponential in worst case. But if I'm able to reduce the process of add constraints P back into U if necessary in constant time, then we can achieve an algorithm which can generate stronger program invariants but still in polynomial time.
---------------------------------
References:
[1] Kapur, Deepak, et al. "Geometric Quantifier
Elimination Heuristics for Automatically Generating Octagonal and
Max-plus Invariants." Automated Reasoning and Mathematics. Springer Berlin Heidelberg, 2013. 189-228.
Tuesday, March 19, 2013
Thoughts on Program Verification
Inspiration:
I just finished the programming assignment in HW3 of Pattern Recognition class. There was a significant bug in my implementation on calculating the log-likelihood of the 1D Triangle Distribution, which resulted in the divergence of the parameter estimation.
So I'm wondering whether it's feasible to maintain the correctness even for such data science programs (or scientific simulation in another perspective). In this domain, the key challenge is that the reason for such divergence can be either a bug or the usage of a wrong statistics model. In the latter case, this result cannot be called an error of the programs.
Thus, my focus is on how to distinguish these two cases. If we are able to achieve this goal, it will be fairly convenient to debug the programs without doubting my choice of models, or on the other hand, I will only think about the pros and cons of the model itself with no concern about some potential bugs in the implementation.
I just finished the programming assignment in HW3 of Pattern Recognition class. There was a significant bug in my implementation on calculating the log-likelihood of the 1D Triangle Distribution, which resulted in the divergence of the parameter estimation.
So I'm wondering whether it's feasible to maintain the correctness even for such data science programs (or scientific simulation in another perspective). In this domain, the key challenge is that the reason for such divergence can be either a bug or the usage of a wrong statistics model. In the latter case, this result cannot be called an error of the programs.
Thus, my focus is on how to distinguish these two cases. If we are able to achieve this goal, it will be fairly convenient to debug the programs without doubting my choice of models, or on the other hand, I will only think about the pros and cons of the model itself with no concern about some potential bugs in the implementation.
Thoughts about Final Project in AdvHaskell
1. Implement abstract interpretation libraries in Haskell.
a. There is one binding for PPL library in Haskell:
http://www.ncc.up.pt/~pbv/research/ppl/ghc.html
b. I would like to see whether Libapron and the tropical polyhedron library can be possible to implemented in Haskell.
c. Importance: making Haskell eligible to do numerical static analysis for those compilers written in Haskell.
d. Compiler.HOOPL package
2. Coq extraction to Haskell.
a. A way to writing certified Haskell programs.
b. Whether it's possible to hack in the Extraction component in Coq.
c. comparing Haskell with Ocaml on coping with Coq Extraction.
d. Adam Chlipala talks about some concepts about Generic Programming concerning Coq and Haskell:
http://adam.chlipala.net/cpdt/html/Generic.html
which might be helpful.
e. This blog post talks about the Maybe monad emulated with properties proved in Coq:
http://pdp7.org/blog/?p=100
a. There is one binding for PPL library in Haskell:
http://www.ncc.up.pt/~pbv/research/ppl/ghc.html
b. I would like to see whether Libapron and the tropical polyhedron library can be possible to implemented in Haskell.
c. Importance: making Haskell eligible to do numerical static analysis for those compilers written in Haskell.
d. Compiler.HOOPL package
2. Coq extraction to Haskell.
a. A way to writing certified Haskell programs.
b. Whether it's possible to hack in the Extraction component in Coq.
c. comparing Haskell with Ocaml on coping with Coq Extraction.
d. Adam Chlipala talks about some concepts about Generic Programming concerning Coq and Haskell:
http://adam.chlipala.net/cpdt/html/Generic.html
which might be helpful.
e. This blog post talks about the Maybe monad emulated with properties proved in Coq:
http://pdp7.org/blog/?p=100
Subscribe to:
Posts (Atom)