• Home
• People
• Projects
• Tools
• Publications
  • 2008
  • 2007
  • 2006
  • 2005
  • 2004
  • 2003
  • 2002
  • 2001
  • 2000
• Contact

VLab Publications

2008

• Tevfik Bultan. "Developing Verifiable Concurrent Software." Position paper. CAV 2008 Workshop on Exploiting Concurrency Efficiently and Correctly.
  ps   pdf
• Tevfik Bultan. "Service Choreography and Orchestration with Conversations." Invited abstract. To appear in the Proceedings of the Nineteenth International Conference on Concurrency Theory.
  ps   pdf
• Fang Yu, Chao Wang, Aarti Gupta and Tevfik Bultan. "Modular Verification of Web Services Using Efficient Symbolic Encoding and Summarization." To appear in the Proceedings of the Sixteenth ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE 2008).
• Graham Hughes, Tevfik Bultan and Muath Alkhalaf. "Client and Server Verification for Web Services Using Interface Grammars." To appear in the Proceedings of the Workshop on Testing, Analysis and Verification of Web Software (TAV-WEB 2008).
  ps   pdf
• Graham Hughes and Tevfik Bultan. "Interface Grammars for Modular Software Model Checking." To appear in IEEE Transactions on Software Engineering, special issue on selected papers from the 2007 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2007).
  ps   pdf
• Fang Yu, Tevfik Bultan, Marco Cova, and Oscar H. Ibarra. "Symbolic String Verification: An Automata-based Approach." To appear in the Proceedings of the 15th International SPIN Workshop on Model Checking of Software (SPIN 2008).
  ps   pdf
• Tevfik Bultan and Constance Heitmeyer. "Applying Infinite State Model Checking and Other Analysis Techniques to Tabular Requirements Specifications of Safety-Critical Systems." To appear in Design Automation for Embedded Systems, special issue on selected papers from the Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2006).
  ps   pdf
• Tevfik Bultan and Xiang Fu. "Specification of Realizable Service Conversations Using Collaboration Diagrams." To appear in Service Oriented Computing and Applications.
  ps   pdf

2007

• Jianwen Su, Tevfik Bultan, Xiang Fu, and Xiangpeng Zhao. "Towards a Theory of Web Service Choreographies." Invited paper. To appear in the Proceedings of the 4th International Workshop on Web Services and Formal Methods (WS-FM 2007).
  ps   pdf
• Graham Hughes and Tevfik Bultan. "Extended Interface Grammars for Automated Stub Generation." Proceedings of the Automated Formal Methods Workshop (AFM 2007).
  ps   pdf
• Elliot D. Barlas and Tevfik Bultan. "NetStub: A Framework for Verification of Distributed Java Applications." Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), pp. 24-33, Atlanta, Georgia, November 5-9, 2007.
  ps   pdf
• Fang Yu, Tevfik Bultan and Erik Peterson. "Automated Size Analysis for OCL." Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2007), pp. 331-340, Dubrovnik, Croatia, September 3-7, 2007.
  ps   pdf
• Graham Hughes and Tevfik Bultan. "Automated Verification of XACML Policies Using a SAT Solver." Workshop Proceedings of the 7th International Conference on Web Engineering, Workshop on Web Quality, Verification and Validation (WQVV 2007), pp. 378-392, Como, Italy, July 16-20, 2007.
  ps   pdf
• Graham Hughes and Tevfik Bultan. "Interface Grammars for Modular Software Model Checking." Proceedings of the 2007 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2007), pp. 39-49, London, United Kingdom, July 9-12, 2007.
  ps   pdf
• Tevfik Bultan and Xiang Fu. "Specification of Realizable Service Conversations Using Collaboration Diagrams." Proceedings of the IEEE International Conference on Service-Oriented Computing and Applications (SOCA 2007), pp. 122-130, Newport Beach, California, June 19-20, 2007.
  ps   pdf
• Aysu Betin-Can, Tevfik Bultan, Mikael Lindvall, Benjamin Lux, and Stefan Topp. "Eliminating Synchronization Faults in Air Traffic Control Software via Design for Verification with Concurrency Controllers." Automated Software Engineering special issue on selected papers from the 20th International Conference on Automated Software Engineering (ASE 2005), vol. 14, no. 2, pp. 129-178, June 2007.
  ps   pdf
