Publication see also Zijiang Yang's DBLP Entry

Journal/Conference/Workshop Papers

2009

1. [LNK][BIB] Dongyoon Lee, Satish Narayanasamy, Mahmoud Said, Zijiang Yang, Offline Symblolic Analysis for Multi-Processor Replay. The 42nd IEEE/ACM International Symposium on Microarchitecure (Micro-42),  December 12-16, New York, NY, USA. To Appear.
2. [LNK][BIB] Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic, Model Checking Sequential Software Programs Via Mixed Symbolic Analysis. ACM Transactions on Design Automation of Electronic Systems (TODAES), Volume 14, Issue 1, January, 2009, ACM.
3. [LNK][BIB] Qichang Chen, Liqiang Wang, Zijiang Yang, and Scott D. Stoller. HAVE: Integrated Dynamic and Static Analysis for Atomicity Violations. International Conference on Fundamental Approaches to Software Engineering (FASE), European Joint Conferences on Theory and Practice of Software (ETAPS). York, UK. Springer-Verlag, 2009. 
4. [LNK][BIB] Z. Yang, B. Al-Rawi, K. Sakallah, X. Huang, S.A. Smolka and R. Grosu. Dynamic Path Reduction for Software Model Checking. The 7th International Conference on Integrated Formal Methods, Duesseldorf, Germany, February 2009, Springer, LNCS.
5. [LNK][BIB] Qichang Chen, Liqiang Wang, Zijiang Yang. A Combined Static and Dynamic Approach for Escape Analysis. 33rd Annual IEEE International Computer Software and Applications Conference (COMPSAC) . Seattle,Washington. IEEE Press, 2009. 

1. [LNK][BIB] Aleksandr Zaks, Zijiang Yang, Ilya Shlyakhter, Franjo Ivancic, Srihari Cadambi, Malay K. Ganai, Aarti Gupta, and Pranav Ashar, Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking,  IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD),  Volume 27(8), August 2008, IEEE.
2. [LNK][BIB] Franjo Ivancic, Zijiang Yang, Malay Ganai, Aarti Gupta, and Pranav Ashar, Efficient SAT-based Bounded Model Checking for Software Verification,  Theoretical Computer Science (TCS), Volume 404(3), September 2008,  Elsevier. 
3. [LNK][BIB] Zijiang Yang and Karem Sakallah, SMT-based Symbolic Model Checking for Multi-Threaded Programs,  Exploiting Concurrency Efficiently and Correctly Workshop, Princeton, NJ, July 2008.
4. [LNK][BIB] Chao Wang, Zijiang Yang and Aarti Gupta, Peephole Partial Order Reduction , 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, Hungary, April 2008. 

2007

1. [LNK][BIB] Formal Modelling and Analysis of Scientific Workflows Using Hierarchical State Machines, 2nd International Workshop on Scientific Workflows and Business Workflow Standards in e-Science, held in conjuction with IEEE international conference on e-science and grid computing, (with P. Yang, Z. and S. Lu), 2007. To Appear.
2. [LNK][BIB] Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra.  19th International Conference on  Computer Aided Verification (CAV), (with Chao Wang, Aarti Gupta, and Franjo Ivancic),  Berlin, Germany, July 3-7, 2007.  
3. [LNK][BIB] Disjunctive Image Computation for Software Verification.  ACM Transactions on Design Automation of Electronic Systems (TODAES),  (with Chao Wang, Franjo Ivancic, and Aarti Gupta), volume 12(2), April 2007, article 10, ACM. ACM TODAES 2008 Best Paper Award.
4. [LNK][BIB] Model Checking Approach to Itinerary-based Access Control Enforcement of Mobile Tasks in Scientific Workflows, Journal of Autonomic and Trusted Computing, (with S. Lu and P. Yang), 2007. To Appear.
   
5. [LNK][BIB] Itinerary-Based Access Control for Mobile Tasks in Scientific Workflows,   The 2007 IEEE International Symposium on Ubisafe Computing (UbiSafe-07), (with Shiyong Lu and Ping Yang), Niagara Falls, Ontario, Canada, May 21-23, 2007. 
6. [LNK][BIB] Opportunistic Networks for Emergency Applications and Their Standard Implementation Framework, The First International Workshop on Next Generation Networks for First Responders and Critical Infrastructure (NetCri07), (with Leszek Lilien, Ajay Gupta), New Orleans, Louisiana, April 11-13, 2007. 

