VLab Publications

2022

• Seemanta Saha, Mara Downing, Tegan Brennan, and Tevfik Bultan. "PReach: A Heuristic for Probabilistic Reachability to Identify Hard to Reach Statements." Proceedings of the 44th International Conference on Software Engineering (ICSE 2022).
• William Eiers, Ganesh Sankaran, Albert Li, Emily O'Mahony, Benjamin Prince, Tevfik Bultan. "Quantifying Permissiveness of Access Control Policies." Proceedings of the 44th International Conference on Software Engineering (ICSE 2022).

2021

• Chaofan Shou, Ismet Burak Kadron, Qi Su, Tevfik Bultan. "CorbFuzz: Checking Browser Security Policies with Fuzzing." Proceedings of the the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE 2021).

2020

• Tegan Brennan, Seemanta Saha, and Tevfik Bultan. "JVM Fuzzing for JIT-Induced Side-Channel Detection." Proceedings of the 42nd International Conference on Software Engineering (ICSE 2020).
• Tegan Brennan, Nicolás Rosner, and Tevfik Bultan. "JIT Leaks: Inducing Timing Side Channels Through Just-In-Time Compilation." Proceedings of the 41st IEEE Symposium on Security and Privacy (Security and Privacy 2020).
• Ismet Burak Kadron, Nicolás Rosner, Tevfik Bultan. "Feedback-Driven Side-Channel Analysis for Networked Applications." Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2020).

2019

• William Eiers, Seemanta Saha, Tegan Brennan, Tevfik Bultan. "Subformula Caching for Model Counting and Quantitative Program Analysis." Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE 2019)
• Seemanta Saha, William Eiers, Ismet Burak Kadron, Lucas Bang, Tevfik Bultan. "Incremental Attack Synthesis." Java Pathfinder Workshop 2019.
• Nicolás Rosner, Ismet Burak Kadron, Lucas Bang, and Tevfik Bultan. "Profit: Detecting and Quantifying Side Channels in Networked Applications." Proceedings of the Network and Distributed System Security Symposium (NDSS 2019).

2018

• Abdulbaki Aydin, William Eiers, Lucas Bang, Tegan Brennan, Miroslav Gavrilov, Tevfik Bultan, Fang Yu. "Parameterized Model Counting for String and Numeric Constraints." Proceedings of the 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE '18)
• Seemanta Saha, Ismet Burak Kadron, William Eiers, Lucas Bang, Tevfik Bultan. "Attack Synthesis for Strings using Meta-Heuristics." Java Pathfinder Workshop 2018.
• Tegan Brennan, Seemanta Saha, Tevfik Bultan, and Corina Pasareanu. "Symbolic Path Cost Analysis for Side-Channel Detection." Proceedings of the 2018 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2018).
• Lucas Bang, Nicolas Rosner, and Tevfik Bultan. "Online Synthesis of Adaptive Side-Channel Attacks Based On Noisy Observations." Proceedings of the IEEE European Symposium on Security and Privacy (EuroS&P 2018).

2017

• Tevfik Bultan, Fang Yu, Muath Alkhalaf, Abdulbaki Aydin. "String Analysis for Software Verification and Security." Springer 2017, ISBN 978-3-319-68668-4.
• Tegan Brennan, Nestan Tsiskaridze, Nicolás Rosner, Abdulbaki Aydın and Tevfik Bultan. "Constraint Normalization and Parameterized Caching for Quantitative Program Analysis." Proceedings of the 11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineerins (ESEC/FSE 2017)
• Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria, and Tevfik Bultan. "Synthesis of Adaptive Side-Channel Attacks." To appear in the Proceedings of the 2017 IEEE Computer Security Foundations Symposium (CSF 2017).
• Ivan Bocic and Tevfik Bultan. "Symbolic Model Extraction for Web Application Verification." Proceedings of the 39th International Conference on Software Engineering (ICSE 2017).

2016

• Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, and Tevfik Bultan. "String Analysis for Side Channels with Segmented Oracles." To appear in the Proceedings of the 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016).
• Ivan Bocic and Tevfik Bultan. "Finding Access Control Bugs in Web Applications with CanCheck." To appear in the Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering (ASE 2016).
• Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Bow-Yaw Wang and Tevfik Bultan. "Optimal Sanitization Synthesis for Web Application Vulnerability Repair." To appear in the Proceedings of the 2016 International Symposium on Software Testing and Analysis (ISSTA 2016).
• Samik Basu and Tevfik Bultan. "Automated Choreography Repair" Proceedings of the, 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016). pages 13-30, Eindhoven, The Netherlands, April 2-8, 2016.
• Samik Basu and Tevfik Bultan. "On Deciding Synchronizability for Asynchronously Communicating Systems." Accepted for publication in Theoretical Computer Science (TCS).

