Andrew E. Santosa's Web Page

Andrew E. Santosa
Research Fellow
Department of Computer Science
National University of Singapore
Computing 1 #02-15, Law Link, Singapore 117590
Republic of Singapore
Phone: +65-6516-2792, Mobile: +65-9482-7396
FAX: +65-6779-4580 (Attn: Andrew E. Santosa/RF)
E-Mail:

Brief Bio
Research
- Program Reasoning in CLP
- Declarative Concurrent Programming
- Selected Other Work
CLP(R) Bag of Tricks

Brief Bio

I am a professional researcher currently working on verification and analysis of programs (in general, anything that can be specified as recursive function or relation, both deterministic (sequential) or nondeterministic (concurrent), even with fairness requirement) by means of symbolic execution, especially using constraint logic programming (CLP). The basic approach is to invent novel non-heuristic techniques for search algorithms. The application area currently being targeted at encompasses the analysis of C source code, verification of real-time systems, and reasoning about omega automata (for which live sequence charts are instances). I am interested in literature, and as mentioned, I'm also doing a little bit of computer science.

My degrees are Doctor of Philosophy (Computer Science, National University of Singapore, 2008), Master of Engineering (Graduate School of Information Systems, University of Electro-Communications (UEC), 1999), Bachelor of Engineering (Computer Science and Information Mathematics, UEC, 1997).

Research

Program Reasoning in CLP

Here are some of the fruits of research projects led by Professor Joxan Jaffar and with the collaboration of Dr. Razvan Voicu in which I am a member. It resulted in my PhD thesis mentioned below.

J. Jaffar, A. E. Santosa, and R. Voicu. A Coinduction Rule for Entailment of Recursively-Defined Properties. In P. J. Stuckey, ed. Constraint Programming: Proceedings of the 14th International Conference on Principles and Practice of Constraint Programming, Sydney, Australia, 14-18 September 2008. pp. 493-508, LNCS 5202, Springer, 2008. DOI Slides PDF

Oct. 2008 First Automatic Prover! The above paper presents an idea of an automated inductive prover of recursive assertions based on search. The paper did not discuss an implementation, but as a proof of concept we have worked on a runnable prototype given here. The engine is the CLP(R) program datastruct.clpr. A sample problem is encoded in the file idempotent.clpr, which specifies the function idempotence proof problem presented in the paper.
For the constraint solving part, the above engine provides solving using congruence closure and simple arithmetic sanity test to check that there are no different numeric constants in the same equivalence class. This solver is enough for the proof of the above problem.
The constraint solving is implemented as a separate predicate constraintproof_aux, which is independent of the unfolding part, such that variety of solvers can be accommodated in the future. We are especially aiming for application in data structure verification, for which solver for the array theory would be needed.
To run, put both CLP(R) files in the same directory, and execute CLP(R) with clpr idempotent.clpr. Then at the CLP(R) prompt, say run. When the program stops for input, simply press Ctrl-D to continue. The resulting messages would not be easily comprehensible, but it shows that the engine searches for, and finds the proof that is presented in the paper.
Followings are some complete examples of manual data structure property proofs using our proof method:

