Joxan Jaffar

Research Page -- May 2017

Recent Work

Local Reasoning on Recursive Data Structures, Chu Duc Hiep and Joxan Jaffar, draft ( abstract , pdf )

Chu Duc Hiep, Joxan Jaffar and Andrew Santosa, Bounded Verification and Testing of Heap Programs, draft ( abstract , pdf )

Invited talk, Workshop on Horn Clauses for Verification and Synthesis, CAV, July 2015, Slides

A Shape Neutral Analysis for Graph Data-structures, G. Duck, J. Jaffar and R. Yap, draft ( abstract , pdf )

Joxan Jaffar and Vijayaraghavan Murali, Trace Generalization via Loop Compression, draft ( abstract , pdf )

Selected Publications 1990 --

Minh-Thai Trinh, Chu Duc Hiep and Joxan Jaffar, Model Counting for Recursively-Defined Strings CAV 2017 ( abstract , pdf )

Symbolic Execution for Memory Consumption Analysis Chu Duc Hiep, Joxan Jaffar and Rasool Maghareh, LCTES 2016 ( abstract , pdf )

Minh-Thai Trinh, Chu Duc Hiep and Joxan Jaffar, Progressive Reasoning over Recursively-Defined Strings CAV 2016 ( abstract , pdf )

Precise Cache Timing Analysis via Symbolic Simulation, Chu Duc Hiep, Joxan Jaffar and Rasool Maghareh, RTAS 2016 ( abstract , pdf )

Chu Duc Hiep Joxan Jaffar, and Minh-Thai Trinh Automatic Induction Proofs of Data-Structures in Imperative Programs, PLDI 2015 ( abstract , pdf )

Chu Duc Hiep and Joxan Jaffar, A Framework to Synergize Partial Order Reduction with State Interpolation, Haifa Verification Conference, 2014 ( abstract , pdf )

Minh-Thai Trinh, Chu Duc Hiep and Joxan Jaffar, S3: A Symbolic String Solver for Vulnerability Detection in Web Applications, ACM-CCS 2014 ( abstract , pdf )

Joxan Jaffar and Vijayaraghavan Murali, A Path-Sensitively Sliced Control Flow Graph, FSE'2014 ( abstract , pdf )

Chu Duc Hiep, Joxan Jaffar and Vijayaraghavan Murali, Lazy Symbolic Execution and Enhanced Learning, Runtime Verification, 2014 ( abstract , pdf )

Joxan Jaffar, Vijayaraghavan Murali and Jorge Navas, Boosting Concolic Testing with Interpolation, FSE 2013 ( abstract , pdf )

Chu Duc Hiep and Joxan Jaffar, Path-Sensitive Resource Analysis Compliant with Assertions, EMSOFT 2013 ( abstract , pdf )

Gregory Duck, Joxan Jaffar and Nicolas Koh, A Constraint Solver for Heaps with Separation, CP 2013 ( abstract , pdf )

Joxan Jaffar, Vijayaraghavan Murali, Jorge Navas and Andrew Santosa, TRACER: A Symbolic Execution Tool for Verification, CAV'2012 ( abstract , pdf )

Xiao Jia, Kenny Q. Zhu, J. Jaffar and R. Yap, A Runtime System for Generalized Committed Choice, 2012 Asia-Pacific Programming Languages and Compilers Workshop, 2012

Chu Duc Hiep and Joxan Jaffar, A Complete Method for Symmetry Reduction in Safety Verification, CAV'2012 ( abstract , pdf )

Joxan Jaffar, Vijayaraghavan Murali, Jorge Navas and Andrew Santosa, Path Sensitive Backward Slicing, SAS'2012 ( abstract , pdf )

Joxan Jaffar, Jorge Navas and Andrew Santosa, Unbounded Symbolic Execution for Program Verification, draft ( abstract , pdf ), RV'2011

Chu Duc Hiep and Joxan Jaffar, Symbolic Simulation on Complicated Loops for WCET Path Analysis, draft ( abstract , pdf ), EMSOFT'2011

Joxan Jaffar and Andrew Santosa, Recursive Abstractions for Parameterized Systems, FM'09, ( abstract , pdf )

