Joxan Jaffar
Email Address
dcsjj@nus.edu.sg
33 results
Publication Search Results
Now showing 1 - 10 of 33
Publication Architecture and prototype implementation of a system for individualized workflows in medical information systems(1999) Jaffar, Joxan; Maher, Michael J.; Neumann, Gustaf; COMPUTER SCIENCEThis 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.Publication Toward optimal mc/dc test case generation(ACM, 2021-07-11) Godboley, Sangharatna; Jaffar, Joxan; Maghareh, Rasool; Dutta, Arpita; Prof Joxan Jaffar; DEPARTMENT OF COMPUTER SCIENCEPublication Generalized committed choice(2007) Jaffar, J.; Yap, R.H.C.; Zhu, K.Q.; COMPUTER SCIENCEWe 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.Publication A complete method for symmetry reduction in safety verification(2012) Chu, D.-H.; Jaffar, J.; COMPUTER SCIENCESymmetry 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.Publication Constraint-based program reasoning with heaps and separation(2013) Duck, G.J.; Jaffar, J.; Koh, N.C.H.; COMPUTER SCIENCEThis 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.Publication Unbounded symbolic execution for program verification(2012) Jaffar, J.; Navas, J.A.; Santosa, A.E.; COMPUTER SCIENCESymbolic 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.Publication Coordination of many agents(2005) Jaffar, J.; Yap, R.H.C.; Zhu, K.Q.; COMPUTER SCIENCEThis 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.Publication Relative safety(2006) Jaffar, J.; Santosa, A.E.; Voicu, R.; COMPUTER SCIENCEA 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.Publication Fast algorithm for scheduling instructions with deadline constraints on RISC machines(2000) Wu, Hui; Jaffar, Joxan; Yap, Roland; COMPUTER SCIENCEWe 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.Publication Path-sensitive resource analysis compliant with assertions(2013) Chu, D.-H.; Jaffar, J.; COMPUTER SCIENCEWe 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.