• Aysu Betin-Can and Tevfik Bultan. "Highly Dependable Concurrent Programming Using Design for Verification." Formal Aspects of Computing, special issue on Verified Software: Theories, Tools, Experiments (VSTTE) Conference, vol. 19, no. 2, pp. 243-268, June 2007.
  ps   pdf
• Mikael Lindvall, Ioana Rus, Paolo Donzelli, Atif Memon, Marvin Zelkowitz, Aysu Betin-Can, Tevfik Bultan, Chris Ackermann, Bettina Anders, Sima Asgari, Victor Basili, Jörg Fellmann, Daniel Hirschbach, Lorin Hochstein, Forrest Shull, Roseanne Tvedt and Daniel Pech. "Experimenting with Software Testbeds for Evaluating New Technologies." Empirical Software Engineering, vol. 12, no. 4, pp. 417-444, August 2007.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Realizability Analysis of Top-down Web Service Composition Specifications." Invited book chapter. To appear in Web Services Research and Practices, Volume 2 of the Advances in Web Services Research (WSR) Series, Liang-Jie Zhang (ed.), Idea Group, Inc., 2007.
  ps   pdf
• Tevfik Bultan, Xiang Fu, and Jianwen Su. "Analyzing Conversations: Realizability, Synchronizability, and Verification." Book chapter. Test and Analysis of Web Services, Luciano Baresi and Elisabetta Di Nitto (eds.), pp. 57-86, Springer, 2007.
  ps   pdf

2006

• Tevfik Bultan. "Modeling Interactions of Web Software." Invited paper. Proceedings of the Second International Workshop on Automated Specification and Verification of Web Systems (WWV 2006), pp. 525-529, November 19, 2006.
  ps   pdf
• Tevfik Bultan and Xiang Fu. "Realizability of Interactions in Collaboration Diagrams." Technical Report 2006-11, Computer Science Department, University of California, Santa Barbara.
  ps   pdf
• Tevfik Bultan and Constance Heitmeyer. "Analyzing Tabular Requirements Specifications Using Infinite State Model Checking." Proceedings of the Fourth ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2006), pp. 7-16, Napa, CA, July 27-29, 2006.
  ps   pdf
• Tevfik Bultan, Xiang Fu, Jianwen Su. "Analyzing Conversations of Web Services." IEEE Internet Computing, vol. 10, no. 1, pp. 18-25, January/February 2006.
  ps   pdf
• Constantinos Bartzis and Tevfik Bultan. "Efficient BDDs for Bounded Arithmetic Constraints." International Journal on Software Tools for Technology Transfer (STTT), special issue on selected papers from the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), vol. 8, no. 1, pp. 26-36, February 2006.
  ps   pdf

2005

• Xiang Fu, Tevfik Bultan, Jianwen Su. "Synchronizability of Conversations among Web Services." IEEE Transactions on Software Engineering, vol. 31, no. 12, pp. 1042-1055, December 2005.
  ps   pdf
• Aysu Betin-Can, Tevfik Bultan, Mikael Lindvall, Benjamin Lux, and Stefan Topp. "Application of Design for Verification with Concurrency Controllers to Air Traffic Control Software." ACM SIGSOFT Distinguished Paper Award, ASE 2005 Best Paper Award. In Proceedings of the 20th IEEE International Conference on Automated Software Engineering (ASE 2005), pp. 14-23, Long Beach, California, USA, November 7-11, 2005.
  ps   pdf
• Tevfik Bultan and Aysu Betin-Can. "Scalable Software Model Checking Using Design for Verification." Proceedings of the IFIP Working Conference on Verified Software: Theories, Tools, Experiments (VSTTE), Bertrand Meyer (ed.), LNCS 4171, Zurich, Switzerland, October 10-14, 2005.
  ps   pdf
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Verification of Parameterized Hierarchical State Machines Using Action Language Verifier." In Proceedings of the Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2005), pp. 79-87, Verona, Italy, July 11-14, 2005.
  ps   pdf
• Tevfik Bultan, Constance Heitmeyer and John O'Leary. "Panel on Design For Verification." Position paper. In Proceedings of the Third ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2005), pp. 233-235, Verona, Italy, July 11-14, 2005.
  ps   pdf
• Aysu Betin-Can and Tevfik Bultan. "Verifiable Web Services with Hierarchical Interfaces." In Proceedings of the 2005 IEEE International Conference on Web Services (ICWS 2005), pp. 85-94, Orlando, Florida, USA, July 11-15, 2005.
  ps   pdf