Joxan Jaffar, Andrew Santosa and Razvan Voicu, An Interpolation Method for CLP traversal, CP'09 ( abstract , pdf )

Joxan Jaffar, Andrew Santosa and Razvan Voicu, Efficient Memoization for Dynamic Programming with Adhoc Constraints, AAAI'08, ( abstract , pdf )

Joxan Jaffar, Andrew Santosa and Razvan Voicu, A Coinduction Rule for Entailment of Recursively Defined Properties, CP'08, ( abstract , pdf )

Joxan Jaffar, Roland Yap and Kenny Zhu, "Generalized Committed Choice", Coordination'07, ( abstract , pdf )

Hui Wu and Joxan Jaffar and Jingling Xue, Instruction Scheduling with Release Times and Deadlines on ILP Processors, Proc 12th IEEE Intl Conf on Embedded and Real-Time Computing Systems and Applications, 51-60, 2006.

Joxan Jaffar, Andrew Santosa and Razvan Voicu, Relative Safety, Proc. 7th Intl Conf on Verification, Model Checking and Abstract Interpretation (VMCAI), Charleston, South Carolina, January 8-10, 2006, LNCS 3855 pp 282-297. ( abstract , pdf ).

Joxan Jaffar, Roland H.C. Yap and Kenny Q.Zhu, Indexing for Dynamic Abstract Regions, Proceedings of the IEEE Intl Conference on Data Engineering (ICDE), Atlanta, April 2006. ( abstract , pdf ).

Joxan Jaffar, Andrew Santosa and Razvan Voicu, A CLP Method for Compositional and Intermittent Abstraction, Proc. 7th Intl Conf on Verification, Model Checking and Abstract Interpretation (VMCAI), Charleston, South Carolina, January 8-10, 2006, LNCS 3855 pp 17-32. ( abstract , pdf ).

Joxan Jaffar, Roland H.C. Yap and Kenny Q.Zhu, Coordination of Many Agents, Proceedings of the 21st Intl Conference on Logic Programming (ICLP), October 2005, LNCS, pp 98-112. ( abstract , pdf )

Joxan Jaffar, Andrew Santosa and Razvan Voicu, "Modeling Systems in CLP with Coinductive Tabling", Proceedings of the 21st Intl Conference on Logic Programming (ICLP), poster, LNCS 2668 pp 412-413. ( abstract , long-version pdf )

Joxan Jaffar, Andrew Santosa and Razvan Voicu, A CLP Proof Method for Timed Automata, 25th IEEE Real-Time Systems Symposium (RTSS), Dec 2004, Lisbon, 175-186, IEEE Computer Society Press. ( abstract , ps )

Hui Wu and Joxan Jaffar, A Fast Algorithm for Two Processor Scheduling with Release Times and Deadlines, SIAM Journal on Computing, To appear.

Hui Wu and Joxan Jaffar, Two Processor Scheduling with Real Release Times and Deadlines, Symposium on Parallel Algorithms and Architectures (SPAA), 11-13 August 2002, Manitoba, Canada.

Hui Wu and Joxan Jaffar, An Efficient Algorithm for Scheduling Instructions with Deadline Constraints on ILP Processors, 22nd IEEE Real-Time Systems Symposium (RTSS), December 3-6, 2001, London, UK.

Wu Hui, Joxan Jaffar and Roland Yap, "Instruction Scheduling with Timing Constraints on Single RISC Processor with 0/1 Latencies", Sixth Int Conf on Principles and Practice of Constraint Programming (CP), pp 457-469, 2000.

Wu Hui, Chin W.N. and Joxan Jaffar, "An Optimal Distributed Deadlock Avoidance Algorithm for AND Model", IEEE Transactions on Software Engineering, Vol. 28, No. 1, Jan 2002.

Nevin Heintze, Joxan Jaffar and Razvan Voicu, "A Framework for Analysis and Verification", Proceedings SIGACT/SIGPLAN Symp on Principles of Programming Languages (POPL), Jan 2000, pp 26-39. ( postscript )

Hui Wu, Joxan Jaffar and R. Yap, A Fast Algorithm for Scheduling Instructions with Deadline Constraints on RISC Processors, Int Conf on Parallel Architectures and Compilation Teachniques (PACT), Philadelphia, PA, pp 281-290, 2000.