2015

• Ivan Bocic and Tevfik Bultan. "Efficient Data Model Verification with Many-Sorted Logic." Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015) pages 42-52, November 9–13, 2015, Lincoln, Nebraska, USA.
• Lucas Bang, Abdulbaki Aydin, and Tevfik Bultan. "Automatically Computing Path Complexity of Programs." Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2015), pages 61-72, Bergamo, Italy, August 30-September 4, 2015.
• Tevfik Bultan. "String Analysis for Vulnerability Detection and Repair." Invited Paper. In Proceedings of the 22nd International Symposium on Model Checking Software (SPIN 2015), Stellenbosch, South Africa, August 24-26, 2015.
• Abdulbaki Aydin, Lucas Bang, and Tevfik Bultan. "Automata-based model counting for string constraints." Proceedings of the 27th International Conference on Computer Aided Verification (CAV 2015), pages 255-272, San Francisco, CA, USA, July 18-24, 2015.
• Ivan Bocic and Tevfik Bultan. "Coexecutability for Efficient Verification of Data Model Updates." Proceedings of the 37th International Conference on Software Engineering (ICSE 2015), pages 744-754, Florence, Italy, May 16-24, 2015.
• Ivan Bocic and Tevfik Bultan. "Data Model Bugs." Short paper. To appear in the Proceedings of the 7th NASA Formal Methods Symposium (NFM 2015), Pasadena, California, April 27-29, 2015.
• Jaideep Nijjar, Ivan Bocic and Tevfik Bultan. "Data Model Property Inference, Verification and Repair for Web Applications." ACM Transactions on Software Engineering and Methodology (TOSEM) , special issue on selected papers from the 2013 International Symposium on Software Testing and Analysis (ISSTA 2013), volume 24, issue 4, article no. 25, August 2015.
• Jian Lu, David S. Rosenblum, Tevfik Bultan, Valerie Issarny, Schahtam Dustdar, Margaret-Anne Storey, and Dongmei Zhang. "The Future of Software Engineering For Internet Computing." IEEE Software , pages 91-97, January/February 2015.

2014

• Samik Basu and Tevfik Bultan. "Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers." Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014), ACM SIGSOFT Distinguished Paper Award, pages 743-754, Vasteras, Sweden, September 15-19, 2014.
• Muath Alkhalaf, Abdulbaki Aydin, and Tevfik Bultan. "Semantic Differential Repair for Input Validation and Sanitization." Proceedings of the 2014 International Symposium on Software Testing and Analysis (ISSTA 2014), pages 225-236, San Jose, California, USA, July 21-25, 2014.
• Ivan Bocic and Tevfik Bultan. "Inductive Verification of Data Model Invariants for Web Applications." Proceedings of the 36th International Conference on Software Engineering (ICSE 2014), pages 620-631, Hyderabad, India, May 31-June 7, 2014. UCSB Computer Science Outstanding Publication Award.
• Abdulbaki Aydin, Muath Alkhalaf and Tevfik Bultan. "Automated Test Generation from Vulnerability Signatures." Proceedings of the 7th International Conference on Software Testing, Verification and Validation (ICST 2014), pages 193-202, Cleveland, Ohio, USA, March 31-April 4, 2014.
• Chandra Krintz, Hiranya Jayathilaka, Stratos Dimopoulos, Alexander Pucher, Rich Wolski and Tevfik Bultan. "Cloud Platform Support for API Governance." Proceedings of the IEEE International Workshop on the Future of PaaS 2014, Boston, Massachusetts, USA, March 11th, 2014.
• Fang Yu, Muath Alkhalaf, Tevfik Bultan and Oscar H. Ibarra. "Automata-Based Symbolic String Analysis for Vulnerability Detection." Formal Methods in System Design, volume 44, number 1, pages 44-70, 2014.

2013