• Jianwen Su, Tevfik Bultan, Xiang Fu. "Web Service Interactions: Analysis and Design." Invited paper. In Proceedings of the Second International Workshop on Semantic and Dynamic Web Processes (SDWP 2005), pp. 14-19, Orlando, Florida, USA, July 12-15, 2005.
  ps   pdf
• Tuba Yavuz-Kahveci, Constantinos Bartzis, and Tevfik Bultan. "Action Language Verifier, Extended." Tool paper. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV 2005), pp. 413-417, Edinburgh, Scotland, UK, July 6-10, 2005.
  ps   pdf
• Aysu Betin-Can, Tevfik Bultan and Xiang Fu. "Design for Verification for Asynchronously Communicating Web Services." In Proceedings of the Fourteenth International World Wide Web Conference (WWW 2005), pp. 750-759, Chiba, Japan, May 10-14, 2005.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Realizability of Conversation Protocols With Message Contents." International Journal of Web Services Research (JWSR), vol. 2, no. 4, pp. 68-93, 2005. Extended version of the paper selected from the 2004 IEEE International Conference on Web Services (ICWS 2004) and invited for journal publication.
  ps   pdf
• Shriram Krishnamurthi and Tevfik Bultan. "Characteristics of Web Services and Their Impact on Testing, Analysis and Verification." Discussion summary for the Workshop on Testing, Analysis and Verification of Web Services (TAV-WEB) 2004. ACM SIGSOFT Software Engineering Notes, vol. 30, no. 1, January 2005.
  ps   pdf

2004

• Graham Hughes and Tevfik Bultan "Automated Verification of Access Control Policies." Technical report 2004-22, Department of Computer Science, University of California, Santa Barbara, September 2004.
  ps   pdf
• Tevfik Bultan, Xiang Fu, Jianwen Su. "Tools for Automated Verification of Web Services." Invited paper. In Proceedings of the Second International Symposium on Automated Technology on Verification and Analysis (ATVA 2004), Farn Wang (ed.), LNCS 3299, pp. 8-10, Taipei, Taiwan, October 31-November 3, 2004.
  ps   pdf
• Aysu Betin-Can and Tevfik Bultan. "Verifiable Concurrent Programming Using Concurrency Controllers." In Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), pp. 248-257, September 20-25, 2004, Linz, Austria.
  ps   pdf
• Constantinos Bartzis and Tevfik Bultan. "Widening Arithmetic Automata." In Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), Rajeev Alur and Doron Peled (eds.), LNCS 3114, pp. 321-333, Boston, Massachusetts, July 13-17, 2004.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "WSAT: A Tool for Formal Analysis of Web Services." Tool paper. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), Rajeev Alur and Doron Peled (eds.), LNCS 3114, pp. 510-514, Boston, Massachusetts, July 13-17, 2004.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Model Checking XML Manipulating Software." In Proceedings of the 2004 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2004), pp. 252-262, Boston, Massachusetts, July 11-14, 2004.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Realizability of Conversation Protocols With Message Contents." In Proceedings of the 2004 IEEE International Conference on Web Services (ICWS 2004), pp. 96-103, San Diego, California, July 6-9, 2004.
  ps   pdf
• Sandeep K. Shukla, Tevfik Bultan and Constance Heitmeyer. "Panel: Given that Hardware Verification has been an Uphill Battle, What is the Future of Software Verification?" Position paper. In Proceedings of the Second ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2004), pp. 157-158, San Diego , California , June 22-25, 2004.
  ps   pdf
• Xiang Fu, Tevfik Bultan and Jianwen Su. "Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services." Theoretical Computer Science (TCS), special issue on selected papers from the 8th International Conference on Implementation and Application of Automata (CIAA 2003), vol. 328, no. 1-2, pp. 19-37, November 2004.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Analysis of Interacting BPEL Web Services." In Proceedings of the Thirteenth International World Wide Web Conference (WWW 2004), pp. 621-630, New York, NY, May 17-22, 2004.
  ps   pdf
• Zhe Dang, Tevfik Bultan, Oscar H. Ibarra, and Richard A. Kemmerer. "Past Pushdown Timed Automata and Safety Verification." Theoretical Computer Science (TCS), special issue on selected papers from the 6th International Conference on Implementation and Application of Automata (CIAA 2001), vol. 313, no. 1, pp. 57-71, February 2004.
  ps   pdf

2003