1. [LNK][BIB] Whodunit? Causal Analysis for Counterexamples. Fourth international symposium on Automated Technology for Verification and Analysis (ATVA'06), (with Chao Wang, Aarti Gupta, and Franjo Ivancic), Beijing, China, 2006. 
2. [LNK][BIB] Efficient Distributed SAT and SAT-based Distributed Bounded Model Checking. International Journal on Software Tools for Technology Transfer (STTT), (with Malay Ganai, Aarti Gupta, and Pranav Ashar), Volume 8, Numbers 4-5, August 2006, Springer. 
3. [LNK][BIB] Mixed Symbolic Representations for Model Checking Software Programs, ACM/IEEE International Conference on Formal Methods and Models for Codesign (Memocode'06),  (with Chao Wang, Aarti Gupta, and Franjo Ivancic), Napa, California, USA, 2006. 
   
4. [LNK][BIB] Runtime Security Verification for Itinerary-Driven Mobile Code,  IEEE International Symposium on Dependable, Autonomic and Secure Computing (DASC'06), (with Shiyong Lu, and Ping Yang),  Indiana University, Purdue University, Indianapolis, USA, 2006. 
5. [LNK][BIB] Using Range Analysis for Software Verification,  4th International Workshop on Software Verification and Validation(SVV'06), (with Aleks Zaks, Ilya Shlyakhter, Franjo Ivancic, Srihari Cadambi, Malay Ganai, Aarti Gupta and Pranav Ashar), Seattle, USA, 2006. 
   
6. [LNK][BIB] Disjunctive Image Computation for Embedded Software Verification,  Design, Automation and Test in Europe (DATE'06), (with C. Wang, F. Ivancic, and A. Gupta), Munich, Germany. March 2006. 
7. [LNK][BIB] PDC: Pattern Discovery with Confidence in DNA Sequences, IASTED International Conference on Advances in Computer Science and Technology, (with Y. Lu, S. Lu, F. Fotouhi, Y. Sun and L. Liang), Puerto Vallarta, Mexico, 2006.

1. [LNK][BIB] Model Checking C Programs Using F-Soft, invited paper, IEEE International Conference on Computer Design (ICCD), (withF. Ivancic, I. Shlyakhter, A. Gupta, M. K. Ganai, V. Kahlon, C. Wang), 2005.
2. [LNK][BIB] F-Soft: Software Verification Platform, 17th International Conference on Computer-Aided Verification(CAV), (with F.Ivancic,M. Ganai, A. Gupta, I. Shlyakhter and P.Ashar), 2005.

1. [LNK][BIB] Using Routing Data for Information Authentication in Sensor Networks, 3rd International Trusted Internet Workshop, (with V. Bhuse, A. Gupta, M. Terwilliger, and Z. Kamal), 2004.
2. [LNK][BIB] Efficient SAT-based Bounded Model Checking for Software Verification,  1st International Symposium on Leveraging Applications of Formal Methods (ISoLA),(with P.Ashar, M. Ganai, A. Gupta, and F.Ivancic), 2004.
3. [LNK][BIB] Variable Reuse for Efficient Image Computation,  5th International Conference on Formal Methods in Computer-Aided Design (FMCAD),(with R.Alur), 2004.
4. [LNK][BIB] Execution of a Requirement Model in Software Development, ISCA 13th International Conference on Intelligent & Adaptive Systems and Software Engineering (IASSE),(with W.Shen,  M.Guizani, K. Compton and J. Huggins),2004.

1. [LNK][BIB] Iterative Abstraction using SAT-based BMC with Resolution, International Conference on Computer Aided Design(ICCAD), (with A. Gupta, M. Ganai, and P. Ashar), 2003.     
2. [LNK][BIB] Abstraction and BDDs Complement SAT-Based BMC in DiVer, 15th International Conference on Computer-Aided Verification(CAV), (with A. Gupta, M. Ganai, C. Wang and P. Ashar), 2003.     
3. [LNK][BIB] Efficient Distributed SAT and SAT-based Distributed Bounded Model Checking, 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods(CHARME), (with M. Ganai, A. Gupta and P. Ashar), 2003.
4. [LNK][BIB] Learning from BDDs in SAT-based Bounded Model Checking, 40th Design Automation Conference(DAC), (with A. Gupta, C. Wang, M. Ganai, and P. Ashar) ,2003.

1. [LNK][BIB] Exploiting Behavioral Hierarchy for Efficient Model Checking, 14th International Conference on Computer-Aided Verification(CAV), (with R. Alur and M. McDougall), 2002.

1. [LNK][BIB] Partition-Based Decision Heuristics for Image Computation Using SAT and BDDs, International Conference on Computer Aided Design(ICCAD), (with A. Gupta, P. Ashar, L. Zhang and S. Malik), 2001. 
2. [LNK][BIB] Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation, 38th Design Automation Conference(DAC), (with A. Gupta, A. Gupta, and P. Ashar), 2001. 
3. [LNK][BIB] Is There a Best Symbolic Cycle-Detection Algorithm? Tools and Algorithms for the Construction and Analysis of Systems (TACAS), (with K. Fisler, R. Fraer, G. Kamhi and M. Vardi), 2001.

1. [LNK][BIB] SAT Based State Reachability Analysis and Model Checking, 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD), (with A. Gupta, A. Gupta and P. Ashar), 2000.