Scalable Distributed Depth-First Search with Greedy Work Stealing (2009)
Joxan Jaffar, Andrew E. Santosa, Roland H. C, Yap Kenny, Q. Zhu
We present a framework for the parallelization of depthfirst combinatorial search algorithms on a network of computers. Our architecture is intended for a distributed setting and uses a work stealing...
A Framework for Combining Analysis and Verification (2008)
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...
Generalized Committed Choice (2008)
Joxan Jaffar, H. C. Yap, Kenny Q. Zhu
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...
Instruction Scheduling with Release Times and Deadlines on ILP Processors (2008)
Hui Wu, Jingling Xue, Joxan Jaffar, Texas Instruments, Ti C, Philips Trimedia
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...
Efficient Memoization for Dynamic Programming with Ad-Hoc Constraints (2008)
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
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...
J. LOGIC PROGRAMMING: to appear 1 Constraint Logic Programming: A Survey (2008)
Joxan Jaffar, Michael J. Maher
Constraint Logic Programming (CLP) is a merger of two declarative paradigms: constraint solving and logic programming. Though a relatively new eld, CLP has progressed in several quite di erent...
Generalized Committed Choice (2008)
Joxan Jaffar, H. C. Yap, Kenny Q. Zhu
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...
Abstraction in Search-Based Optimization (2008)
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
Search-based techniques for optimization have the advantage of easy formulation. The traditional and only general method to deal with the consequent state explosion is forward-pruning: terminating a...
Abstract Summarizations for Symbolic Executions (2008)
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
Consideration of execution paths is basic in program analysis and verification because it represents the process of exact propagation through the program fragment at hand. This is challenged by the...
Coordination of Many Agents (2008)
Joxan Jaffar, H. C. Yap, Kenny Q. Zhu
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...
J. LOGIC PROGRAMMING: to appear 1 Constraint Logic Programming: A Survey (2007)
Joxan Jaffar, Michael J. Maher
Constraint Logic Programming (CLP) is a merger of two declarative paradigms: constraint solving and logic programming. Though a relatively new field, CLP has progressed in several quite different...
A General Framework for Program Reasoning (2007)
Nevin Heintze, R Azvan Voicu, Joxan Jaffar, Joxan Jaffar
We present a framework for reasoning about programs that incorporates programmer specified assertions and subsumes both Hoare-Logic verification and program analysis. Our aim is to support...
J. LOGIC PROGRAMMING 1994:19, 20:1--679 1 THE SEMANTICS OF CONSTRAINT LOGIC PROGRAMS (2007)
Joxan Jaffar, Michael Maher, Kim Marriott, Peter Stuckey
. 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...
Executable Specifications for Concurrent Programming (2007)
Rafael Ramirez, Joxan Jaffar, Joxan Jaffar
this paper, we use as a basis a new concurrent programming model called Open Constraint Programming. Its roots are in Concurrent Constraint Programming where there is a shared constraint store, and...
A Generic Algorithm for CLP Analysis (2007)
Exte Nd Ed, Extended Abstract, Nevin Heintze, Joxan Jaffar
) Nevin Heintze y and Joxan Jaffar z June 13, 1995 Logic program analyzers typically employ abstract interpretation and consist of two main components: an abstract domain and a generic iterative...
A Decision Procedure for a Class of Set Constraints (Extended Abstract) (2007)
N. Heintze, J. Jaffar, Nevin Heintze, Joxan Jaffar
) Nevin Heintze School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213 (nch@cs.cmu.edu) Joxan Jaffar IBM T.J. Watson Research Center P.O. Box 218 Yorktown Heights, NY 10598...
A Fast Algorithm for Two Processor Scheduling with Release Time and Deadline Constraints (2007)
Scheduling UET (Unit Execution Time) tasks with release time and deadline constraints on two processors was solved by Garey and Johnson. Their algorithm runs in O(n 3) time. In this paper, we propose...
J. LOGIC PROGRAMMING 1994:19, 20:1--679 1 THE SEMANTICS OF CONSTRAINT LOGIC PROGRAMS (2007)
Joxan Jaffar, Michael Maher, Kim Marriott, Peter Stuckey
. 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...
Two Processor Scheduling with Real Release Times and (2007)
Deadlines Hui Wu, Hui Wu, Joxan Jaffar
In a hard real-time system, critical tasks are subject to timing constraints such as release times and deadlines. All timing constraints must be satis ed when tasks are executed. Nevertheless, given...
Scalable Distributed Depth-First Search with Greedy Work Stealing (2007)
Joxan Jaffar, Andrew E. Santosa, Kenny Q. Zhu
We present a framework for the parallelization of depth-first combinatorial search algorithms on a network of computers. Our architecture is based on work stealing and uses a small number of...
A CLP method for compositional and intermittent predicate abstraction (2006)
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
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...
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
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...
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
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...
A CLP method for compositional and intermittent predicate abstraction (2006)
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
joxan,andrews,razvan¡ Abstract. We present an implementation of symbolic reachability analysis with the features of compositionality, and intermittent abstraction, in the sense of pefrorming...
Indexing for dynamic abstract regions (2006)
regions (objects) which may heavily overlap, the RCtree. These objects are “dynamic ” and may have short life spans. The novelty is that rather than representing an object by its minimum bounding...
Modeling Systems in CLP with Coinductive Tabling (2005)
Joxan Jaffar, Andrew E. Santosa, Răzvan Voicu
Abstract. We present a methodology for the modelling of complex program behavior in CLP. The first part of this paper is an informal description about how to represent a system in CLP. At its basic...
A CLP proof method for timed automata (2004)
Joxan Jaffar, Andrew Santosa, Răzvan Voicu
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...
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...
Instruction scheduling with timing constraints on a single risc processor with 0/1 latencies (2000)
We present a fast algorithm for scheduling UET(Unit Execution Time) instructions with precedence constraints in the form of a DAG, latency constraints where the latency between any two instructions...
A Fast Algorithm for Scheduling Instructions with Deadline Constraints on RISC Processors (2000)
Hui Wu, Joxan Jaffar, Krishna Palem
Instruction scheduling is an important issue in the compiler optimization for RISC machines. In this paper, we present a fast approximation algorithm for scheduling instructions of unit execution...
Instruction Scheduling with Timing Constraints on Multiple RISC Processors (2000)
Hui Wu, Joxan Jaffar, Krishna Palem
We present a fast approximation algorithm for scheduling UET(Unit Execution Time) instructions with precedence constraints in the form of a DAG, latency constraints where the latency between any two...
A Calculus for Reactive Databases (2000)
Joxan Jaffar, Limsoon Wong, Roland Yap
Traditionally, interaction with a database is done using a query language like SQL. Such queries apply only to the current state of the database, that is, a query entails computation on a static...
A Framework for Combining Analysis and Verification (2000)
Nevin Heintze, Razvan Voicu, Joxan Jaffar, Joxan Jaffar
interpretation using this domain infers that x0, y0 are even at the end of the loop, although it cannot infer anything about x, y. Combining the results from the Hoare-style reasoner with this...
A Framework for Combining Analysis and Verification (2000)
Nevin Heintze, Joxan Jaffar, Razvan Voicu
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...
Instruction Scheduling with Timing Constraints on a Single RISC Processor with 0/1 Latencies (2000)
Hui Wu, Joxan Jaffar, Roland Yap, Krishna Palem
In this paper, We propose a faster algorithm for the following instruction scheduling problem: Given a set of UET (Unit Execution Time) instructions with precedence constraints in the form of a...
Joxan Jaffar, Michael J. Maher, Gustaf Neumann
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...
Functional Elimination and 0/1/All Constraints (1999)
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...
Joxan Jaffar, Michael J. Maher, Gustaf Neumann
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...
Functional Elimination and 0/1/All Constraints (1999)
Yuanlin Zhang, Joxan Jaffar, Joxan Ja Ar
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...
Open constraint programming (1998)
Joxan Jaffar, Limsoon Wong, H. C. Yap
A new model for high-level concurrent programming is presented. Designed for implementing programs which manipulate and react to shared data which is highly structured, its main elements are: ffl a...
The Semantics Of Constraint Logic Programs (1998)
Joxan Jaffar, Michael Maher, Kim Marriott, Peter Stuckey
This paper presents for the first time the semantic foundations of CLP in a self-contained and complete package. The original presentation of the CLP scheme was in the form of an extended abstract,...
Using Constraints to Model Disjunction in Rule-Based Reasoning (1996)
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...
A Generic Algorithm for CLP Analysis (1995)
Nevin Heintze School, Nevin Heintze, Joxan Jaffar
Logic program analyzers typically employ abstract interpretation and consist of two main components: an abstract domain and a generic iterative fixed-point computation or "engine". In...
Set Constraints and Set-Based Analysis (1994)
This paper contains two main parts. The first examines the set constraint calculus, discusses its history, and overviews the current state of known algorithms and related issues. Here we will also...
Constraint Logic Programming: A Survey (1994)
Joxan Jaffar, Michael J. Maher
Constraint Logic Programming (CLP) is a merger of two declarative paradigms: constraint solving and logic programming. Although a relatively new field, CLP has progressed in several quite different...
Joxan Jaffar, Michael J. Maher, Peter J. Stuckey
Introduction A finite domain constraint system can be viewed as an linear integer constraint system in which each variable has an upper and lower bound. Finite domains have been used successfully in...
Joxan Jaffar, Michael J. Maher, Peter J. Stuckey
Introduction A finite domain constraint system can be viewed as an linear integer constraint system in which each variable has an upper and lower bound. Finite domains have been used successfully in...
Projecting CLP(R ) constraints (1993)
Joxan Jaffar, Michael J. Maher, Peter J. Stuckey
The presentation of constraints in a usable form is an essential aspect of Constraint Logic Programming (CLP) systems. It is needed both in the output of constraints, as well as in the production of...
CLP(R) Programmer's Manual Version 1.1 (1992)
Nevin Heintze Joxan, Joxan Jaffar, Peter Stuckey, Roland Yap
this document; the book by Sterling and Shapiro [13] can serve as a suitable introductory text. Further technical information on CLP(R) is available on language design and implementation [6, 7],...
CLP(R) Programmer's Manual Version 1.2 (1992)
Nevin C. Heintze, Joxan Jaffar, Spiro Michaylov, Peter J. Stuckey, Roland H. C
this document; the book by Sterling and Shapiro [20] can serve as a suitable introductory text. Further technical information on CLP(R) is available on language design and implementation [12, 13],...
An Engine for Logic Program Analysis (1992)
Most logic program analyzers employ a standard approach based on abstract interpretation. At the core of these is a generic algorithm or "engine" which is parameterized by an abstract...
Semantic Types for Logic Programs (1992)
Interpretation: Towards the Global Optimisation of PROLOG Programs", Proceedings 4 th IEEE Symposium on Logic Programming, pp 192 - 204, September 1987. [2] F. G`ecseg and M. Steinby, "Tree...
Semantic Types for Logic Programs (1992)
By Nevin Heintze, Nevin Heintze, Joxan Jaffar
Interpretation: Towards the Global Optimisation of PROLOG Programs", Proceedings 4 th IEEE Symposium on Logic Programming, pp 192 - 204, September 1987. [2] F. G`ecseg and M. Steinby, "Tree...
A Decision Procedure for a Class of Set Constraints (1991)
A set constraint is of the form exp 1 ' exp 2 where exp 1 and exp 2 are set expressions constructed using variables, function symbols, projection symbols, and the set union, intersection and...
Set-Based Program Analysis (Extended Abstract) (1991)
) Nevin Heintze and Joxan Jaffar y 1 January 1991 Summary Program analysis involves approximating the semantics of programs. One important kind of approximation, that of ignoring intervariable...
A Methodology for Managing Hard Constraints in CLP Systems (1991)
In constraint logic programming (CLP) systems, the standard technique for dealing with hard constraints is to delay solving them until additional constraints reduce them to a simpler form. For...
A Finite Presentation Theorem for Approximating Logic Programs (1990)
In program analysis, a key notion used to approximate the meaning of a program is that of ignoring inter-variable dependencies. We formalize this notion in logic programming in order to define an...
A Decision Procedure for a Class of Set Constraints (1990)
Nevin Heintze And, Nevin Heintze, Joxan Jaffar
A set constraint is of the form exp 1 ' exp 2 where exp 1 and exp 2 are set expressions constructed using variables, function symbols, projection symbols, and the set union, intersection and...
A Finite Presentation Theorem for Approximating Logic Programs (Extended Abstract) (1990)
) Nevin Heintze Joxan Jaffar School of Computer Science IBM T.J. Watson Research Center Carnegie Mellon University PO Box 218 Pittsburgh, PA 15213 Yorktown Heights, NY 10598 Summary The notion of...
Most general solutions for trees, multisets and words (1985)
Submitted for the degree of Doctor of Philosophy in the Dept. of Computer Science. Summary: [unpaged] at front of text. Tyescript. Bibliography: leaves 104-107.
Most general solutions for trees, multisets and words (1985)
Submitted for the Degree of Doctor of Philosophy in the Dept. of Computer Science. Summary: [unpaged] at front of text. Microreproduction of original issued: [Clayton, Vic.], 1985. 107 leaves....
Completeness of the negation as failure rule (1983)
Joxan Jaffar, Jean-louis Lassez, John Lloyd
Let P be a Horn clause logic program and comp(p) be its completion in the sense of Clark. Clark gave a justification for the negation as failure rule by showing that if a ground atom A is in the...
Verification decidability of array sorting programs (1981)
Typescript (Photocopy). Bibliography: leaves 83-87.
A Calculus for Reactive Databases
Traditionally, interaction with a database is performed by a query on the current state of the database. Such queries are typically independent of one other; in fact, they are modelled as isolated...
Instruction Scheduling with Timing Constraints on ILP Processors
We present a fast algorithm for scheduling instructions with precedence-latency constraints, timing constraints in the form of individual integer release times and deadlines on an ILP (Instruction...