• Tevfik Bultan. "Software Design From a Verification Perspective." Position paper. National Science Foundation Workshop, Science of Design: Software and Software-Intensive Systems, Airlie Center, Herndon, Virginia, November 2-4, 2003.
  ps   pdf
• Tuba Yavuz-Kahveci and Tevfik Bultan. "A Symbolic Manipulator for Automated Verification of Reactive Systems with Heterogeneous Data Types." International Journal on Software Tools for Technology Transfer (STTT), special issue on selected papers from the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Software Systems (TACAS 2001), vol. 5, no. 1, pp. 15-33, November 2003.
  ps   pdf
• Constantinos Bartzis and Tevfik Bultan. "Efficient Symbolic Representations for Arithmetic Constraints in Verification." International Journal of Foundations of Computer Science (IJFCS), special issue on Verification and Analysis of Infinite State Systems, vol. 14, no. 4, pp. 605-624, August 2003.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "A Top-Down Approach to Modeling Global Behaviors of Web Services." In Proceedings of the Requirements Engineering for Open Systems Workshop (REOS 2003), Monterey, California, September 8, 2003.
  ps   pdf
• Aysu Betin-Can and Tevfik Bultan. "Interface-Based Specification and Verification of Concurrency Controllers." In Proceedings of the Workshop on Software Model Checking (SoftMC 2003), Electronic Notes in Theoretical Computer Science (ENTCS), vol. 89, no. 3. Boulder, Colarado, July 14, 2003.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Conversation Protocols: A Formalism for Specification and Verification of Reactive Electronic Services." In Proceedings of the Eighth International Conference on Implementation and Application of Automata (CIAA 2003). Oscar H. Ibarra and Zhe Dang, eds., LNCS 2759, pp. 188-200, Springer, Santa Barbara, California, July 16-18, 2003.
  ps   pdf
• Constantinos Bartzis and Tevfik Bultan. "Efficient Image Computation in Infinite State Model Checking." In Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003). Warren A. Hunt, Jr. and Fabio Somenzi, eds., LNCS 2725, pp. 249-261, Springer, Boulder, Colarado, July 8-12, 2003.
  ps   pdf
• Tevfik Bultan, Xiang Fu, Richard Hull, and Jianwen Su. "Conversation Specification: A New Approach to Design and Analysis of E-Service Composition." In Proceedings of the Twelfth International World Wide Web Conference (WWW 2003), pp. 403-410, Budapest, Hungary, May 20-24, 2003.
  ps   pdf
• Constantinos Bartzis and Tevfik Bultan. "Construction of Efficient BDDs for Bounded Arithmetic Constraints." In Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), Hubert Garavel and John Hatcliff, eds., LNCS 2619, pp. 394-408, Springer, Warsaw, Poland, April 7-11, 2003.
  ps   pdf

2002

• Tuba Yavuz-Kahveci and Tevfik Bultan. "Automated Verification of Concurrent Linked Lists with Counters." In Proceedings of the 9th International Static Analysis Symposium (SAS 2002). M. V. Hermenegildo, G. Pueble eds., LNCS 2477, pp. 69-84, Springer, Madrid, Spain, September 17-20, 2002.
  ps   pdf
• Constantinos Bartzis and Tevfik Bultan. "Automata-Based Representations for Arithmetic Constraints in Automated Verification." In Proceedings of the Seventh International Conference on Implementation and Application of Automata (CIAA 2002). Jean-Marc Champarnaud and Denis Maurel, eds., LNCS 2608, pp. 282-288, Tours, France, July 3-5, 2002.
  ps   pdf
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Formal Verification of E-Services and Workflows." In Proceedings of the Workshop on Web Services, e-Business, and the Semantic Web: Foundations, Models, Architecture, Engineering and Applications (WES 2002). C. Bussler, R. Hull, S. McIlraith, M.E. Orlowska, B. Pernici, and J. Yang, eds., LNCS 2512, pp. 188-202, Springer, Toronto, Canada, May 27-28, 2002.
  ps   pdf
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Specification, Verification, and Synthesis of Concurrency Control Components." In Proceedings of the 2002 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2002), pp. 169-179, Rome, Italy, July 22-24, 2002.
  ps   pdf
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Heuristics for Efficient Manipulation of Composite Constraints." In Proceedings of the 4th International Workshop on Frontiers of Combining Systems (FroCoS 2002), Alessandro Armando, ed., LNAI 2309, pp. 57-71, Springer, Santa Margherita Ligure, Italy, April 8-10, 2002.
  ps   pdf