• Meriem Ouderni, Gwen Salaun and Tevfik Bultan. "Compatibility Checking for Asynchronously Communicating Software." Proceedings of the 10th International Symposium on Formal Aspects of Component Software (FACS 2013), pages 310-328, Nanchang, China, October 27-29, 2013.
• Jaideep Nijjar and Tevfik Bultan. "Data Model Property Inference and Repair." Proceedings of the 2013 International Symposium on Software Testing and Analysis (ISSTA 2013), pages 202-212, Lugano, Switzerland, July 15-20, 2013.
• Tevfik Bultan. "Analyzing Interactions of Asynchronously Communicating Software Components." Invited Paper. In Proceedings of the Joint IFIP WG 6.1 Internation Conference on Formal Techniques for Distributed Systems (FORTE/FMOODS 2013). , LNCS 7892, pages 1-4, Florence, Italy, June 3-5, 2013.
• Jaideep Nijjar, Ivan Bocic and Tevfik Bultan. "An Integrated Data Model Verifier with Property Templates." Proceedings of the ICSE 2013 Workshop on Formal Methods in Software Engineering (FormaliSE 2013), pages 29-25, San Francisco, USA, May 25, 2013.
• Aysu Betin Can, Sylvain Halle, and Tevfik Bultan. "Modular Verification of Asynchronous Service Interactions Using Behavioral Interfaces." IEEE Transactions on Services Computing, volume 6, number 2, pages 262-275, April-June 2013.
• Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE 2013), Ewen Denney, Tevfik Bultan and Andreas Zeller, editors. ISBN: 978-1-4799-0215-6

2012

• Jaideep Nijjar and Tevfik Bultan. "Unbounded Data Model Verification Using SMT Solvers." Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering (ASE 2012), pages 210-219, Essen, Germany, September 3-7, 2012.
• Muath Alkhalaf, Shauvik Roy Choudhary, Mattia Fazzini, Tevfik Bultan, Alessandro Orso and Christopher Kruegel. "ViewPoints: Differential String Analysis for Discovering Client and Server-Side Input Validation Inconsistencies." Proceedings of the 2012 International Symposium on Software Testing and Analysis (ISSTA 2012), pages 56-66, Minneapolis, USA, July 15-20, 2012.
• Muath Alkhalaf, Tevfik Bultan, and Jose L. Gallegos. "Verifying Client-Side Input Validation Functions Using String Analysis." Proceedings of the 34th International Conference on Software Engineering (ICSE 2012) pages 947-957, Zurich, Switzerland, June 2-9, 2012.
• Samik Basu, Tevfik Bultan, and Meriem Ouederni. "Deciding Choreography Realizability," Proceedings of the 39th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2012), pages 191-202, Philadelphia, Pennsylvania, USA, January 22-28, 2012.
• Samik Basu, Tevfik Bultan, and Meriem Ouederni. "Synchronizability for Verification of Asynchronously Communicating Systems." Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012), LNCS 7148, pages 56-71, Philadelphia, Pennsylvania, USA, January 22-24, 2012.
• Gwen Salaun, Tevfik Bultan, and Nima Roohi "Realizability of Choreographies Using Process Algebra Encodings." IEEE Transactions on Services Computing, volume 5, number 3, pages 290-304, July-September, 2012.
• Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE 2012), Will Tracz, Martin Robillard and Tevfik Bultan, editors. ISBN 978-1-4503- 1614-9.

2011

• Fang Yu, Tevfik Bultan, and Oscar Ibarra. "Relational String Verification Using Multi-Track Automata." International Journal of Foundations of Computer Science (IJFCS), special issue on selected papers from the 15th International Conference on Implementation and Application of Automata (CIAA 2010), volume 22, number 8, pages 1909-1924, 2011.
• Fang Yu, Tevfik Bultan and Ben Hardekopf. "String Abstractions for String Verification." Proceedings of the 18th International SPIN Workshop on Model Checking of Software (SPIN 2011), LNCS 6823, pages 20-37, Snowbird, Utah, USA, July 14-15, 2011.
• Jaideep Nijjar and Tevfik Bultan. "Bounded Verification of Ruby on Rails Data Models." Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA 2011), pages 67-77, Toronto, Ontario, Canada, July 17-21, 2011.
• Samik Basu and Tevfik Bultan. "Choreography Conformance via Synchronizability." Proceedings of the 20th International World Wide Web Conference (WWW 2011), pages 795-804, Hyderabad, India, March 28-April 1, 2011.
• Fang Yu, Muath Alkhalaf and Tevfik Bultan. "Patching Vulnerabilities with Sanitization Synthesis." Proceedings of the 33rd International Conference on Software Engineering (ICSE 2011), pages 251-260, Waikiki, Honolulu , Hawaii, USA, May 21-28, 2011.
• Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA 2011), Tevfik Bultan and Pao-Ann Hsiung, editors. ISBN 978-3-642-24371-4.