Zhang Yuanlin, Roland Yap and Joxan Jaffar, Functional Elimination and 0/1/All Constraints, Proceedings of 16th National Conference on Artificial Intelligence (AAAI), pp 175-180, July 1999, Orlando, FL: AAAI Press/The MIT Press. ( postscript )

Joxan Jaffar and Roland Yap, "Open Constraint Programming", Invited Paper, 4th Intl. Conf on Principles and Practice of Constraint Programming (CP), Pisa, Oct 1998.

Joxan Jaffar, M. Maher, K. Marriott and P. Stuckey, "Semantics of Constraint Logic Programming", Journal of Logic Programming, 37(1), 1-46, 1998.

Alex Brodsky, Joxan Jaffar and Michael Maher, "Toward Practical Query Evaluation for Constraint Databases", The Constraints Journal, 2(3), Dec 1997, 279-304.

Joxan Jaffar and Roland Yap, CP'2000: A Position Paper, ACM Workshop on Strategic Directions in Computing Research, Washington, Aug 1996 (and Constraints Journal 2(1): 71-73, April 1997).

Liu Bing and Joxan Jaffar, ``Using Constraints to Model Disjunctions in Rule Based Programming'', AAAI-96. ( postscript )

Joxan Jaffar, Michael Maher and Gustaf Neumann, ``Logic Programming and Object Modelling: a Case Study'', Proceedings Intl. Logic Programming Symposium (ILPS), Invited Paper, Portland, Oregon, MIT Press, December 1995.

Nevin Heintze and Joxan Jaffar, ``An Generic Algorithm for CLP Analysis'', Proceedings Fifth Intl. Conf. on Logic Programming (ICLP), Tokyo, MIT Press, June 1995. ( postscript )

J.Jaffar and M.Maher, ``Constraint Logic Programming: a Survey'', Journal of Logic Programming, Special 10th Anniversary Issue, Vols 19/20, May/July 1994. Also in Handbook of Artificial Intelligence and Logic Programming, Oxford Univ. Press, 1995.

J.Jaffar, M.Maher, P.Stuckey and R.Yap, ``Projecting CLP(R) Constraints'', New Generation Computing, 11 (3 & 4), 1993.

Alexander Brodsky, Joxan Jaffar and Michael Maher, ``Toward Practical Constraint Databases'', Proc. 19th Conf. on Very Large Data Bases (VLDB), Dublin, July 1993.

J. Jaffar, S. Michaylov, P. Stuckey and R. Yap, ``The CLP(R) Language and System'', ACM Transactions on Programming Languages and Systems, 14(3), July 1992.

Nevin Heintze and Joxan Jaffar, ``An Engine for Logic Program Analysis'', Proceedings Fifth IEEE Symposium on Logic in Computer Science (LICS), Santa Cruz, June 1992, pp 42-51.

J. Jaffar, S. Michaylov, P. Stuckey and R. Yap, ``An Abstract Machine for CLP(R)'', Proceedings SIGPLAN'92 Conf. on Programming Language Design & Implementation (PLDI), San Francisco, 1992.

Nevin Heintze and Joxan Jaffar, ``Semantic Types for Logic Programs'', in Types in Logic Programming, F. Pfenning (Ed), MIT Press, June 1992, pp 141-155.

J.Jaffar, S.Michaylov and R.Yap, ``A Methodology for Managing Hard Constraints in CLP Systems'', Proceedings SIGPLAN'91 Conf. on Programming Language Design & Implementation (PLDI), June 1991, pp 306--316.

N. Heintze and J. Jaffar, ``A Finite Presentation Theorem for Approximating Logic Programs'', Proceedings 17th ACM Symposium on Principles of Programming Langauges (POPL), San Francisco, 1990.

N. Heintze and J. Jaffar, ``A Decision Procedure for a Class of Herbrand Set Constraints'', Proceedings 5th IEEE Symp. on Logic in Computer Science (LICS), Philadelphia, June 1990.

Joxan Jaffar, ``Minimal and Complete Unification'', Journal of the ACM, 37(1), January 1990, pp 47-85.