There is, however, a more general argument against reverence, whether for the Greeks or for anyone else. In studying a philosopher, the right attitude is neither reverence nor contempt, but first a kind of hypothetical sympathy, until it is possible to know what it feels like to believe in his theories, and only then a revival of the critical attitude, which should resemble, as far as possible, the state of mind of a person abandoning opinions which he has hitherto held. Contempt interferes with the first part of this process, and reverence with the second. Two things are to be remembered: that a man whose opinions and theories are worth studying may be presumed to have had some intelligence, but that no man is likely to have arrived at complete and final truth on any subject whatever. When an intelligent man expresses a view which seems to us obviously absurd, we should not attempt to prove that it is somehow true, but we should try to understand how it ever came to seem true. This exercise of historical and psychological imagination at once enlarges the scope of our thinking, and helps us to realize how foolish many of our own cherished prejudices will seem to an age which has a different temper of mind.
-- Page 39, Chapter 4, "A History of Western Philosophy" by Bertrand Russell
Tuesday, April 22, 2014
Saturday, April 19, 2014
Weekly Reading: Cosmology in Heraclitus, Parmenides, and Empedocles
On reading the book "A History of Western Philosophy", I'm at the part of ancient Greek philosophers.
Heraclitus ( Ἡράκλειτος) talks about the world in an perspective that everything is changing all the time. He viewed strife as a power of changing, not necessarily an evil deed, and thus war "is the father of all and king of all". To think about the construction of the cosmos, he believes that fire is the primordial element, out of which everything comes into being.
However, Parmenides (Παρμενίδης) stressed that the cosmos is in essential perpetual with no change. He takes the words in human languages as such an instance, saying that the name of a person is always associated with him, whenever before, during or after his life. However, Bertrand Russell, the author of the book, attacked this theory by proposing that for those who never meet the person, what comes to their mind is their illusion or image based on how they read or hear about him, which is conspicuously not identical to what he really is in the minds of his friends. But after all, Parmenides' theory is partially true in the sense of quantum physics, since scientists can always find the unchangeable part of any object in a smaller and smaller scale, i.e. from Atom to Proton to Hadron. Although this process has not reached its final goal of find the unchangeable kernel, it's widely believed that the constituent of such a property with respect to chemical reactions must exist.
Finally, Empedocles ( Ἐμπεδοκλῆς) combines the theory of cosmology of all the previous philosophers together as a concession. In his theory, the cosmos is made from four elements -- fire, water, air and earth. There are also two powers, Love and Strife, performing the construction and destruction of objects respectively. The two kind of reactions happens in order and consist an infinite cycle. Thus all compound things are temporary and destructible, while only those four elements remains forever. Due to Empedocles, there is a golden age when the power of Love totally supersedes that of Strife. Then people at this era would worship only the Cyprian Aphrodite, who is the Goddess of Love.
Heraclitus ( Ἡράκλειτος) talks about the world in an perspective that everything is changing all the time. He viewed strife as a power of changing, not necessarily an evil deed, and thus war "is the father of all and king of all". To think about the construction of the cosmos, he believes that fire is the primordial element, out of which everything comes into being.
However, Parmenides (Παρμενίδης) stressed that the cosmos is in essential perpetual with no change. He takes the words in human languages as such an instance, saying that the name of a person is always associated with him, whenever before, during or after his life. However, Bertrand Russell, the author of the book, attacked this theory by proposing that for those who never meet the person, what comes to their mind is their illusion or image based on how they read or hear about him, which is conspicuously not identical to what he really is in the minds of his friends. But after all, Parmenides' theory is partially true in the sense of quantum physics, since scientists can always find the unchangeable part of any object in a smaller and smaller scale, i.e. from Atom to Proton to Hadron. Although this process has not reached its final goal of find the unchangeable kernel, it's widely believed that the constituent of such a property with respect to chemical reactions must exist.
Finally, Empedocles ( Ἐμπεδοκλῆς) combines the theory of cosmology of all the previous philosophers together as a concession. In his theory, the cosmos is made from four elements -- fire, water, air and earth. There are also two powers, Love and Strife, performing the construction and destruction of objects respectively. The two kind of reactions happens in order and consist an infinite cycle. Thus all compound things are temporary and destructible, while only those four elements remains forever. Due to Empedocles, there is a golden age when the power of Love totally supersedes that of Strife. Then people at this era would worship only the Cyprian Aphrodite, who is the Goddess of Love.
Weekly Reading: Term Rewriting, Formal Logic System
My current reading goal is to review and finish the book "Term Rewriting And All That" by Franz Baader and Tobias Nipkow as soon as possible. This week, I covered the part of termination, confluence and completion. The first two combined together is used to judge if a term rewriting system (TRS) is convergent, which is regarded as a well-defined TRS, while a completion procedure is to compute a convergent TRS from a given set of identities by applying a number of inference rules if there exists one.
In general, the decision problem on terminating and confluence given an arbitrary order is undecidable. So in the chapter of termination, the book introduced a concept called Reduction Order, which satisfies the properties of well-founded, compatible with Σ-operations, and closed under substitutions, and proposed some widely-used orders as the interpretation methods which are consistent with the reduction order. Note that the property of well-founded can be replaced by that of Simplification Order, which is much easier to show the termination of the given order. There are three classical orders introduced here: polynomial order, lexicographic path order, and the famous Knuth-Bendix order. Polynomial order requires that all function symbols in Σ under interpretation must be monotone in order to satisfy the third property of reduction order. It's easy to define, but can only show the termination of those TRS's that cannot be bound by primitive recursion (like Ackerman function). Both LPO and KBO can address this problem, and the decision procedure using either of them is decidable, while it's an NP-complete problem. LPO and KBO are both recursively defined, but KBO applies an extra weight function and the occurrence of variables in terms for the comparison.
For the issue of confluence, it's closely related to critical pairs under the set of rules R. If TRS is terminating, then by Newman's Lemma, it's confluent iff it's locally confluent. Thus, in this case, if we can show that all critical pairs given E and R are joinable, then TRS is confluent. More generally, for a not necessarily terminating TRS, we have to show that it's left-linear (i.e. no variable occurs twice in l of any rule l -> r in R) and parallel closed over all critical pairs, which is Corollary 6.4.9 from the Parallel Closure Theorem (Theorem 6.4.8).
In the chapter of completion procedures, a basic completion procedure is introduced, which is correct as a semidecision procedure and quite inefficient. Then an improved completion procedure was defined by applying a set of inference rules, like DEDUCE, ORIENT, DELETE, SIMPLIFY-INDENTIFY, R-SIMPLIFY-RULE, L-SIMPLIFY-RULE, many of which are quite similar to those in the decision procedure of equational unification problems. The main idea is to add those identities in E and critical pairs computed from E and R into R, then simplifying them under R and forming all resulted rules in R satisfying the reduction order >. This procedure is iterative until E becomes empty, which means that all critical pairs are joinable and the procedure terminates SUCESSFULLY. Otherwise, if E is never empty, which means that there exists some un-joinable critical pair, or some (s, t) is not comparable, which means that neither s -> t nor t -> s satisfies the reduction order >, then the procedure terminates with FAILURE. A tool named proof order is used to prove the correctness of the improved completion procedure, which is also a fair completion procedure. After that, a famous Huet's completion procedure was introduced, which works in a similar way, is correct but not fair.
In general, the decision problem on terminating and confluence given an arbitrary order is undecidable. So in the chapter of termination, the book introduced a concept called Reduction Order, which satisfies the properties of well-founded, compatible with Σ-operations, and closed under substitutions, and proposed some widely-used orders as the interpretation methods which are consistent with the reduction order. Note that the property of well-founded can be replaced by that of Simplification Order, which is much easier to show the termination of the given order. There are three classical orders introduced here: polynomial order, lexicographic path order, and the famous Knuth-Bendix order. Polynomial order requires that all function symbols in Σ under interpretation must be monotone in order to satisfy the third property of reduction order. It's easy to define, but can only show the termination of those TRS's that cannot be bound by primitive recursion (like Ackerman function). Both LPO and KBO can address this problem, and the decision procedure using either of them is decidable, while it's an NP-complete problem. LPO and KBO are both recursively defined, but KBO applies an extra weight function and the occurrence of variables in terms for the comparison.
For the issue of confluence, it's closely related to critical pairs under the set of rules R. If TRS is terminating, then by Newman's Lemma, it's confluent iff it's locally confluent. Thus, in this case, if we can show that all critical pairs given E and R are joinable, then TRS is confluent. More generally, for a not necessarily terminating TRS, we have to show that it's left-linear (i.e. no variable occurs twice in l of any rule l -> r in R) and parallel closed over all critical pairs, which is Corollary 6.4.9 from the Parallel Closure Theorem (Theorem 6.4.8).
In the chapter of completion procedures, a basic completion procedure is introduced, which is correct as a semidecision procedure and quite inefficient. Then an improved completion procedure was defined by applying a set of inference rules, like DEDUCE, ORIENT, DELETE, SIMPLIFY-INDENTIFY, R-SIMPLIFY-RULE, L-SIMPLIFY-RULE, many of which are quite similar to those in the decision procedure of equational unification problems. The main idea is to add those identities in E and critical pairs computed from E and R into R, then simplifying them under R and forming all resulted rules in R satisfying the reduction order >. This procedure is iterative until E becomes empty, which means that all critical pairs are joinable and the procedure terminates SUCESSFULLY. Otherwise, if E is never empty, which means that there exists some un-joinable critical pair, or some (s, t) is not comparable, which means that neither s -> t nor t -> s satisfies the reduction order >, then the procedure terminates with FAILURE. A tool named proof order is used to prove the correctness of the improved completion procedure, which is also a fair completion procedure. After that, a famous Huet's completion procedure was introduced, which works in a similar way, is correct but not fair.
Tuesday, January 28, 2014
Minimal Comprehensive Groebner Bases
Goals:
1. Decide if the transitivity of non-essentiality is necessary;
2. Prove the generated Groebner basis is minimal, faithful and comprehensive;
3. Extend it to general comprehensive Groebner systems;
4. Try to define the Canonical Minimal Comprehensive Groebner basis.
Done:
1. We do need the transitivity of non-essentiality to guarantee the comprehensiveness of the generated Groebner basis;
2. Faithfulness and comprehensiveness are trivial to prove; Minimality is able to be proved;
3. Extension: replace "LPP_X is x" by "LPP_X divides x".
1. Decide if the transitivity of non-essentiality is necessary;
2. Prove the generated Groebner basis is minimal, faithful and comprehensive;
3. Extend it to general comprehensive Groebner systems;
4. Try to define the Canonical Minimal Comprehensive Groebner basis.
Done:
1. We do need the transitivity of non-essentiality to guarantee the comprehensiveness of the generated Groebner basis;
2. Faithfulness and comprehensiveness are trivial to prove; Minimality is able to be proved;
3. Extension: replace "LPP_X is x" by "LPP_X divides x".
Saturday, September 28, 2013
![[ Celebrate 30 years of GNU! ]](https://static.fsf.org/nosvn/misc/GNU_30th_badge.png){kind=icon}
Thursday, June 13, 2013
Review on Decision Procedure on Linear Arithmetic
This is about the review of topics that De Moura covered in SSFT2013.
1. Here is my implementation on Sturm's Theorem in Univariate Polynomial case:
1. Here is my implementation on Sturm's Theorem in Univariate Polynomial case:
The language I choose is Haskell.
2. Here is my proof of Sturm's Theorem:
Friday, May 24, 2013
Day V: Summer School on Formal Techniques
Putting Numerical Abstract Domain to Work: A Study of Array-Bound Checking for C Programs (by Arnaud J. Venet, slides):
1. Review of Abstract Interpretation using Polyhedra abstract domain;
My Question: what is the difference between polyhedron intersecting and the narrowing operator?
2. Gauge domain: modified interval domain to help scale the operations within loops (specifically, widening and convex-hull operations);
3. He uses New Polka library and XXX's fixed-point algorithm:
a. Issue: Program Crashed for widening operations: too many dimensions (i.e. program variables). Solution: eliminate unimportant variables;
b. Issue: still crashed. Solution: directly propagate unchanged constraints rather than calculate again and again. Solved.
Verified Programming in VCC (by Ernie Cohen, slides):
1. VCC is heavily based on ghost data, which costs zero executing time;
2. There is no invariant check when VCC applies the owning operation on objects;
3. Verification on concurrent programs: lock-free; lock is container.
Program Verification and Synthesis as Horn-like Constraint Solving (by Andrey Rybalchenko):
1. verification using temporal logic (especially CTL);
2. Doing abstract interpretation using horn-like constraint solving strategy (using Interpolant).
Lab (by Ernie Cohen):
1. Write you own binary search program in C;
2. Use VCC (either in Visual Studio or with online version (http://rise4fun.com/Vcc)) to verify the code;
3. VCC code you need to write: function-level (pre-condition using requires; post-condition using ensures; terminating using decreases), loop-level (invariant specification).
4. My original code has 27 bugs, all of which are related to overflow. After fixing it for one hour, I get it bug-free under VCC verification.
1. Review of Abstract Interpretation using Polyhedra abstract domain;
My Question: what is the difference between polyhedron intersecting and the narrowing operator?
2. Gauge domain: modified interval domain to help scale the operations within loops (specifically, widening and convex-hull operations);
3. He uses New Polka library and XXX's fixed-point algorithm:
a. Issue: Program Crashed for widening operations: too many dimensions (i.e. program variables). Solution: eliminate unimportant variables;
b. Issue: still crashed. Solution: directly propagate unchanged constraints rather than calculate again and again. Solved.
Verified Programming in VCC (by Ernie Cohen, slides):
1. VCC is heavily based on ghost data, which costs zero executing time;
2. There is no invariant check when VCC applies the owning operation on objects;
3. Verification on concurrent programs: lock-free; lock is container.
Program Verification and Synthesis as Horn-like Constraint Solving (by Andrey Rybalchenko):
1. verification using temporal logic (especially CTL);
2. Doing abstract interpretation using horn-like constraint solving strategy (using Interpolant).
Lab (by Ernie Cohen):
1. Write you own binary search program in C;
2. Use VCC (either in Visual Studio or with online version (http://rise4fun.com/Vcc)) to verify the code;
3. VCC code you need to write: function-level (pre-condition using requires; post-condition using ensures; terminating using decreases), loop-level (invariant specification).
4. My original code has 27 bugs, all of which are related to overflow. After fixing it for one hour, I get it bug-free under VCC verification.
Day IV: Summer School on Formal Techniques
Automatic Deduction Applied: Program Synthesis and Question Answering (by Richard Waldinger, slides):
1. Program Synthesis: extracting programs from proofs;
2. History on Automatic Deduction:
a. McCarthy's advice taker;
b. Slagle's deducum;
c. Amphion system used in planetary astronomy;
3. Question in natural language and based on deduction rather than statistical search (on which IBM Watson applies)
Program Verification and Synthesis as Horn-like Constraint Solving (by Andrey Rybalchenko, slides):
1. Summarization vs. Invariance :
a. For the case with procedure invocations;
b. Owicki / Gries Proof Rule;
c. Rely / Guarantee Proof Rule;
2. Type System in Programming Languages:
a. Well-typed programs can never go wrong;
b. Type Tree vs. Refinement Tree (PVS-friendly specification).
Exercise proposed by Shankar: use PVS to write the specification for 2b, and submit to him.
Static and Dynamic Analysis of Concurrent Programs (by Aarti Gupta, slides):
1. Context Bounded Analysis using Sequentialization;
2. Dynamic Analysis:
a. Preemptive Context Bounding;
b. Trace Based Verification;
c. Predicative Analysis;
3. Garbage Collection in C++11;
4. SMT-Based symbolic search:
a. based on Concurrent Static Single Assignment (CSSA) encoding;
b. Modular Analysis.
Lab (by Andrey Rybalchenko):
ARMC: http://www7.in.tum.de/~rybal/
My Comment: it can be easily screwed up writing a much longer horn-like constraint verification code, even for just 20 lines of source code with inter-procedure calls. Is there any related work or possibility to generate these constraints automatically?
Prof. from CAS commented: Horn Clause was under warm studying and researching during 1980s. Then people came to obstacles and put it on the shelf for a long time. Recently it returns to alive. Deepak has done a bunch of elegant stuffs, including Ideal Generation, etc.
PPT Karaoke for fun tonight.
1. Program Synthesis: extracting programs from proofs;
2. History on Automatic Deduction:
a. McCarthy's advice taker;
b. Slagle's deducum;
c. Amphion system used in planetary astronomy;
3. Question in natural language and based on deduction rather than statistical search (on which IBM Watson applies)
Program Verification and Synthesis as Horn-like Constraint Solving (by Andrey Rybalchenko, slides):
1. Summarization vs. Invariance :
a. For the case with procedure invocations;
b. Owicki / Gries Proof Rule;
c. Rely / Guarantee Proof Rule;
2. Type System in Programming Languages:
a. Well-typed programs can never go wrong;
b. Type Tree vs. Refinement Tree (PVS-friendly specification).
Exercise proposed by Shankar: use PVS to write the specification for 2b, and submit to him.
Static and Dynamic Analysis of Concurrent Programs (by Aarti Gupta, slides):
1. Context Bounded Analysis using Sequentialization;
2. Dynamic Analysis:
a. Preemptive Context Bounding;
b. Trace Based Verification;
c. Predicative Analysis;
3. Garbage Collection in C++11;
4. SMT-Based symbolic search:
a. based on Concurrent Static Single Assignment (CSSA) encoding;
b. Modular Analysis.
Lab (by Andrey Rybalchenko):
ARMC: http://www7.in.tum.de/~rybal/
My Comment: it can be easily screwed up writing a much longer horn-like constraint verification code, even for just 20 lines of source code with inter-procedure calls. Is there any related work or possibility to generate these constraints automatically?
Prof. from CAS commented: Horn Clause was under warm studying and researching during 1980s. Then people came to obstacles and put it on the shelf for a long time. Recently it returns to alive. Deepak has done a bunch of elegant stuffs, including Ideal Generation, etc.
PPT Karaoke for fun tonight.
Day III: Summer School on Formal Techniques
Speaking Logic (by N. Shankar, slides):
1. Unification;
2. Resolution (Negation -> Prenexation -> Skolemization -> Distribution and Isolation -> Universal Quantifier Elimination -> Q.E.D.)
Static and Dynamic Verification on Concurrent Programs (by Aarti Gupta, slides)
Verified Programming in VCC (by Ernie Cohen, slides):
1. "Programming Pearls" Chapter -- How to verify Binary Search;
2. Separation Logic;
3. Positive Polarity;
4. Linearly Isolability.
Lab (Aarti Gupta, instructions):
Active Testing: CalFuzzer http://sp09.pbworks.com/w/page/6721195/FrontPage
http://srl.cs.berkeley.edu/~ksen/calfuzzer/
Homework: http://sp09.pbworks.com/w/page/6721216/RaceFuzzer%20Homework
Student Presentation:
1. Anvesh Komuravelli, "Abstraction in SMT-based Model Checking".
a. Predicate Abstraction;
b. SLAM, BLAST, SDV; IMPACT, UFO;
c. Over-approximation Driven; Under-approximation Driven;
d. His approach is a little bit like widening operator in Abstract Interpretation. The difference is that it can approximate with respect to the counterexample, which is the feature of Model Checking (Dynamic Analysis);
e. Using UZ SMT Solver.
2. Sridhar Duggirala, "Annotations for Verification of Dynamical and Hybrid Systems".
1. Unification;
2. Resolution (Negation -> Prenexation -> Skolemization -> Distribution and Isolation -> Universal Quantifier Elimination -> Q.E.D.)
Static and Dynamic Verification on Concurrent Programs (by Aarti Gupta, slides)
Verified Programming in VCC (by Ernie Cohen, slides):
1. "Programming Pearls" Chapter -- How to verify Binary Search;
2. Separation Logic;
3. Positive Polarity;
4. Linearly Isolability.
Lab (Aarti Gupta, instructions):
Active Testing: CalFuzzer http://sp09.pbworks.com/w/page/6721195/FrontPage
http://srl.cs.berkeley.edu/~ksen/calfuzzer/
Homework: http://sp09.pbworks.com/w/page/6721216/RaceFuzzer%20Homework
Student Presentation:
1. Anvesh Komuravelli, "Abstraction in SMT-based Model Checking".
a. Predicate Abstraction;
b. SLAM, BLAST, SDV; IMPACT, UFO;
c. Over-approximation Driven; Under-approximation Driven;
d. His approach is a little bit like widening operator in Abstract Interpretation. The difference is that it can approximate with respect to the counterexample, which is the feature of Model Checking (Dynamic Analysis);
e. Using UZ SMT Solver.
2. Sridhar Duggirala, "Annotations for Verification of Dynamical and Hybrid Systems".
Tuesday, May 21, 2013
Day II: Summer School on Formal Techniques
Speaking Logic (by N. Shankar, slides):
1. Sequant Calculus (contd.) -- Cut rule;
2. Peirce's Formula: $$ ((p \Rightarrow q) \Rightarrow p) \Rightarrow p $$;
3. Concepts of derivied rule and admissible rule;
4. How to prove $$\exists x. (p(x) \Rightarrow \forall y. p(y))$$;
5. Prenex Normal Form.
PVS (by C. Munoz, lecture 2):
1. Proof by Induction (proving strategy; can go around by making use of data type specifications);
2. Recursion specification.
Decision Methods on Arithmetic (by L. de Moura, slides and materials):
1. Multivariate case: recursive representation of multivariate polynomials (with some order on variables);
2. Sturm Tree -- Case analysis based on Sturm's sequence and Tarski query;
3. Leonardo's method is built in the Z3 theorem prover.
Discussion with Leonardo de Moura:
For the proof of Sturm's Theorem, most proofs only consider the case that \( h_m\) is a constant polynomial. However, though rarely, there can be the case that \( h_m \) is a non-constant polynomial. In the latter case, we need to divide each polynomial in the Sturm Sequence by \( h_m \) and show that the resulting sequence \( \hat{h_i} \) is still a sequence of polynomials. Further, to prove that the only point that decreases the total sign change number is the real root of \( f \), we need to discuss by case analysis on the sign of \( \hat{h_1} \) using the property of even and odd functions.
PVS Lab Session (instructions, homework):
1. PVS examples in PVSLab directory provided by Munoz;
2. PVS 6.0 with NASALib installed (http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/);
3. discussion with students: the online textbook named "Software Foundations" by Benjamin C. Pierce (http://www.cis.upenn.edu/~bcpierce/sf/).
Student Presentation:
1. Martin Schäf, Joogie: Infeasible Code Detection on Java bytecode.
a. https://code.google.com/p/joogie/ ;
b. Uses Soot (Java Optimization Framework), Wala (static analyzer on Java and JavaScript), and Z3 Theorem Prover;
c. Based on Weakest Liberal Precondition rather than Weakest Precondition, i.e. only consider partial correctness;
d. Can outperform the static code checker in Eclipse;
e. Can have issues on false positive cases;
f. He is a postdoc at United Nations University -- International Institute for Software Technology at Macau, China.
2. Etienne Kneuss, "Leon Verification and Synthesis":
a. Using Scala;
b. Writing specifications on data structures and functions, then the system will search in the library to synthesize the reified code;
c. Purely functional style syntax defined by them;
d. Issues: due to the functional syntax, many real-world data structures like Doubly-Linked List cannot be specified; besides, High-order is not possible to be combined in.
1. Sequant Calculus (contd.) -- Cut rule;
2. Peirce's Formula: $$ ((p \Rightarrow q) \Rightarrow p) \Rightarrow p $$;
3. Concepts of derivied rule and admissible rule;
4. How to prove $$\exists x. (p(x) \Rightarrow \forall y. p(y))$$;
5. Prenex Normal Form.
PVS (by C. Munoz, lecture 2):
1. Proof by Induction (proving strategy; can go around by making use of data type specifications);
2. Recursion specification.
Decision Methods on Arithmetic (by L. de Moura, slides and materials):
1. Multivariate case: recursive representation of multivariate polynomials (with some order on variables);
2. Sturm Tree -- Case analysis based on Sturm's sequence and Tarski query;
3. Leonardo's method is built in the Z3 theorem prover.
Discussion with Leonardo de Moura:
For the proof of Sturm's Theorem, most proofs only consider the case that \( h_m\) is a constant polynomial. However, though rarely, there can be the case that \( h_m \) is a non-constant polynomial. In the latter case, we need to divide each polynomial in the Sturm Sequence by \( h_m \) and show that the resulting sequence \( \hat{h_i} \) is still a sequence of polynomials. Further, to prove that the only point that decreases the total sign change number is the real root of \( f \), we need to discuss by case analysis on the sign of \( \hat{h_1} \) using the property of even and odd functions.
PVS Lab Session (instructions, homework):
1. PVS examples in PVSLab directory provided by Munoz;
2. PVS 6.0 with NASALib installed (http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/);
3. discussion with students: the online textbook named "Software Foundations" by Benjamin C. Pierce (http://www.cis.upenn.edu/~bcpierce/sf/).
Student Presentation:
1. Martin Schäf, Joogie: Infeasible Code Detection on Java bytecode.
a. https://code.google.com/p/joogie/ ;
b. Uses Soot (Java Optimization Framework), Wala (static analyzer on Java and JavaScript), and Z3 Theorem Prover;
c. Based on Weakest Liberal Precondition rather than Weakest Precondition, i.e. only consider partial correctness;
d. Can outperform the static code checker in Eclipse;
e. Can have issues on false positive cases;
f. He is a postdoc at United Nations University -- International Institute for Software Technology at Macau, China.
2. Etienne Kneuss, "Leon Verification and Synthesis":
a. Using Scala;
b. Writing specifications on data structures and functions, then the system will search in the library to synthesize the reified code;
c. Purely functional style syntax defined by them;
d. Issues: due to the functional syntax, many real-world data structures like Doubly-Linked List cannot be specified; besides, High-order is not possible to be combined in.
Monday, May 20, 2013
Day I: SRI Summer School on Formal Methods
Speaking Logic (by Natarajan Shankar, slides here):
1. How logic formalization can be used to address ruddles;
2. Couturant, "Algebra of Logic";
3. Substitution Lemma in propositional logic;
4. Sequant Calculus.
PVS (by Cesar Munoz, lecture 0, lecture 1):
1. TCAS alerting logic;
Decision Methods for Arithmetic (by Leonardo de Moura, slides and materials):
1. Fourier-Motzkin Elimination Method;
2. Sturm's Sequence;
3. Sturm-Tarski Theorem;
4. Tarski Query;
5. Formal statement in univariate case.
Lab Session on Arithmetic Decision Methods (assignment):
1. Tutorials on Z3: http://z3.codeplex.com/documentation ;
http://stackoverflow.com/users/2327608/juan-ospina?tab=questions&sort=activity ;
2. Prove Sturm's Theorem;
3. Implement polynomial operations (+, *, /, etc.); Implement Sturm Sequence generating method; implement Tarski Query. Note: All only in univariate cases.
Student Talks:
1. Konstantin Korovin, Nestan Tsiskaridze, and Andrei Voronkov, Conflict Resolution:
a. Used for solving linear (in)equality systems [satisfiability] on integer, real and rational fields;
b. Based on Fourier-Motzkin Elimination;
c. Main Method: 1) Assignment Refinement; 2) Constraint Generation based on Conflict;
d. Drastically reduce the number of redundant constraints generated, i.e. better than Fourier-Motzkin Elimination, comparable to Simplex Method;
e. Heuristics on choosing conflicting constraints: mini-lower, max-upper; or longest geometric distance;
f. Easy to switch to incremental version;
g. Suitable for combining with SMT solver;
h. Future Work: combine with SMT solver; implement a better preprocessor.
2. Gidon Ernst, et al. "A Formal Model of a Virtual Filesystem Switch":
a. https://swt.informatik.uni-augsburg.de/swt/projects/ ;
b. Implement a simulation on the very top level, the core part (i.e. the part dealing with flash disks) is still under developing;
c. Specification written in PVS, implementation in Scala.
1. How logic formalization can be used to address ruddles;
2. Couturant, "Algebra of Logic";
3. Substitution Lemma in propositional logic;
4. Sequant Calculus.
PVS (by Cesar Munoz, lecture 0, lecture 1):
1. TCAS alerting logic;
Decision Methods for Arithmetic (by Leonardo de Moura, slides and materials):
1. Fourier-Motzkin Elimination Method;
2. Sturm's Sequence;
3. Sturm-Tarski Theorem;
4. Tarski Query;
5. Formal statement in univariate case.
Lab Session on Arithmetic Decision Methods (assignment):
1. Tutorials on Z3: http://z3.codeplex.com/documentation ;
http://stackoverflow.com/users/2327608/juan-ospina?tab=questions&sort=activity ;
2. Prove Sturm's Theorem;
3. Implement polynomial operations (+, *, /, etc.); Implement Sturm Sequence generating method; implement Tarski Query. Note: All only in univariate cases.
Student Talks:
1. Konstantin Korovin, Nestan Tsiskaridze, and Andrei Voronkov, Conflict Resolution:
a. Used for solving linear (in)equality systems [satisfiability] on integer, real and rational fields;
b. Based on Fourier-Motzkin Elimination;
c. Main Method: 1) Assignment Refinement; 2) Constraint Generation based on Conflict;
d. Drastically reduce the number of redundant constraints generated, i.e. better than Fourier-Motzkin Elimination, comparable to Simplex Method;
e. Heuristics on choosing conflicting constraints: mini-lower, max-upper; or longest geometric distance;
f. Easy to switch to incremental version;
g. Suitable for combining with SMT solver;
h. Future Work: combine with SMT solver; implement a better preprocessor.
2. Gidon Ernst, et al. "A Formal Model of a Virtual Filesystem Switch":
a. https://swt.informatik.uni-augsburg.de/swt/projects/ ;
b. Implement a simulation on the very top level, the core part (i.e. the part dealing with flash disks) is still under developing;
c. Specification written in PVS, implementation in Scala.
Monday, April 8, 2013
AIHaskell: Final Project for CS 591
Part I. Front-end
I choose Parsec library to help implement the front-end. A sample of its usage can be found here:
http://book.realworldhaskell.org/read/using-parsec.html
I choose Parsec library to help implement the front-end. A sample of its usage can be found here:
http://book.realworldhaskell.org/read/using-parsec.html
Wednesday, April 3, 2013
Dimension Analysis in multiple languages
http://meltumn.wordpress.com/2012/03/21/existing-approaches/
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)