2010

• Tevfik Bultan. "Software for Everyone by Everyone." Position paper. Proceedings of the 2010 FSE/SDP Workshop on the Future of Software Engineering Research, pages 69-74, Santa Fe, New Mexico, November 7 and 8, 2010.
• Ben Rubinger and Tevfik Bultan. "Contracting the Facebook API." Proceedings of the 4th International Workshop on Testing, Analysis and Verification of Web Software (TAV-WEB 2010), pages 63-74, Antwerp, Belgium, 21 September 2010.
• Sylvain Halle, Taylor Ettema, Chris Bunch and Tevfik Bultan. "Eliminating Navigation Errors in Web Applications via Model Checking and Runtime Enforcement of Navigation State Machines." Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010), pages 235-244, Antwerp, Belgium, 20-24 September 2010.
• Fang Yu, Tevfik Bultan and Oscar Ibarra. "Relational String Verification Using Multi-track Automata." Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), LNCS 6482, pages 290-299, Winnipeg, Manitoba, Canada on August 12-15 2010.
• Sylvain Halle and Tevfik Bultan. "Realizability Analysis for Message-based Interactions Using Shared-State Projections." Proceedings of the 18th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2010), pages 27-36, Santa Fe, New Mexico, November 7-11, 2010.
• Tevfik Bultan, Fang Yu, and Aysu Betin Can. "Modular Verification of Synchronization with Reentrant Locks." Proceedings of the 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pages 59-68, Grenoble, France, July 26-28, 2010.
• Fang Yu, Muath Alkhalaf and Tevfik Bultan. "Stranger: An Automata-based String Analysis Tool for PHP." Tool paper. Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010), LNCS 6015, pages 154-157, Paphos, Cyprus, March 20-28, 2010.
• Sylvain Halle, Tevfik Bultan, Graham Hughes, Muath Alkhalaf and Roger Villemaire. "Runtime Verification of Web Service Interface Contracts." IEEE Computer, volume 43, number 3, pages 59-66, March 2010.
• Proceedings of the 7th International Workshop on Web Services and Formal Methods (WS-FM 2010), Tevfik Bultan and Mario Bravetti, editors. ISBN 978-3-642-19588-4.

2009

• Sylvain Halle, Graham Hughes, Tevfik Bultan, and Muath Alkhalaf. "Generating Interface Grammars from WSDL for Automated Verification of Web Services." Proceedings of the 7th International Conference on Service Oriented Computing (ICSOC 2009), pp. 516-530, Stockholm, Sweden, November 24-27, 2009.
• Fang Yu, Muath Alkhalaf and Tevfik Bultan. "Generating Vulnerability Signatures for String Manipulating Programs Using Automata-based Forward and Backward Symbolic Analyses." Short paper. Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009), pp. 605-609, Auckland, New Zealand, November 16-20, 2009.
• Zachary Stengel and Tevfik Bultan. "Analyzing Singularity Channel Contracts." Proceedings of the 2009 International Symposium on Software Testing and Analysis (ISSTA 2009), pp. 13-24, Chicago, Illinois, July 19-23, 2009.
• Tevfik Bultan, Chris Ferguson and Xiang Fu "A Tool for Choreography Analysis Using Collaboration Diagrams." Proceedings of the 7th IEEE International Conference on Web Services (ICWS 2009), pp. 856-863, Los Angeles, CA, July 6-10, 2009.
• Fang Yu, Tevfik Bultan and Oscar H. Ibarra. "Symbolic String Verification: Combining String Analysis and Size Analysis." Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), pp. 322-336, York, UK, March 22-29, 2009.
• Gwen Salaün and Tevfik Bultan. "Realizability of Choreographies using Process Algebra Encodings." Proceedings of the 7th International Conference on integrated Formal Methods (IFM 2009), pp. 167-182, Dusseldorf, Germany, February 16-19, 2009
• Tuba Yavuz Kahveci and Tevfik Bultan. "Action Language Verifier: An Infinite State Model Checker for Reactive Software Specifications." Formal Methods in System Design, Volume 35, Issue 3 (2009), Page 325-367.

2008

