ScholarBank@NUShttps://scholarbank.nus.edu.sgThe DSpace digital repository system captures, stores, indexes, preserves, and distributes digital research material.Tue, 15 Oct 2024 04:06:16 GMT2024-10-15T04:06:16Z50331- Path-sensitive resource analysis compliant with assertionshttps://scholarbank.nus.edu.sg/handle/10635/78281Title: Path-sensitive resource analysis compliant with assertions
Authors: Chu, D.-H.; Jaffar, J.
Abstract: We consider the problem of bounding the worst-case resource usage of programs, where assertions about valid program executions may be enforced at selected program points. It is folklore that to be precise, path-sensitivity (up to loops) is needed. This entails unrolling loops in the manner of symbolic simulation. To be tractable, however, the treatment of the individual loop iterations must be greedy in the sense once analysis is finished on one iteration, we cannot backtrack to change it. We show that under these conditions, enforcing assertions produces unsound results. The fundamental reason is that complying with assertions requires the analysis to be fully sensitive (also with loops) wrt. the assertion variables. We then present an algorithm where the treatment of each loop is separated in two phases. The first phase uses a greedy strategy in unrolling the loop. This phase explores what is conceptually a symbolic execution tree, which is of enormous size, while eliminates infeasible paths and dominated paths that guaranteed not to contribute to the worst case bound. A compact representation is produced at the end of this phase. Finally, the second phase attacks the remaining problem, to determine the worst-case path in the simplified tree, excluding all paths that violate the assertions from bound calculation. Scalability, in both phases, is achieved via an adaptation of a dynamic programming algorithm. © 2013 IEEE.
Tue, 01 Jan 2013 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/782812013-01-01T00:00:00Z
- An efficient algorithm for scheduling instructions with deadline constraints on ILP processorshttps://scholarbank.nus.edu.sg/handle/10635/40556Title: An efficient algorithm for scheduling instructions with deadline constraints on ILP processors
Authors: Wu, H.; Jaffar, J.
Abstract: We propose an efficient algorithm for scheduling UET (Unit Execution Time) instructions with deadline constraints on ILP (Instruction Level Parallelism) processors with multiple functional units of different types. The time complexity of our algorithm is O(ne + nd), where n is the number of instructions, e is the number of edges in the precedence graph and d is the maximum latency. Our algorithm is guaranteed to compute a feasible schedule whenever one exists in the following special cases: I) Arbitrary precedence constraints, latencies in {-1, 0} and two functional units. 2) In-forest, equal latencies and multiple functional units. 3) Monotone interval graph and multiple functional units. For all above special cases, if no feasible schedule exists, our algorithm will compute a schedule with minimum lateness. In each of the above special cases, no polynomial time algorithm existed before. Moreover, by setting all deadlines to a sufficiently large integer, our algorithm will compute a schedule with minimum length in all the above special cases.
Mon, 01 Jan 2001 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/405562001-01-01T00:00:00Z
- Modeling systems in CLPhttps://scholarbank.nus.edu.sg/handle/10635/40660Title: Modeling systems in CLP
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/406602005-01-01T00:00:00Z
- Generalized committed choicehttps://scholarbank.nus.edu.sg/handle/10635/40845Title: Generalized committed choice
Authors: Jaffar, J.; Yap, R.H.C.; Zhu, K.Q.
Abstract: We present a generalized committed choice construct for concurrent programs that interact with a shared store. The generalized committed choice (GCC) allows multiple computations from different alternatives to occur concurrently and later commit to one of them. GCC generalizes the traditional committed choice in Dijkstra's Guarded Command Language to handle don't know non-determinism and also allows for speculative computation. The main contribution of the paper is to introduce the GCC programming construct and the associated semantics framework for formalizing GCC. We give some experimental results which show that the power of GCC can be made practical. © Springer-Verlag Berlin Heidelberg 2007.
Mon, 01 Jan 2007 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/408452007-01-01T00:00:00Z
- Instruction scheduling with release times and deadlines on ILP processorshttps://scholarbank.nus.edu.sg/handle/10635/40858Title: Instruction scheduling with release times and deadlines on ILP processors
Authors: Wu, H.; Jaffar, J.; Xue, J.
Abstract: ILP (Instruction Level Parallelism) processors are being increasingly used in embedded systems. In embedded systems, instructions may be subject to timing constraints. An optimising compiler for ILP processors needs to find a feasible schedule for a set of time-constrained instructions. In this paper, we present a fast algorithm for scheduling instructions with precedence-latency constraints, individual integer release times and deadlines on an ILP processor with multiple functional units. The time complexity of our algorithm is O(n 2 log d) + min{O(de), O(ne)} + min{O(ne), O(n 2.376)}, where n is the number of instructions, e is the number of edges in the precedence graph and d is the maximum latency. Our algorithm is guaranteed to find a feasible schedule whenever one exists in the following special cases: 1) one functional unit, arbitrary precedence constraints, latencies in {0, 1}, integer release times and deadlines; 2) two identical functional units, arbitrary precedence constraints, latencies of 0, integer release times and deadlines; 3) multiple identical functional units or multiple functional units of different types, monotone interval-ordered graph, integer release times and deadlines; 4) multiple identical functional units, in-forest, equal latencies, integer release times and deadlines. In case 1), our algorithm improves the existing fastest algorithm from O(n 2 log n) + mm{O(ne),O(n 2.376)} to min{O(ne), O(n 2.376)}. In case 2), our algorithm improves the existing faste st algorithm from O(ne + n 2 log n) to min{O(ne), O(n 2.376)}. In case 3), no polynomial time algorithm for multiple functional units of different types was known before. © 2006 IEEE.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/408582006-01-01T00:00:00Z
- Two processor scheduling with real release times and deadlineshttps://scholarbank.nus.edu.sg/handle/10635/40985Title: Two processor scheduling with real release times and deadlines
Authors: Wu, H.; Jaffar, J.
Abstract: In a hard real-time system, critical tasks are subject to timing constraints such as release times and deadlines. All timing constraints must be satisfied when tasks are executed. Nevertheless, given a set of tasks, finding a feasible schedule which satisfies all timing constraints is NP-complete even on one processor. In this paper, we study the following special non-preemptive two processor scheduling problem: Given a set of UET (Unit Execution Time) tasks with arbitrary precedence constraints, individual real release times and deadlines, find a feasible schedule on two identical processors whenever one exists. The complexity status of this problem has been open for a long time, we propose the first polynomial algorithm for this problem. Our algorithm is underpinned by the key consistency notion: Successor-tree-consistency. The time complexity of our algorithm is O(n4), where n is the number of tasks.
Tue, 01 Jan 2002 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/409852002-01-01T00:00:00Z
- A coinduction rule for entailment of recursively defined propertieshttps://scholarbank.nus.edu.sg/handle/10635/41110Title: A coinduction rule for entailment of recursively defined properties
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: Recursively defined properties are ubiquitous. We present a proof method for establishing entailment of such properties and over a set of common variables. The main contribution is a particular proof rule based intuitively upon the concept of coinduction. This rule allows the inductive step of assuming that an entailment holds during the proof the entailment. In general, the proof method is based on an unfolding (and no folding) algorithm that reduces recursive definitions to a point where only constraint solving is necessary. The constraint-based proof obligation is then discharged with available solvers. The algorithm executes the proof by a search-based method which automatically discovers the opportunity of applying induction instead of the user having to specify some induction schema, and which does not require any base case. © 2008 Springer-Verlag Berlin Heidelberg.
Tue, 01 Jan 2008 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411102008-01-01T00:00:00Z
- Efficient memoization for dynamic programming with ad-hoc constraintshttps://scholarbank.nus.edu.sg/handle/10635/41111Title: Efficient memoization for dynamic programming with ad-hoc constraints
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: We address the problem of effective reuse of subproblem solutions in dynamic programming. In dynamic programming, a memoed solution of a subproblem can be reused for another if the latter's context is a special case of the former. Our objective is to generalize the context of the memoed subproblem such that more subproblems can be considered subcases and hence enhance reuse. Toward this goal we propose a generalization of context that 1) does not add better solutions than the subproblem's optimal, yet 2) requires that subsumed sub-problems preserve the optimal solution. In addition, we also present a general technique to search for at most k ≥ 1 optimal solutions. We provide experimental results on resource-constrained shortest path (RCSP) benchmarks and program's exact worst-case execution time (WCET) analysis. Copyright © 2008, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
Tue, 01 Jan 2008 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411112008-01-01T00:00:00Z
- A CLP proof method for timed automatahttps://scholarbank.nus.edu.sg/handle/10635/41107Title: A CLP proof method for timed automata
Authors: Jaffar, J.; Santosa, A.; Voicu, R.
Abstract: Constraint Logic Programming (CLP) has been used to model programs and transition systems for the purpose of verification problems. In particular, it has been used to model Timed Safety Automata (TSA). In this paper, we start with a systematic translation of TSA into CLP. The main contribution is an expressive assertion language and a new CLP inference method for proving assertions. A distinction of the assertion language is that it can specify important properties beyond traditional safety properties. We highlight one important property: that a system of processes is symmetric. The new inference mechanism is based upon the well-known method of tabling in logic programming. It is distinguished by its ability to use assertions that are not yet proven, using a principle of coinduction. Apart from given assertions, the proof mechanism can also prove implicit assertions such as discovering a lower or upper bound of a variable. Finally, we demonstrate significant improvements over state-of-the-art systems using standard TSA benchmark examples. © 2004 IEEE.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411072004-01-01T00:00:00Z
- Coordination of many agentshttps://scholarbank.nus.edu.sg/handle/10635/41109Title: Coordination of many agents
Authors: Jaffar, J.; Yap, R.H.C.; Zhu, K.Q.
Abstract: This paper presents a reactive programming and triggering framework for the coordination of a large number of distributed agents with shared knowledge. At the heart of this framework is a highly structured shared store in the form of a constraint logic program (CLP), which is used as a knowledge base and being reacted to by agents through the use of "reactors". The biggest challenge arising from such a reactive programming framework using CLP is to develop a trigger mechanism that allows efficient "wakeup" of blocked reactors. This paper addresses the architecture of this open framework, and discusses a general methodology for doing triggering of logic conditions using views and abstractions. © Springer-Verlag Berlin Heidelberg 2005.
Sat, 01 Jan 2005 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411092005-01-01T00:00:00Z
- Scalable distributed depth-first search with greedy work stealinghttps://scholarbank.nus.edu.sg/handle/10635/41101Title: Scalable distributed depth-first search with greedy work stealing
Authors: Jaffar, J.; Santosa, A.E.; Yap, R.H.C.; Zhu, K.Q.
Abstract: We present a framework for the parallelization of depth-first combinatorial search algorithms on a network of computers. Our architecture is intended for a distributed setting and uses a work stealing strategy coupled with a small number of primitives for the processors (which we call workers) to obtain new work and to communicate to other workers. These primitives are a minimal imposition and integrate easily with constraint programming systems. The main contribution is an adaptive architecture which allows workers to incrementally join and leave and has good scaling properties as the number of workers increases. Our empirical results illustrate that near-linear speedup for backtrack search is achieved for up to 61 workers. It suggests that near-linear speedup is possible with even more workers. The experiments also demonstrate where departures from linearity can occur for small problems, and also for problems where the parallelism can itself affect the search as in branch and bound. © 2004 IEEE.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411012004-01-01T00:00:00Z
- Unbounded symbolic execution for program verificationhttps://scholarbank.nus.edu.sg/handle/10635/41106Title: Unbounded symbolic execution for program verification
Authors: Jaffar, J.; Navas, J.A.; Santosa, A.E.
Abstract: Symbolic execution with interpolation is emerging as an alternative to cegar for software verification. The performance of both methods relies critically on interpolation in order to obtain the most general abstraction of the current symbolic or abstract state which can be shown to remain error-free. cegar naturally handles unbounded loops because it is based on abstract interpretation. In contrast, symbolic execution requires a special extension for such loops. In this paper, we present such an extension. Its main characteristic is that it performs eager subsumption, that is, it always attempts to perform abstraction in order to avoid exploring redundant symbolic states. It balances this primary desire for more abstraction with the secondary desire to maintain the strongest loop invariant, for earlier detection of infeasible paths, which entails less abstraction. Occasionally certain abstractions are not permitted because of the reachability of error states; this is the underlying mechanism which then causes selective unrolling, that is, the unrolling of a loop along relevant paths only. © 2012 Springer-Verlag.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411062012-01-01T00:00:00Z
- Recursive abstractions for parameterized systemshttps://scholarbank.nus.edu.sg/handle/10635/41105Title: Recursive abstractions for parameterized systems
Authors: Jaffar, J.; Santosa, A.E.
Abstract: We consider a language of recursively defined formulas about arrays of variables, suitable for specifying safety properties of parameterized systems. We then present an abstract interpretation framework which translates a paramerized system as a symbolic transition system which propagates such formulas as abstractions of underlying concrete states. The main contribution is a proof method for implications between the formulas, which then provides for an implementation of this abstract interpreter. © 2009 Springer-Verlag Berlin Heidelberg.
Thu, 01 Jan 2009 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411052009-01-01T00:00:00Z
- An interpolation method for CLP traversalhttps://scholarbank.nus.edu.sg/handle/10635/41103Title: An interpolation method for CLP traversal
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: We consider the problem of exploring the search tree of a CLP goal in pursuit of a target property. Essential to such a process is a method of tabling to prevent duplicate exploration. Typically, only actually traversed goals are memoed in the table. In this paper we present a method where, upon the successful traversal of a subgoal, a generalization of the subgoal is memoed. This enlarges the record of already traversed goals, thus providing more pruning in the subsequent search process. The key feature is that the abstraction computed is guaranteed not to give rise to a spurious path that might violate the target property. A driving application area is the use of CLP to model the behavior of other programs. We demonstrate the performance of our method on a benchmark of program verfication problems. © 2009 Springer Berlin Heidelberg.
Thu, 01 Jan 2009 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411032009-01-01T00:00:00Z
- TRACER: A symbolic execution tool for verificationhttps://scholarbank.nus.edu.sg/handle/10635/41102Title: TRACER: A symbolic execution tool for verification
Authors: Jaffar, J.; Murali, V.; Navas, J.A.; Santosa, A.E.
Abstract: We present TRACER, a verifier for safety properties of sequential C programs. It is based on symbolic execution (se) and its unique features are in how it makes se finite in presence of unbounded loops and its use of interpolants from infeasible paths to tackle the path-explosion problem. © 2012 Springer-Verlag.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/411022012-01-01T00:00:00Z
- Fast algorithm for scheduling instructions with deadline constraints on RISC machineshttps://scholarbank.nus.edu.sg/handle/10635/40999Title: Fast algorithm for scheduling instructions with deadline constraints on RISC machines
Authors: Wu, Hui; Jaffar, Joxan; Yap, Roland
Abstract: We present a fast algorithm for scheduling UET(Unit Execution Time) instructions with deadline constraints in a basic block on RISC machines with multiple processors. Unlike Palem and Simon's algorithm, our algorithm allows latency of lij = -1 which denotes that instruction vj cannot be started before vi. The time complexity of our algorithms is O(ne + nd), where n is the number of instructions, e is the number of edges in the precedence graph and d is the maximum latency. Our algorithm is guaranteed to compute a feasible schedule whenever one exists in the following special cases: 1) Arbitrary precedence constraints, latencies in {0, 1} and one processor. In this special case, our algorithm improves the existing fastest algorithm from O(ne + e′ log n) to O(min{ne, n2.376}), where e′ is the number of edges in the transitively closed precedence graph. 2) Arbitrary precedence constraints, latencies in {-1, 0} and two processors. In the special case where all latencies are 0, our algorithm degenerates to Garey and Johnson's two processor algorithm. 3) Special precedence constraints in the form of monotone interval graph, arbitrary latencies in {-1, 0, 1, ..., d} and multiple processors. 4) Special precedence constraints in the form of in-forest, equal latencies and multiple processors. In the above special cases, if no feasible schedule exists, our algorithm will compute a schedule with minimum lateness. Moreover, by setting all deadlines to a sufficiently large integer, our algorithm will compute a schedule with minimum length in all the above special cases and the special case of out-forest, equal latencies and multiple processors.
Sat, 01 Jan 2000 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/409992000-01-01T00:00:00Z
- An efficient distributed deadlock avoidance algorithm for the AND modelhttps://scholarbank.nus.edu.sg/handle/10635/39175Title: An efficient distributed deadlock avoidance algorithm for the AND model
Authors: Wu, H.; Chin, W.-N.; Jaffar, J.
Abstract: A new rank-based distributed deadlock avoidance algorithm for the AND resource request model is presented. Deadlocks are avoided by dynamically maintaining an invariant Con(WFG): For each pair of processes pi and pj, pi is allowed wait for process pj iff the rank of pj is greater than that of pi for the WFG (Wait-For Graph). Our algorithm neither restricts the order of resource requests nor needs a priori information about resource requests nor causes unnecessary abortion of processes. Multidimensional ranks, which are partially ordered and dynamically modified, are used to drastically reduce the cost of maintaining Con(WFG). Our simulation results show that the performance of our algorithm is better than that of existing algorithms.
Tue, 01 Jan 2002 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/391752002-01-01T00:00:00Z
- Functional elimination and 0/1/All constraintshttps://scholarbank.nus.edu.sg/handle/10635/39265Title: Functional elimination and 0/1/All constraints
Authors: Zhang, Yuanlin; Yap, Roland H.C.; Jaffar, Joxan
Abstract: We present new complexity results on the class of 0/1/All constraints. The central idea involves functional elimination, a general method of elimination whose focus is on the subclass of functional constraints. One result is that for the subclass of 'All' constraints, strong n-consistency and minimality is achievable in O(en) time, where e, n are the number of constraints and variables. The main result is that we can solve 0/1/All constraints in O(e(d + n)) time, where d is the domain size. This is an improvement over known results, which are O(ed(d + n)). Furthermore, our algorithm also achieves strong n-consistency and minimality.
Fri, 01 Jan 1999 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/392651999-01-01T00:00:00Z
- Toward optimal mc/dc test case generationhttps://scholarbank.nus.edu.sg/handle/10635/194481Title: Toward optimal mc/dc test case generation
Authors: Godboley, Sangharatna; Jaffar, Joxan; Maghareh, Rasool; Dutta, Arpita
Sun, 11 Jul 2021 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/1944812021-07-11T00:00:00Z
- Constraint Programming 2000: A Position Paperhttps://scholarbank.nus.edu.sg/handle/10635/99226Title: Constraint Programming 2000: A Position Paper
Authors: Jaffar, J.; Yap, R.H.C.
Abstract: We put forward that required enhancements to constraint programming technology include concurrency, more sophisticated control mechanisms, and new features for expressing preferences.
Wed, 01 Jan 1997 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/992261997-01-01T00:00:00Z
- A CLP approach to modelling systemshttps://scholarbank.nus.edu.sg/handle/10635/39369Title: A CLP approach to modelling systems
Authors: Jaffar, J.
Thu, 01 Jan 2004 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/393692004-01-01T00:00:00Z
- Framework for combining analysis and verificationhttps://scholarbank.nus.edu.sg/handle/10635/40247Title: Framework for combining analysis and verification
Authors: Heintze, N.; Jaffar, J.; Voicu, R.
Abstract: We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis. In this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. The framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. Further, it has some important features: it is flexible: any number of assertions can be used anywhere; it is open: it can employ an arbitrary analyzer; it is modular: we reason with conditional correctness of assertions; it is incremental: it can be tuned for the accuracy/efficiency tradeoff.
Sat, 01 Jan 2000 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/402472000-01-01T00:00:00Z
- A complete method for symmetry reduction in safety verificationhttps://scholarbank.nus.edu.sg/handle/10635/40008Title: A complete method for symmetry reduction in safety verification
Authors: Chu, D.-H.; Jaffar, J.
Abstract: Symmetry reduction is a well-investigated technique to counter the state space explosion problem for reasoning about a concurrent system of similar processes. Here we present a general method for its application, restricted to verification of safety properties, but without any prior knowledge about global symmetry. We start by using a notion of weak symmetry which allows for more reduction than in previous notions of symmetry. This notion is relative to the target safety property. The key idea is to perform symmetric transformations on state interpolation, a concept which has been used widely for pruning in SMTand CEGAR. Our method naturally favors "quite symmetric" systems: more similarity among the processes leads to greater pruning of the tree. The main result is that the method is complete wrt. weak symmetry: it only considers states which are not weakly symmetric to an already encountered state. © 2012 Springer-Verlag.
Sun, 01 Jan 2012 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/400082012-01-01T00:00:00Z
- A CLP method for compositional and intermittent predicate abstractionhttps://scholarbank.nus.edu.sg/handle/10635/40121Title: A CLP method for compositional and intermittent predicate abstraction
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: We present an implementation of symbolic reachability analysis with the features of compositionality, and intermittent abstraction, in the sense of pefrorming approximation only at selected program points, if at all. The key advantages of compositionality are well known, while those of intermittent abstraction are that the abstract domain required to ensure convergence of the algorithm can be minimized, and that the cost of performing abstractions, now being intermittent, is reduced. We start by formulating the problem in CLP, and first obtain compositionality. We then address two key efficiency challenges. The first is that reasoning is required about the strongest-postcondition operator associated with an arbitrarily long program fragment. This essentially means dealing with constraints over an unbounded number of variables describing the states between the start and end of the program fragment at hand. This is addressed by using the variable elimination or projection mechanism that is implicit in CLP systems. The second challenge is termination, that is, to determine which subgoals are redundant. We address this by a novel formulation of memoization called coinductive tabling. We finally evaluate the method experimentally. At one extreme, where abstraction is performed at every step, we compare against a model checker. At the other extreme, where no abstraction is performed, we compare against a program verifier. Of course, our method provides for the middle ground, with a flexible combination of abstraction and Hoare-style reasoning with predicate transformers and loop-invariants. © Springer-Verlag Berlin Heidelberg 2006.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/401212006-01-01T00:00:00Z
- Relative safetyhttps://scholarbank.nus.edu.sg/handle/10635/40122Title: Relative safety
Authors: Jaffar, J.; Santosa, A.E.; Voicu, R.
Abstract: A safety property restricts the set of reachable states. In this paper, we introduce a notion of relative safety which states that certain program states are reachable provided certain other states are. A key, but not exclusive, application of this method is in representing symmetry in a program. Here, we show that relative safety generalizes the programs that are presently accommodated by existing methods for symmetry. Finally, we provide a practical algorithm for proving relative safety. © Springer-Verlag Berlin Heidelberg 2006.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/401222006-01-01T00:00:00Z
- Symbolic simulation on complicated loops for WCET path analysishttps://scholarbank.nus.edu.sg/handle/10635/40047Title: Symbolic simulation on complicated loops for WCET path analysis
Authors: Chu, D.-H.; Jaffar, J.
Abstract: We address the Worst-Case Execution Time (WCET) Path Analysis problem for bounded programs, formalized as discovering a tight upper bound of a resource variable. A key challenge is posed by complicated loops whose iterations exhibit non-uniform behavior. We adopt a brute-force strategy by simply unrolling them, and show how to make this scalable while preserving accuracy. Our algorithm performs symbolic simulation of the program. It maintains accuracy because it preserves, at critical points, path-sensitivity. In other words, the simulation detects infeasible paths. Scalability, on the other hand, is dealt with by using summarizations, compact representations of the analyses of loop iterations. They are obtained by a judicious use of abstraction which preserves critical information flowing from one iteration to another. These summarizations can be compounded in order for the simulation to have linear complexity: the symbolic execution can in fact be asymptotically shorter than a concrete execution. Finally, we present a comprehensive experimental evaluation using a standard benchmark suite. We show that our algorithm is fast, and importantly, we often obtain not just accurate but exact results. Copyright © 2011 ACM.
Sat, 01 Jan 2011 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/400472011-01-01T00:00:00Z
- Constraint-based program reasoning with heaps and separationhttps://scholarbank.nus.edu.sg/handle/10635/78067Title: Constraint-based program reasoning with heaps and separation
Authors: Duck, G.J.; Jaffar, J.; Koh, N.C.H.
Abstract: This paper introduces a constraint language H for finite partial maps (a.k.a. heaps) that incorporates the notion of separation from Separation Logic. We use H to build an extension of Hoare Logic for reasoning over heap manipulating programs using (constraint-based) symbolic execution. We present a sound and complete algorithm for solving quantifier-free (QF) H-formulae based on heap element propagation. An implementation of the H-solver has been integrated into a Satisfiability Modulo Theories (SMT) framework. We experimentally evaluate the implementation against Verification Conditions (VCs) generated from symbolic execution of large (heap manipulating) programs. In particular, we mitigate the path explosion problem using subsumption via interpolation - made possible by the constraint-based encoding. © 2013 Springer-Verlag.
Tue, 01 Jan 2013 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/780672013-01-01T00:00:00Z
- Boosting concolic testing via interpolationhttps://scholarbank.nus.edu.sg/handle/10635/78046Title: Boosting concolic testing via interpolation
Authors: Jaffar, J.; Murali, V.; Navas, J.A.
Abstract: Concolic testing has been very successful in automatically generating test inputs for programs. However one of its major limitations is path-explosion that limits the generation of high coverage inputs. Since its inception several ideas have been proposed to attack this problem from various angles: defining search heuristics that increase coverage, caching of function summaries, pruning of paths using static/dynamic information etc. We propose a new and complementary method based on interpolation, that greatly mitigates pathexplosion by subsuming paths that can be guaranteed to not hit a bug. We discuss new challenges in using interpolation that arise specifically in the context of concolic testing. We experimentally evaluate our method with different search heuristics using Crest, a publicly available concolic tester. Copyright 2013 ACM.
Tue, 01 Jan 2013 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/780462013-01-01T00:00:00Z
- Indexing for dynamic abstract regionshttps://scholarbank.nus.edu.sg/handle/10635/40573Title: Indexing for dynamic abstract regions
Authors: Jaffar, J.; Yap, R.H.C.; Zhu, K.Q.
Abstract: We propose a new main memory index structure for abstract regions (objects) which may heavily overlap, the RC-tree. These objects are "dynamic" and may have short life spans. The novelty is that rather than representing an object by its minimum bounding rectangle (MBR), possibly with pre-processed segmentation into many small MBRs, we use the actual shape of the object to maintain the index. This saves significant space for objects with large spatial extents since pre-segmentation is not needed. We show that the query performance of RC-tree is much better than many indexing schemes on synthetic overlapping data sets. The performance is also competitive on real-life GIS non-overlapping data sets. © 2006 IEEE.
Sun, 01 Jan 2006 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/405732006-01-01T00:00:00Z
- Architecture and prototype implementation of a system for individualized workflows in medical information systemshttps://scholarbank.nus.edu.sg/handle/10635/40467Title: Architecture and prototype implementation of a system for individualized workflows in medical information systems
Authors: Jaffar, Joxan; Maher, Michael J.; Neumann, Gustaf
Abstract: This paper is a report from a project that tried to design and implement a highly flexible workflow management system in the area of patient care delivery. Within eight weeks the authors developed a formal model for the specification of medical directives, designed and implemented a coordination system (based on the IBM prototype OBJCHART) with multi-user capabilities, and developed graphical user agents for the most important classes of users of the system (medical doctors, nurses and nurse technicians). This rapid development was possible not least due to the modular design of the system, which is made up of highly specialized, declarative and orthogonal components.
Fri, 01 Jan 1999 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/404671999-01-01T00:00:00Z
- Toward Practical Query Evaluation for Constraint Databaseshttps://scholarbank.nus.edu.sg/handle/10635/99444Title: Toward Practical Query Evaluation for Constraint Databases
Authors: Brodsky, A.; Jaffar, J.; Maher, M.J.
Abstract: Linear constraint databases (LCDBs) extend relational databases to include linear arithmetic constraints in both relations and queries. A LCDB can also be viewed as a powerful extension of linear programming (LP) where the system of constraints is generalized to a database containing constraints and the objective function is generalized to a relational query containing constraints. Our major concern is query optimization in LCDBs. Traditional database approaches are not adequate for combination with LP technology. Instead, we propose a new query optimization approach, based on statistical estimations and iterated trials of potentially better evaluation plans. The resulting algorithms are not only effective on LCDBs, but also applicable to existing query languages. A number of specific constraint algebra algorithms are also developed: select-project-join for two relations, constraint sort-join and constraint multi-join.
Wed, 01 Jan 1997 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/994441997-01-01T00:00:00Z
- The semantics of constraint logic programshttps://scholarbank.nus.edu.sg/handle/10635/99440Title: The semantics of constraint logic programs
Authors: Jaffar, J.; Maher, M.; Marriott, K.; Stuckey, P.
Abstract: The Constraint Logic Programming (CLP) Scheme was introduced by Jaffar and Lassez. The scheme gave a formal framework, based on constraints, for the basic operational, logical and algebraic semantics of an extended class of logic programs. This paper presents for the first time the semantic foundations of CLP in a self-contained and complete package. The main contributions are threefold. First, we extend the original conference paper by presenting definitions and basic semantic constructs from first principles, giving new and complete proofs for the main lemmas. Importantly, we clarify which theorems depend on conditions such as solution compactness, satisfaction completeness and independence of constraints. Second, we generalize the original results to allow for incompleteness of the constraint solver. This is important since almost all CLP systems use an incomplete solver. Third, we give conditions on the (possibly incomplete) solver which ensure that the operational semantics is confluent, that is, has independence of literal scheduling. © 1998 Elsevier Science Inc. All rights reserved.
Thu, 01 Oct 1998 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/994401998-10-01T00:00:00Z
- Using constraints to model disjunctions in rule-based reasoninghttps://scholarbank.nus.edu.sg/handle/10635/99612Title: Using constraints to model disjunctions in rule-based reasoning
Authors: Liu, Bing; Jaffar, Joxan
Abstract: Rule-based systems have long been widely used for building expert systems to perform practical knowledge intensive tasks. One important issue that has not been addressed satisfactorily is the disjunction, and this significantly limits their problem solving power. In this paper, we show that some important types of disjunction can be modeled with Constraint Satisfaction Problem (CSP) techniques, employing their simple representation schemes and efficient algorithms. A key idea is that disjunctions are represented as constraint variables, relations among disjunctions are represented as constraints, and rule chaining is integrated with constraint solving. In this integration, a constraint variable or a constraint is regarded as a special fact, and rules can be written with constraints and information about constraints. Chaining of rules may trigger constraint propagation, and constraint propagation may cause firing of rules. A prototype system (called CFR) based on this idea has been implemented.
Mon, 01 Jan 1996 00:00:00 GMThttps://scholarbank.nus.edu.sg/handle/10635/996121996-01-01T00:00:00Z