• Oscar H. Ibarra, Jianwen Su, Zhe Dang, Tevfik Bultan, and Richard A. Kemmerer. "Counter Machines and Verification Problems." Theoretical Computer Science (TCS), vol. 289, no. 1, pp. 165-189, October 2002.
  ps   pdf

2001

• Giorgio Delzanno and Tevfik Bultan. "Constraint-based Verification of Client-Server Protocols." In Proceedings of the Seventh International Conference on Principles and Practice of Constraint Programming (CP 2001), T. Walsh ed., LNCS 2239, pp. 286-301, Springer, Paphos, Cyprus, November 26-December 1, 2001.
  ps   pdf
• Tevfik Bultan and Tuba Yavuz-Kahveci. "Action Language Verifier." Short paper. In Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), pp. 382-386, Coronado Island, California, November 26-29, 2001.
  ps   pdf
• Tuba Yavuz-Kahveci, Murat Tuncer, and Tevfik Bultan. "A Library for Composite Symbolic Representations." In Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), Tiziana Margaria and Wang Yi, eds., LNCS 2031, pp. 52-66, Springer, Genova, Italy, April 2-6, 2001.
  ps   pdf
• Xiang Fu, Tevfik Bultan, Richard Hull, and Jianwen Su. "Verification of Vortex Workflows." In Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), Tiziana Margaria and Wang Yi, eds., LNCS 2031, pp. 143-157, Springer, Genova, Italy, April 2-6, 2001.
  ps   pdf
• Zhe Dang, Tevfik Bultan, Oscar H. Ibarra, and Richard A. Kemmerer. "Past Pushdown Timed Automata." In Proceedings of the Sixth International Conference on Implementation and Application of Automata (CIAA 2001). Bruce W. Watson and Derick Wood, eds., LNCS 2494, pp. 74-86, CIAA 2001, Pretoria, South Africa, July 23-25, 2001.
  ps   pdf
• Oscar H. Ibarra, Tevfik Bultan, and Jianwen Su. "On Reachability and Safety in Infinite-State Systems." International Journal of Foundations of Computer Science (IJFCS), vol. 12, no. 6, pp. 821-836, December 2001.
  ps   pdf

2000

• Tevfik Bultan, Richard Gerber and Christopher League. "Composite Model Checking: Verification with Type-Specific Symbolic Representations." ACM Transactions on Software Engineering and Methodology (TOSEM), special issue on selected papers from the 1998 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 1998), vol. 9, no. 1, pp. 3-50, January 2000.
  ps   pdf
• Tevfik Bultan. "Action Language: A Specification Language for Model Checking Reactive Systems." In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), pp. 335-344, University of Limerick, Ireland, June 4-11, 2000.
  ps   pdf
• Tevfik Bultan. "A Composite Model Checking Toolset for Analyzing Software Systems." Project summary. ACM SIGSOFT Software Engineering Notes, vol. 25, no. 1, pp. 37-38, January 2000.
  ps   pdf
• Tevfik Bultan. "BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems." In Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000). Susanne Graf and Michael Schwartzbach, eds., LNCS 1785, pp. 441-455, Springer, Berlin, Germany, March 25-April 2, 2000.
  ps   pdf
• Oscar H. Ibarra, Tevfik Bultan, and Jianwen Su. "Reachability Analysis for Some Models of Infinite-State Transition Systems." In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000), Catuscia Palamidessi, ed., LNCS 1877, pp. 183-198, Springer, University Park, PA, August 22-25, 2000.
  ps   pdf
• Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, and Jianwen Su. "Binary Reachability Analysis of Discrete Pushdown Timed Automata." In Proceedings of the 12th International Conference on Computer Aided Verification (CAV 2000), E. Allen Emerson and A. Prasad Sistla, eds., LNCS 1855, pp. 69-84, Springer, Chicago, IL, July 15-19, 2000.
  ps   pdf
• Oscar H. Ibarra, Jianwen Su, Zhe Dang, Tevfik Bultan, and Richard A. Kemmerer. "Counter Machines: Decidable Properties and Applications to Verification Problems." In Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science (MFCS 2000), M. Nielsen and B. Rovan eds., LNCS 1893, Springer, pp. 426-435, Bratislava, Slovak Republic, August 28-September 1, 2000.
  ps   pdf