List reset (my thesis advisor Joxan Jaffar's original example)
List reverse (from Reynold's LICS '02 paper on separation logic)
Binary search tree insertion
AVL tree (from a paper by Rugina)

J. Jaffar, A. E. Santosa, and R. Voicu. Efficient Memoization for Dynamic Programming with Ad-Hoc Constraints. In the Proceedings of AAAI '08. Pages 297-303. PDF copyrighted by AAAI. Follow this link to obtain AAAI '08 proceedings. Also available are the talk slides at AAAI '08. Better slides are from my CS Seminar talk at NUS, 26 September 2008.

This paper details the summarization technique presented in the thesis, with emphasis on the use of Craig interpolants to solve resource-constrained shortest path (RCSP) problems more efficiently.
Notes

We expect that memoing more solutions would enhance reusability such that the number of nodes traversed decreases as k increases, however, in the experiments reported in Table 1 where DP+I, with k=1 column is sometimes better than k=2. This can be explained as follows:
Look at the picture to the left, which illustrates a hypothetical search tree. The search is done in depth-first manner left-to-right. The horizontal arrows represent potential subsumption of nodes in the search tree, where both the graph vertices are the same, and the resource consumption of the potentially subsumed node implies the resource consumption of the potentially subsuming node.
When k=1, the algorithm only stores 1st optimal in the constraint store (represented with thick solid lines). In this case, A' is not subsumed by A due to having different optimal than A (that is, A's second optimal). In the subtree of A', B' is visited. Here, B' is not subsumed by B, due to again, having different optimal than B' (B's 3rd optimal). In another part of the search tree, B'' is subsumed by B' by inheriting the optimal.
When k=2, the algorithm stores both 1st and 2nd optimal. Here. A' is subsumed by A, since the 2nd optimal of A is the best solution of A'. However, we no longer visit B' and therefore it is no longer tabled. B'' now can no longer be subsumed by the memo table (also since B only stores 1st and 2nd, but not 3rd optimal). The algorithm then expands the potentially large subtree of B''.
The story does not end here: If B'' has a context that is equivalent to B', then we can expect that the tree size stays the same or even less due to more successful memoing within subtree of B'' with k=2 than the same within subtree of B' with k=1. However, B'' can have a strictly less solutions than B', and the algorithm's efficiency is also dependent on how early/late we discover nodes with general context, where the earlier the smaller the resulting search tree.

Errata

On Page 3, third paragraph of "The Basic Idea" section, the first sentence which reads "In order to reuse the solution of (α) at (β), we also require that the context upon reaching (β) be subsumed by the generalized context inferred for (α)," should instead read: "In order to reuse the solution of (α) at (β), we also require that the recorded optimal solution of (α) be applicable for (β)."
In the third paragraph of "The Algorithm" section, R ≤ 10 must be R' ≤ 10, as in the given example. Initial state trivially satisfies the constraint.

A. E. Santosa. A Framework for Program Reasoning Based on Constraint Traces. PhD Thesis. National University of Singapore, 2008. Download PDF version of the thesis or my thesis defense slides of which a shorter version has been presented at USI-CMU 2007 Lugano Summer School on Dependable Computer Systems.

Short Abstract. We propose a CLP-based framework that accommodates both program analysis and program verification approaches. Our framework is centered on a general verification condition computation algorithm which performs abstraction selectively. This allows for compositionality and simpler yet accurate abstraction than abstract interpretation. The algorithm is optimized between the abstraction points using a proof summarization technique. The formal foundations include modeling of programs and high-level specifications in CLP, assertions to specify traditional safety which includes recursive data structure properties, as well as structural properties (e.g., symmetry), and a proof method and techniques for proving the assertions. Our framework handles traditional safety proof, data structure verification which precision is helped by selective abstraction, and reductions using symmetry or other structural properties which can handle more cases than existing approaches. We discuss implementations of variants of our general algorithm in CLP(R) and provide their running results.
Errata

On Page 127, "Hence a finite refutation of length k implies a corresponding k left unfold LU applications that result in contradiction," should read "Hence a finite refutation of length k implies a corresponding k left unfold (LU) applications that result in contradiction."
On Page 127, "G |= H has a finite refutation of length k if and only if ..." should be "G |= H has a finite refutation of length k only if ..."
On Page 127, right below point 2, "... G |= H holds if Ai holds for all 1<=i<=n hold ..." should read "... G |= H holds if Ai holds for all 1<=i<=n ..."
On Page 129, last sentence of Section 5.7.2. The sentence should read "We provide a detailed comparison to Mesnard et al.'s proof method in Section 5.10.1." (without "of the appendix").

Notes. Some clarification on the finite refutation of length k in the correctness proof (Section 5.7.1). An assertion G |= H has a finite refutation of length k, for some k, if and only if lm(Gamma) does not imply (G |= H), which implies that Tup k does not imply G |= H (hence the errata no. 2 above). The existence of finite refutation here does not mean that we can compute the refutation. This is because in some cases, refutation can only be found at the limit.
For example, assume the program P:
odd(1). odd(X+2) :- odd(X). even(0). even(X+2) :- even(X).
One of the proof obligations obtained after performing left unfold (LU) to odd(X) |= even(X) is true |= even(1). Using our proof method, we cannot refute this last assertion, but at the limit, the assertion is not true, that is, lm(P) does not imply odd(X) |= even(X).

J. Jaffar, A. E. Santosa, and R. Voicu. Relative Safety. VMCAI 2006. PDF Talk slides PDF

Notes. Coinduction in what sense? In this paper, in the thesis above, and in our RTSS '04 paper, we have categorized our inductive proof method as coinductive and the induction that we used to be coinduction. Our proof method is coinduction in the sense that a path in the proof tree ends when we encounter a cycle. When our proof method concludes a proof, it is because the proof tree is regular, that is, there is no infinite path with unique assertion at each node (such that it is rational, which means that it has a finite representation). This is typical of coinduction proof.
For the discussion below, a useful reference would be Park's 1969 paper Fixpoint induction and proof of program properties, which appeared in Machine Intelligence 5, Edinburgh University Press, 1969.
Typically, a coinduction/greatest fixpoint-based proof is used to prove that A is included in B by restricting B into B' (= T^-1(B) for the given monotonic operator T --- since T is monotonic, necessarily B' => B, and T^-1 is also monotonic), until a fixpoint is reached, and demonstrate that A is undeniably in the fixpoint. That is,
(A => T(B')) => (A => B') ------------------------- A => gfp(T)
This can be derived from the simpler form of greatest (maximal) fixpoint induction which can be inferred from Park's article mentioned above, as follows:
B => T^-1(B) ------------- B => gfp(T)

On an assertion A (of the form G |= H), we apply any of our proof rules resulting in a set of assertions. For example, using the left unfold LU rule we obtain a set of assertions, each is the result of unfold using a particular CLP clause. This set represents a conjunction of these assertions. Using the right unfold RU rule, we obtain a set containing a single new obligation that replaces the original. Using all applicable rules other than AP we obtain a disjunction of conjunctions of assertions. Each of the disjunct implies the original assertion A, and hence the disjunction implies the original assertion A.
Therefore the parallel application our proof rules represents a monotonic operator c* (T^-1 in the above), and its inverse monotonic operator c (T in the above).
Our proof method advocates a search strategy to find "inconsistency." Formally, an assertion A is inconsistent, iff, given a program P, lm(P) does not imply A. Our proof method establishes lm(P) => A by coinduction. First, we transform A into a number of conjunctions assertions S1 ... Sn. Now since our proof rules (without AP) represent a monotonic operator, maximal fixpoint induction (a.k.a. coinduction applies).
With the application of AP rule, we establish
(lm(P) => A) => (lm(P) => (S1 \/ ... \/ Sn))
That is, assuming G |= H "holds" (formally, lm(P) => (G |= H)), we prove that its descendants also hold, and by maximal fixpoint induction rule we can therefore establish that
lm(P) => gfp(c).

Note that this discussion by no means establishes the soundness of our proof method. First, it simply says that concluding a proof using our proof method is equivalent to an inability to find inconsistency. Second, it also demonstrates the "coinductive" view of our proof method. For the soundness proof, page visitors may refer to the thesis above.

J. Jaffar, A. E. Santosa, and R. Voicu. A CLP Method for Compositional and Intemittent Predicate Abstraction. VMCAI 2006. PDF

Modeling Systems in CLP slides presented at ICLP '05 with a poster.

Errata. Unfolding does not corresponds to weakest precondition (what I have in mind here is the weakest liberal precondition of E. W. Dijkstra: A Discipline of Programming, that is, Dijkstra's weakest precondition without the requirement for termination). It is either strongest postcondition of a transition, or the strongest postcondition of its inverse (pre-image), depending on how program transitions are modeled as CLP clauses.
This does not mean that we cannot implement weakest precondition propagation indirectly using pre-image computation. Note that in a sequence t1;t2 the weakest precondition of a condition Cf for the statement t2 is wp(Cf,t2), which is equivalent to ∀(xf) (Rt2(x,xf) → Cf[xf/x]), where Rt2 is the state transition relation defined by the statement t2. Now, weakest precondition of the sequence is
∀(xf1) (Rt1(x,xf1) → (∀(xf) (Rt2(x,xf) → Cf[xf/x]))[x/xf1]),
which is equivalent to
∀(xf1,xf) (Rt1(x,xf1) /\ Rt2(xf1,xf) → Cf[xf/xf1]).
Here, Rt1(x,xf1) /\ Rt2(xf1,xf) are obtainable by pre-image computation, with unconditional initial state (final state of the program).

J. Jaffar, A. E. Santosa, and R. Voicu. A CLP Proof Method for Timed Automata. RTSS 2004. PDF

An improved version of the the prototype CLP(R) timed safety automata verifier implementation that we used in the paper is contained in this file. Also included sample bridge crossing, cafe (thanks to Dong Jinsong), dining philosophers, and Fischer's algorithm.
To run, first have CLP(R) properly installed in your system, then do:
% clpr bridge3.clpr CLP(R) Version 1.2a (c) Copyright International Business Machines Corporation 1989 (1991, 1992) All Rights Reserved ... 1 ?- run(0). Time 0.01 seconds, Unsubsumed 22 nodes, Tried 33 nodes *** Yes 2 ?-
To say, run the 3-process bridge crossing problem.
Symmetry reduction can be turned on/off by defining have_symmetry(1) or have_symmetry(0) in the source file.
Specific files in the zip are as follows:

bridge3.clpr 3-process bridge crossing
cafe.clpr work-cafe example
diners3.clpr 3-persons dining philosophers
fischer2.clpr 2-process Fischer's algorithm
u28b.clpr the verifier engine

Declarative Concurrent Programming

This work is the result of my collaboration with Professor Rafael Ramirez of Universitat Pompeu Fabra.

R. Ramirez and A. E. Santosa. Concurrent Programming Made Easy. ICECCS 2000. PDF

A. E. Santosa and Y. Kawata and M. Maekawa. A Solution to Inheritance Anomaly Based on Reusable Behavior Definitions In PDCS '98. PDF

Some of my earlier ideas on inheritance anomaly problem in concurrent object-oriented programming languages, put here due to its relation with declarative concurrent programming. I consider inheritance anomaly problem to be solved not by me, but by Crnogorac, Rao and Ramamohanarao in Classifying Inheritance Mechanism in Concurrent Object-Oriented Programming, ECOOP '98, demonstrating the power of solid mathematics to scaffold ideas.

Selected Other Work

K. Q. Zhu and A. E. Santosa. A Meeting Scheduling System Based on Open Constraint Programming. CAiSE 2002. PDF
A. E. Santosa: Fast mutual exclusion algorithms: The MPI implementation. 23 October 2000. This is a short survey on fast mutual exclusion algorithms (algorithms with O(1) without contention), either with or without special instructions. MPI implementations included. PDF

CLP(R) Bag of Tricks

Before I start, for those who want to learn constraint logic programming or Prolog, the fastest possible way known to me is to study the short book Professional Programmer's Guide to Prolog by A. G. Hamilton, published in 1989 by Pitman Publishing. It does not only teach you how to program, but how to program the logic programming way. You can always attach a counter at every recursion ala imperative for loops, but the book will teach you the more effective use of logic programming recursions.

The Tao of debugging using printf. In the current version, CLP(R) only has rudimentary debugging support using codegen_debug, and spy, trace. These, however, are difficult to use: they tend to produce huge call traces that are difficult to analyze.
When a programmer suspects that a call to a predicate, say, p(X,Y,Z) does not behave correctly, an easy way to check input-output behavior is to first identify the input variables of the predicate. If uncertain, only pick as input variables conservatively (only those you are certain to be input variables). Suppose that in the call p(X,Y,Z), we know that X and Y are input. Now, before the call, add a printf and a read, resulting in:
```
printf("p(%, %, Z)\n", [X, Y]),
read(_),
p(X, Y, Z),
```
instead of the original call. In this way, when it is about to execute the call, the program would first print, say, p(1, [2,3], Z) on the terminal and waits for standard input. Here, the programmer can input something (say x.) on the standard input to continue to the next breakpoint. More importantly, the programmer terminate the program (by Ctrl-C), then copy the output p(1, [2,3], Z) to CLP(R)'s prompt, and execute it in isolation to observe the behavior.
Software engineering wise, this allows rapid writing of CLP(R) programs to be debugged later. I need to do more programming myself to confirm that the technique is actually effective for rapid production of CLP(R) programs.
How to negate constraints. Sometimes negating constraints on a set of variables is necessary, for instance, when proving implication problems dynamically generated during program run (implication of A => B holds iff A and not B is unsatisfiable).
Suppose that we want to prove X > 2 => X > 0. To negate X > 0, we use the following procedure:
```
p(X, X1) :-
    dump([X1], [Y], L), negate_list(L, X, Y).

negate_list([], X, Y).
negate_list([C|R], X, Y) :-
    negate(C), not X=Y, negate_list(R, X, Y).

negate(quote(A > B)) :-
    once(expreval(A)), once(expreval(B)), A <= B.
...

expreval(X) :- var(A).
expreval(X) :- atomic(A).
...
expreval(quote(A + B)) :- A + B.
...
```
The main point here is the use of dump/3 to produce the quoted form of the constraint at hand, which we can then negate.
To prove the implication X > 2 => X > 0, we run
```
:- X > 2, X1 > 0, p(X, X1).
```

Latest update: 9 October 2008. Contents created using Emacs, LaTeX, and Xfig.