| 2025 | ICST | Black-Box Multi-Robustness Testing for Neural Networks. | Mara Downing, Tevfik Bultan |
| 2025 | ICST | Hybrid Equivalence/Non-Equivalence Testing. | Laboni Sarker, Tevfik Bultan |
| 2024 | ICFEM | Quantitative Symbolic Robustness Verification for Quantized Neural Networks. | Mara Downing, William Eiers, Erin DeLong, Anushka Lodha, Brian Ozawa Burns, Ismet Burak Kadron, Tevfik Bultan |
| 2023 | ISSTA | Quantitative Policy Repair for Access Control on the Cloud. | William Eiers, Ganesh Sankaran, Tevfik Bultan |
| 2023 | ISSTA | Rare Path Guided Fuzzing. | Seemanta Saha, Laboni Sarker, Md Shafiuzzaman, Chaofan Shou, Albert Li, Ganesh Sankaran, Tevfik Bultan |
| 2022 | ICSE | Quantifying Permissiveness of Access Control Policies. | William Eiers, Ganesh Sankaran, Albert Li, Emily O'Mahony, Benjamin Prince, Tevfik Bultan |
| 2022 | ICSE | PREACH: A Heuristic for Probabilistic Reachability to Identify Hard to Reach Statements. | Seemanta Saha, Mara Downing, Tegan Brennan, Tevfik Bultan |
| 2020 | ICSE | JVM fuzzing for JIT-induced side-channel detection. | Tegan Brennan, Seemanta Saha, Tevfik Bultan |
| 2020 | ISSTA | Feedback-driven side-channel analysis for networked applications. | Ismet Burak Kadron, Nicols Rosner, Tevfik Bultan |
| 2020 | SP | JIT Leaks: Inducing Timing Side Channels through Just-In-Time Compilation. | Tegan Brennan, Nicols Rosner, Tevfik Bultan |
| 2019 | NDSS | Profit: Detecting and Quantifying Side Channels in Networked Applications. | Nicols Rosner, Ismet Burak Kadron, Lucas Bang, Tevfik Bultan |
| 2018 | ATVA | Information Leakage in Arbiter Protocols. | Nestan Tsiskaridze, Lucas Bang, Joseph McMahan, Tevfik Bultan, Timothy Sherwood |
| 2018 | ICSE | Symbolic path cost analysis for side-channel detection. | Tegan Brennan, Seemanta Saha, Tevfik Bultan |
| 2018 | ICSE | Static detection of API call vulnerabilities in iOS executables. | Chun-Han Lin, Fang Yu, Jie-Hong Roland Jiang, Tevfik Bultan |
| 2018 | ISSTA | Symbolic path cost analysis for side-channel detection. | Tegan Brennan, Seemanta Saha, Tevfik Bultan, Corina S. Pasareanu |
| 2017 | ICSE | Symbolic model extraction for web application verification. | Ivan Bocic, Tevfik Bultan |
| 2016 | FASE | Automated Choreography Repair. | Samik Basu, Tevfik Bultan |
| 2016 | ISSTA | Optimal sanitization synthesis for web application vulnerability repair. | Fang Yu, Ching-Yuan Shueh, Chun-Han Lin, Yu-Fang Chen, Bow-Yaw Wang, Tevfik Bultan |
| 2015 | CAV | Automata-Based Model Counting for String Constraints. | Abdulbaki Aydin, Lucas Bang, Tevfik Bultan |
| 2015 | ICSE | Coexecutability for Efficient Verification of Data Model Updates. | Ivan Bocic, Tevfik Bultan |
| 2014 | IC2E | Cloud Platform Support for API Governance. | Chandra Krintz, Hiranya Jayathilaka, Stratos Dimopoulos, Alexander Pucher, Rich Wolski, Tevfik Bultan |
| 2014 | ICSE | Inductive verification of data model invariants for web applications. | Ivan Bocic, Tevfik Bultan |
| 2014 | ICST | Automated Test Generation from Vulnerability Signatures. | Abdulbaki Aydin, Muath Alkhalaf, Tevfik Bultan |
| 2014 | ISSTA | Semantic differential repair for input validation and sanitization. | Muath Alkhalaf, Abdulbaki Aydin, Tevfik Bultan |
| 2013 | FORTE | Analyzing Interactions of Asynchronously Communicating Software Components - (Invited Paper). | Tevfik Bultan |
| 2013 | ICSE | An integrated data model verifier with property templates. | Jaideep Nijjar, Ivan Bocic, Tevfik Bultan |
| 2013 | ISSTA | Data model property inference and repair. | Jaideep Nijjar, Tevfik Bultan |
| 2012 | ICSE | Verifying client-side input validation functions using string analysis. | Muath Alkhalaf, Tevfik Bultan, Jose L. Gallegos |
| 2012 | ISSTA | ViewPoints: differential string analysis for discovering client- and server-side input validation inconsistencies. | Muath Alkhalaf, Shauvik Roy Choudhary, Mattia Fazzini, Tevfik Bultan, Alessandro Orso, Christopher Kruegel |
| 2012 | POPL | Deciding choreography realizability. | Samik Basu, Tevfik Bultan, Meriem Ouederni |
| 2012 | VMCAI | Synchronizability for Verification of Asynchronously Communicating Systems. | Samik Basu, Tevfik Bultan, Meriem Ouederni |
| 2011 | ICSE | Patching vulnerabilities with sanitization synthesis. | Fang Yu, Muath Alkhalaf, Tevfik Bultan |
| 2011 | ISSTA | Bounded verification of Ruby on Rails data models. | Jaideep Nijjar, Tevfik Bultan |
| 2011 | WWW | Choreography conformance via synchronizability. | Samik Basu, Tevfik Bultan |
| 2010 | MEMOCODE | Modular verification of synchronization with reentrant locks. | Tevfik Bultan, Fang Yu, Aysu Betin-Can |
| 2010 | TACAS | Stranger: An Automata-Based String Analysis Tool for PHP. | Fang Yu, Muath Alkhalaf, Tevfik Bultan |
| 2009 | ICSOC | Generating Interface Grammars from WSDL for Automated Verification of Web Services. | Sylvain Hall, Graham Hughes, Tevfik Bultan, Muath Alkhalaf |
| 2009 | ICWS | A Tool for Choreography Analysis Using Collaboration Diagrams. | Tevfik Bultan, Chris Ferguson, Xiang Fu |
| 2009 | IFM | Realizability of Choreographies Using Process Algebra Encodings. | Gwen Salan, Tevfik Bultan |
| 2009 | ISSTA | Analyzing singularity channel contracts. | Zachary Stengel, Tevfik Bultan |
| 2009 | TACAS | Symbolic String Verification: Combining String Analysis and Size Analysis. | Fang Yu, Tevfik Bultan, Oscar H. Ibarra |
| 2008 | CONCUR | Service Choreography and Orchestration with Conversations. | Tevfik Bultan |
| 2008 | ISSTA | Workshop on testing, analysis and verification of web software (TAV-WEB 2008). | Tevfik Bultan, Tao Xie |
| 2008 | ISSTA | Client and server verification for web services using interface grammars. | Graham Hughes, Tevfik Bultan, Muath Alkhalaf |
| 2007 | ISSTA | Interface grammars for modular software model checking. | Graham Hughes, Tevfik Bultan |
| 2006 | MEMOCODE | Analyzing tabular requirements specifications using infinite state model checking. | Tevfik Bultan, Constance L. Heitmeyer |
| 2005 | CAV | Action Language Verifier, Extended. | Tuba Yavuz-Kahveci, Constantinos Bartzis, Tevfik Bultan |
| 2005 | ICWS | Verifiable Web Services with Hierarchical Interfaces. | Aysu Betin-Can, Tevfik Bultan |
| 2005 | ICWS | Web Service Interactions: Analysis and Design. | Jianwen Su, Tevfik Bultan, Xiang Fu |
| 2005 | MEMOCODE | Panel on design for verification. | Tevfik Bultan, Constance L. Heitmeyer, John O'Leary |
| 2005 | MEMOCODE | Verification of parameterized hierarchical state machines using action language verifier. | Tuba Yavuz-Kahveci, Tevfik Bultan |
| 2005 | WWW | Design for verification for asynchronously communicating Web services. | Aysu Betin-Can, Tevfik Bultan, Xiang Fu |
| 2004 | ATVA | Tools for Automated Verification of Web Services. | Tevfik Bultan, Xiang Fu, Jianwen Su |
| 2004 | CAV | Widening Arithmetic Automata. | Constantinos Bartzis, Tevfik Bultan |
| 2004 | CAV | WSAT: A Tool for Formal Analysis of Web Services. | Xiang Fu, Tevfik Bultan, Jianwen Su |
| 2004 | ICWS | Realizability of Conversation Protocols With Message Contents. | Xiang Fu, Tevfik Bultan, Jianwen Su |
| 2004 | ISSTA | Model checking XML manipulating software. | Xiang Fu, Tevfik Bultan, Jianwen Su |
| 2004 | MEMOCODE | Panel: given that hardware verification has been an uphill battle, what is the future of software verification? | Sandeep K. Shukla, Tevfik Bultan, Constance L. Heitmeyer |
| 2004 | WWW | Analysis of interacting BPEL web services. | Xiang Fu, Tevfik Bultan, Jianwen Su |
| 2003 | CAV | Efficient Image Computation in Infinite State Model Checking. | Constantinos Bartzis, Tevfik Bultan |
| 2003 | WWW | Conversation specification: a new approach to design and analysis of e-service composition. | Tevfik Bultan, Xiang Fu, Richard Hull, Jianwen Su |
| 2003 | TACAS | Construction of Efficient BDDs for Bounded Arithmetic Constraints. | Constantinos Bartzis, Tevfik Bultan |
| 2002 | ISSTA | Specification, verification, and synthesis of concurrency control components. | Tuba Yavuz-Kahveci, Tevfik Bultan |
| 2002 | SAS | Automated Verification of Concurrent Linked Lists with Counters. | Tuba Yavuz-Kahveci, Tevfik Bultan |
| 2001 | CP | Constraint-Based Verification of Client-Server Protocols. | Giorgio Delzanno, Tevfik Bultan |
| 2001 | TACAS | Verification of Vortex Workflows. | Xiang Fu, Tevfik Bultan, Richard Hull, Jianwen Su |
| 2001 | TACAS | A Library for Composite Symbolic Representations. | Tuba Yavuz-Kahveci, Murat Tuncer, Tevfik Bultan |
| 2000 | CAV | Binary Reachability Analysis of Discrete Pushdown Timed Automata. | Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, Jianwen Su |
| 2000 | CONCUR | Reachability Analysis for Some Models of Infinite-State Transition Systems. | Oscar H. Ibarra, Tevfik Bultan, Jianwen Su |
| 2000 | ICSE | Action Language: a specification language for model checking reactive systems. | Tevfik Bultan |
| 2000 | MFCS | Conter Machines: Decidable Properties and Applications to Verification Problems. | Oscar H. Ibarra, Jianwen Su, Zhe Dang, Tevfik Bultan, Richard A. Kemmerer |
| 2000 | TACAS | BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. | Tevfik Bultan |
| 1998 | ISSTA | Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach. | Tevfik Bultan, Richard Gerber, Christopher League |
| 1997 | CAV | Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. | Tevfik Bultan, Richard Gerber, William W. Pugh |
| 1996 | ISSTA | Compositional Verification by Model Checking for Counter-Examples. | Tevfik Bultan, Jeffrey Fischer, Richard Gerber |