| 2024 | ICST | Does Going Beyond Branch Coverage Make Program Repair Tools More Reliable? | Amirfarhad Nilizadeh, Gary T. Leavens, Corina S. Pasareanu, Xuan-Bach Dinh Le, David R. Cok |
| 2022 | FTfJP | Automated Reasoning Repair. | Amirfarhad Nilizadeh, Gary T. Leavens, David R. Cok |
| 2022 | ISoLA | Abstraction in Deductive Verification: Model Fields and Model Methods. | David R. Cok, Gary T. Leavens |
| 2021 | ICST | Exploring True Test Overfitting in Dynamic Automated Program Repair using Formal Methods. | Amirfarhad Nilizadeh, Gary T. Leavens, Xuan-Bach Dinh Le, Corina S. Pasareanu, David R. Cok |
| 2021 | ISSRE | More Reliable Test Suites for Dynamic APR by using Counterexamples. | Amirfarhad Nilizadeh, Marlon Calvo, Gary T. Leavens, Xuan-Bach Dinh Le |
| 2021 | TAP | Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs. | Amirfarhad Nilizadeh, Gary T. Leavens, Corina S. Pasareanu |
| 2018 | ICSE | An algorithm and tool to infer practical postconditions. | John L. Singleton, Gary T. Leavens, Hridesh Rajan, David R. Cok |
| 2017 | CVPR | Information Hiding in RGB Images Using an Improved Matrix Pattern Approach. | Amirfarhad Nilizadeh, Wojciech Mazurczyk, Cliff C. Zou, Gary T. Leavens |
| 2016 | ECOOP | Towards Modular Reasoning for Context-Oriented Programs. | Tomoyuki Aotani, Gary T. Leavens |
| 2016 | IRI | Spekl: A Layered System for Specification Authoring, Sharing, and Usage. | John L. Singleton, Gary T. Leavens |
| 2016 | ISoLA | Specifying and Verifying Advanced Control Features. | Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani |
| 2015 | ECOOP | Conditional effects in fine-grained region logic. | Yuyan Bao, Gary T. Leavens, Gidon Ernst |
| 2015 | ICSE | Inferring Behavioral Specifications from Large-scale Repositories by Leveraging Collective Intelligence. | Hridesh Rajan, Tien N. Nguyen, Gary T. Leavens, Robert Dyer |
| 2014 | ICSE | Verily: a web framework for creating more reasonable web applications. | John L. Singleton, Gary T. Leavens |
| 2013 | OOPSLA | Client-aware checking and information hiding in interface specifications with JML/ajmlc. | Henrique Reblo, Gary T. Leavens, Ricardo Massa Ferreira Lima |
| 2012 | ICST | @tComment: Testing Javadoc Comments to Detect Comment-Code Inconsistencies. | Shin Hwei Tan, Darko Marinov, Lin Tan, Gary T. Leavens |
| 2011 | ECOOP | On the interplay of exception handling and design by contract: an aspect-oriented recovery approach. | Henrique Reblo, Roberta Coelho, Ricardo M. F. Lima, Gary T. Leavens, Marieke Huisman, Alexandre Mota, Fernando Castor |
| 2011 | FM | The 1st Verified Software Competition: Experience Report. | Vladimir Klebanov, Peter Mller, Natarajan Shankar, Gary T. Leavens, Valentin Wstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Wei |
| 2011 | OOPSLA | Modularizing crosscutting concerns with ptolemy. | Hridesh Rajan, Sean L. Mooney, Gary T. Leavens, Robert Dyer, Rex D. Fernando, Mohammad Ali Darvish Darab, Bryan Welter |
| 2010 | OOPSLA | Translucid contracts for modular reasoning about aspect-oriented programs. | Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens, Sean L. Mooney |
| 2010 | SEFM | temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties. | Faraz Hussain, Gary T. Leavens |
| 2009 | ESOP | Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services. | Hridesh Rajan, Jia Tao, Steve M. Shaner, Gary T. Leavens |
| 2008 | ECOOP | Ptolemy: A Language with Quantified, Typed Events. | Hridesh Rajan, Gary T. Leavens |
| 2008 | SEKE | Integrating Random Testing with Constraints for Improved Efficiency and Diversity. | Yoonsik Cheon, Antonio Cortes, Gary T. Leavens, Martine Ceberio |
| 2007 | CAV | A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. | Gary T. Leavens, Joseph R. Kiniry, Erik Poll |
| 2007 | ECOOP | MAO: Ownership and Effects for More Effective Reasoning About Aspects. | Curtis Clifton, Gary T. Leavens, James Noble |
| 2007 | ICSE | Information Hiding and Visibility in Interface Specifications. | Gary T. Leavens, Peter Mller |
| 2007 | OOPSLA | Modular verification of higher-order methods with mandatory calls specified by model programs. | Steve M. Shaner, Gary T. Leavens, David A. Naumann |
| 2006 | GPCE | Roadmap for enhanced languages and methods to aid verification. | Gary T. Leavens, Jean-Raymond Abrial, Don S. Batory, Michael J. Butler, Alessandro Coglio, Kathi Fisler, Eric C. R. Hehner, Cliff B. Jones, Dale Miller, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump |
| 2006 | ICFEM | JML's Rich, Inherited Specifications for Behavioral Subtypes. | Gary T. Leavens |
| 2005 | ECOOP | Extending JML for Modular Specification and Verification of Multi-threaded Programs. | Edwin Rodrguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby |
| 2002 | ECOOP | A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. | Yoonsik Cheon, Gary T. Leavens |
| 2001 | SAC | Formal semantics of an algorithm for translating model-based specifications to concurrent constraint programs. | Tim Wahls, Gary T. Leavens |
| 2000 | OOPSLA | MultiJava: modular open classes and symmetric multiple dispatch for Java. | Curtis Clifton, Gary T. Leavens, Craig Chambers, Todd D. Millstein |
| 2000 | OOPSLA | JML (poster session): notations and tools supporting detailed design in Java. | Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs |
| 2000 | OOPSLA | Safely creating correct subclasses without seeing superclass code. | Clyde Ruby, Gary T. Leavens |
| 1999 | FM | Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. | Gary T. Leavens, Albert L. Baker |
| 1999 | SAC | Formal Semantics for SA Style Data Flow Diagram Specification Languages. | Gary T. Leavens, Tim Wahls, Albert L. Baker |
| 1998 | OOPSLA | Multiple Dispatch as Dispatch on Tuples. | Gary T. Leavens, Todd D. Millstein |
| 1996 | ICSE | Forcing Behavioral Subtyping through Specification Inheritance. | Krishna Kishore Dhara, Gary T. Leavens |
| 1994 | OOPSLA | Typechecking and Modules for Multi-Methods. | Craig Chambers, Gary T. Leavens |
| 1991 | MFPS | Typed Homomorphic Relations Extended with Sybtypes. | Gary T. Leavens, Don Pigozzi |
| 1991 | OOPSLA | Formal Techniques for OO Software Development (Panel). | Dennis de Champeaux, Pierre America, Derek Coleman, Roger Duke, Doug Lea, Gary T. Leavens, Fiona Hayes |
| 1990 | OOPSLA | Reasoning about Object-Oriented Programs that Use Subtypes. | Gary T. Leavens, William E. Weihl |