• Graham Hughes and Tevfik Bultan. "Automated Verification of Access Control Policies Using a SAT Solver" International Journal on Software Tools for Technology Transfer (STTT), special issue on selected papers from the Workshop on Web Quality, Verification and Validation (WQVV 2007) vol. 10, no. 6, pp. 473 – 534, December 2008.
• Tevfik Bultan and Xiang Fu. "Choreography Modeling and Analysis with Collaboration Diagrams." Invited paper. Data Engineering Bulletin, vol. 31, no. 3, pp. 27–30, September 2008.
• Tevfik Bultan. "Developing Verifiable Concurrent Software." Position paper. CAV 2008 Workshop on Exploiting Concurrency Efficiently and Correctly.
• Tevfik Bultan.   "Service Choreography and Orchestration with Conversations." Invited abstract. Proceedings of the Nineteenth International Conference on Concurrency Theory (CONCUR 2008), pp. 2-3, Toronto, Canada, August 19-22, 2008.
• Fang Yu, Chao Wang, Aarti Gupta and Tevfik Bultan. "Modular Verification of Web Services Using Efficient Symbolic Encoding and Summarization." Proceedings of the Sixteenth ACM SIGSOFT Symposium on Foundations of Software Engineering (FSE 2008), pp. 192-202, Atlanta, Georgia, November 9-14, 2008.
• Graham Hughes, Tevfik Bultan and Muath Alkhalaf. "Client and Server Verification for Web Services Using Interface Grammars." Proceedings of the Workshop on Testing, Analysis and Verification of Web Software (TAV-WEB 2008), pp. 40-46, Seattle, Washington, July 21, 2008.
• Tevfik Bultan and Tao Xie. "Workshop on Testing, Analysis and Verification of Web Software (TAV-WEB 2008)." Workshop Summary. Proceedings of the 2008 International Symposium on Software Testing and Analysis (ISSTA 2008), pp. 311-312, Seattle, Washington, July, 2008.
• Graham Hughes and Tevfik Bultan. "Interface Grammars for Modular Software Model Checking." IEEE Transactions on Software Engineering, special issue on selected papers from the 2007 ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2007), vol. 34, no. 5, pp. 614-632, 2008.
• Fang Yu, Tevfik Bultan, Marco Cova, and Oscar H. Ibarra. "Symbolic String Verification: An Automata-based Approach." Proceedings of the 15th International SPIN Workshop on Model Checking of Software (SPIN 2008), pp. 306-324, Los Angeles, CA, August 10-12, 2008.
• Tevfik Bultan and Constance Heitmeyer. "Applying Infinite State Model Checking and Other Analysis Techniques to Tabular Requirements Specifications of Safety-Critical Systems." 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), vol. 12, no. 1-2, pp. 97-137, June 2008.
• Tevfik Bultan and Xiang Fu. "Specification of Realizable Service Conversations Using Collaboration Diagrams." Service Oriented Computing and Applications, vol. 2, no. 1, pp. 27-39, April 2008.
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Realizability Analysis of Top-down Web Service Composition Specifications." Invited book chapter. Web Services Research and Practices, Volume 2 of the Advances in Web Services Research (WSR) Series, Liang-Jie Zhang (ed.), Idea Group, Inc., April 2008.
• Proceedings of the Workshop on Testing, Analysis and Verification of Web Software (TAV-WEB 2008), Tevfik Bultan and Tao Xie, editors, ACM, ISBN: 978-1-60558-052-4.

2007

• Jianwen Su, Tevfik Bultan, Xiang Fu, and Xiangpeng Zhao. "Towards a Theory of Web Service Choreographies." Invited paper. Proceedings of the 4th International Workshop on Web Services and Formal Methods (WS-FM 2007). Marlon Dumas, Reiko Heckel (eds.), LNCS 4937, pp. 1-16, Brisbane, Australia, September 28-29, 2007.
• Graham Hughes and Tevfik Bultan. "Extended Interface Grammars for Automated Stub Generation." Proceedings of the Automated Formal Methods Workshop (AFM 2007), pp. 41-54, Atlanta, Georgia, November 6, 2007
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.

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.
• Tevfik Bultan and Xiang Fu. "Realizability of Interactions in Collaboration Diagrams." Technical Report 2006-11, Computer Science Department, University of California, Santa Barbara.
• 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.
• Tevfik Bultan, Xiang Fu, Jianwen Su. "Analyzing Conversations of Web Services." IEEE Internet Computing, vol. 10, no. 1, pp. 18-25, January/February 2006.
• 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.
• Proceedings of the Workshop on Testing, Analysis and Verification of Web Services and Applications (TAV-WEB 2006), Tevfik Bultan, editor, ACM, ISBN: 1-59593-458-8.

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.
• 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.
• 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, pp. 337-346, Zurich, Switzerland, October 10-14, 2005.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.

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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.

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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.

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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.

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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.