Gary T. Leavens

ORCID

Publication Activity (10 Years)

Years Active: 1984-2024
Publications (10 Years): 25

Top Venues

FTfJP@ECOOP

MODULARITY (Companion)

CoRR

MODULARITY

Publications

Amirfarhad Nilizadeh, Gary T. Leavens, Corina S. Pasareanu, Yannic Noller
JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion Checking. Formal Aspects Comput. 36 (1) (2024)
Amirfarhad Nilizadeh, Gary T. Leavens, David R. Cok
Toward Using Fuzzers and Lightweight Specifications to Reveal Semantic Bugs. J. Object Technol. 23 (2) (2024)
Syeda Khairunnesa Samantha, Shibbir Ahmed, Sayem Mohammad Imtiaz, Hridesh Rajan, Gary T. Leavens
What Kinds of Contracts Do ML APIs Need? CoRR (2023)
Syeda Khairunnesa Samantha, Shibbir Ahmed, Sayem Mohammad Imtiaz, Hridesh Rajan, Gary T. Leavens
What kinds of contracts do ML APIs need? Empir. Softw. Eng. 28 (6) (2023)
Amirfarhad Nilizadeh, Gary T. Leavens
Be Realistic: Automated Program Repair is a Combination of Undecidable Problems. APR@ICSE (2022)
Amirfarhad Nilizadeh, Shirin Nilizadeh, Wojciech Mazurczyk, Cliff C. Zou, Gary T. Leavens
Adaptive Matrix Pattern Steganography on RGB Images. J. Cyber Secur. Mobil. 11 (1) (2022)
Gary T. Leavens, David R. Cok, Amirfarhad Nilizadeh
Further Lessons from the JML Project. The Logic of Software. A Tasting Menu of Formal Methods (2022)
Amirfarhad Nilizadeh, Marlon Calvo, Gary T. Leavens, David R. Cok
Generating Counterexamples in the form of Unit Tests from Hoare-style Verification Attempts. FormaliSE@ICSE (2022)
David R. Cok, Gary T. Leavens
Abstraction in Deductive Verification: Model Fields and Model Methods. ISoLA (1) (2022)
Amirfarhad Nilizadeh, Gary T. Leavens, David R. Cok
Automated Reasoning Repair. FTfJP@ECOOP (2022)
Amirfarhad Nilizadeh, Gary T. Leavens, Corina S. Pasareanu
Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs. TAP@STAF (2021)
Amirfarhad Nilizadeh, Gary T. Leavens, Xuan-Bach Dinh Le, Corina S. Pasareanu, David R. Cok
Exploring True Test Overfitting in Dynamic Automated Program Repair using Formal Methods. ICST (2021)
Amirfarhad Nilizadeh, Marlon Calvo, Gary T. Leavens, Xuan-Bach D. Le
More Reliable Test Suites for Dynamic APR by using Counterexamples. ISSRE (2021)
John L. Singleton, Gary T. Leavens, Hridesh Rajan, David R. Cok
Inferring Concise Specifications of APIs. CoRR (2019)
John L. Singleton, Gary T. Leavens, Hridesh Rajan, David R. Cok
An algorithm and tool to infer practical postconditions. ICSE (Companion Volume) (2018)
Peter W. V. Tran-Jørgensen, Peter Gorm Larsen, Gary T. Leavens
Automated translation of VDM to JML-annotated Java. Int. J. Softw. Tools Technol. Transf. 20 (2) (2018)
Yuyan Bao, Gary T. Leavens
A Methodology for Invariants, Framing, and Subtyping in JML. Principled Software Development (2018)
Yuyan Bao, Gary T. Leavens, Gidon Ernst
Unifying separation logic and region logic to allow interoperability. Formal Aspects Comput. 30 (3-4) (2018)
Henrique Rebêlo, Gary T. Leavens
Aspect-Oriented Programming Reloaded. SBLP (2017)
Amirfarhad Nilizadeh, Wojciech Mazurczyk, Cliff C. Zou, Gary T. Leavens
Information Hiding in RGB Images Using an Improved Matrix Pattern Approach. CVPR Workshops (2017)
Gary T. Leavens, David A. Naumann
An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping. SETSS (2017)
José Sánchez, Gary T. Leavens
Reasoning tradeoffs in languages with enhanced modularity features. MODULARITY (2016)
Gary T. Leavens, David A. Naumann, Hridesh Rajan, Tomoyuki Aotani
Specifying and Verifying Advanced Control Features. ISoLA (2) (2016)
John L. Singleton, Gary T. Leavens
Spekl: A Layered System for Specification Authoring, Sharing, and Usage. IRI (2016)
Tomoyuki Aotani, Gary T. Leavens
Towards Modular Reasoning for Context-Oriented Programs. FTfJP@ECOOP (2016)
Yuyan Bao, Gary T. Leavens, Gidon Ernst
Conditional effects in fine-grained region logic. FTfJP@ECOOP (2015)
Henrique Rebêlo, Gary T. Leavens
Enforcing information hiding in interface specifications: a client-aware checking approach. MODULARITY (Companion) (2015)
Gary T. Leavens
JML: Expressive Contracts, Specification Inheritance, and Behavioral Subtyping. PPPJ (2015)
Hridesh Rajan, Tien N. Nguyen, Gary T. Leavens, Robert Dyer
Inferring Behavioral Specifications from Large-scale Repositories by Leveraging Collective Intelligence. ICSE (2) (2015)
Gary T. Leavens, David A. Naumann
Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. ACM Trans. Program. Lang. Syst. 37 (4) (2015)
Henrique Rebêlo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Massa Ferreira Lima, Daniel M. Zimmerman, Márcio Cornélio, Thomas Thüm
Modularizing crosscutting contracts with AspectJML. MODULARITY (Companion) (2014)
José Sánchez, Gary T. Leavens
Static verification of ptolemyrely programs using openJML. FOAL (2014)
Henrique Rebêlo, Gary T. Leavens, Mehdi Bagherzadeh, Hridesh Rajan, Ricardo Massa Ferreira Lima, Daniel M. Zimmerman, Márcio Cornélio, Thomas Thüm
AspectJML: modular specification and runtime checking for crosscutting contracts. MODULARITY (2014)
John L. Singleton, Gary T. Leavens
Verily: a web framework for creating more reasonable web applications. ICSE Companion (2014)
Ghaith Haddad, Gary T. Leavens
Specifying subtypes in Safety Critical Java programs. Concurr. Comput. Pract. Exp. 25 (16) (2013)
José Sánchez, Gary T. Leavens
Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification. SC@STAF (2013)
Henrique Rebêlo, Ricardo Massa Ferreira Lima, Gary T. Leavens, Márcio Cornélio, Alexandre Mota, César A. L. Oliveira
Optimizing generated aspect-oriented assertion checking code for JML using program transformations: An empirical study. Sci. Comput. Program. 78 (8) (2013)
Henrique Rebêlo, Gary T. Leavens, Ricardo Massa Ferreira Lima
Client-aware checking and information hiding in interface specifications with JML/ajmlc. SPLASH (Companion Volume) (2013)
Gary T. Leavens, Peter H. Schmitt, Jooyong Yi
The Java Modeling Language (JML) (NII Shonan Meeting 2013-3). NII Shonan Meet. Rep. 2013 (2013)
Henrique Rebêlo, Gary T. Leavens, Ricardo Massa Ferreira Lima, Paulo Borba, Márcio Ribeiro
Modular aspect-oriented design rule enforcement with XPIDRs. FOAL (2013)
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson
Behavioral interface specification languages. ACM Comput. Surv. 44 (3) (2012)
Shin Hwei Tan, Darko Marinov, Lin Tan, Gary T. Leavens
@tComment: Testing Javadoc Comments to Detect Comment-Code Inconsistencies. ICST (2012)
Rochelle Elva, Gary T. Leavens
Semantic clone detection using method IOE-behavior. IWSC (2012)
Henrique Rebêlo, Roberta Coelho, Ricardo M. F. Lima, Gary T. Leavens, Marieke Huisman, Alexandre Mota, Fernando Castor
On the interplay of exception handling and design by contract: an aspect-oriented recovery approach. FTfJP@ECOOP (2011)
Mehdi Bagherzadeh, Gary T. Leavens, Robert Dyer
Applying translucid contracts for modular reasoning about aspect and object oriented events. FOAL (2011)
Hridesh Rajan, Sean L. Mooney, Gary T. Leavens, Robert Dyer, Rex D. Fernando, Mohammad Ali Darvish Darab, Bryan Welter
Modularizing crosscutting concerns with ptolemy. OOPSLA Companion (2011)
Hridesh Rajan, Gary T. Leavens, Robert Dyer, Mehdi Bagherzadeh
Modularizing crosscutting concerns with Ptolemy. AOSD (Companion) (2011)
Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens, Sean L. Mooney
Translucid contracts: expressive specification and modular verification for aspect-oriented interfaces. AOSD (2011)
Ghaith Haddad, Gary T. Leavens
Specifying subtypes in SCJ programs. JTRES (2011)
Frank Piessens, Bart Jacobs, Gary T. Leavens
Special Section on Formal Techniques for Java-like Programs. J. Object Technol. 10 (2011)
Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, 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ß
The 1st Verified Software Competition: Experience Report. FM (2011)
Faraz Hussain, Gary T. Leavens
temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking of Temporal Properties. SEFM (2010)
Mehdi Bagherzadeh, Hridesh Rajan, Gary T. Leavens, Sean L. Mooney
Translucid contracts for modular reasoning about aspect-oriented programs. SPLASH/OOPSLA Companion (2010)
Gary T. Leavens
The future of library specification. FoSER (2010)
Tomas Kalibera, Pavel Parízek, Ghaith Haddad, Gary T. Leavens, Jan Vitek
Challenge benchmarks for verification of real-time programs. PLPV (2010)
Ghaith Haddad, Faraz Hussain, Gary T. Leavens
The design of SafeJML, a specification language for SCJ with support for WCET specification. JTRES (2010)
Tomas Kalibera, Pavel Parízek, Ghaith Haddad, Gary T. Leavens, Jan Vitek
Challenge benchmarks for verification of real-time programs: (abstract only). ACM SIGPLAN Notices 44 (11) (2009)
Hridesh Rajan, Jia Tao, Steve M. Shaner, Gary T. Leavens
Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services. ESOP (2009)
C. A. R. Hoare, Jayadev Misra, Gary T. Leavens, Natarajan Shankar
The verified software initiative: A manifesto. ACM Comput. Surv. 41 (4) (2009)
Gary T. Leavens
Use concurrent programming models to motivate teaching of programming languages. ACM SIGPLAN Notices 43 (11) (2008)
Eric Allen, Mark W. Bailey, Rastislav Bodík, Kim B. Bruce, Kathleen Fisher, Stephen N. Freund, Robert Harper, Chandra Krintz, Shriram Krishnamurthi, James R. Larus, Doug Lea, Gary T. Leavens, Lori L. Pollock, Stuart Reges, Martin C. Rinard, Mark A. Sheldon, Franklyn A. Turbak, Mitchell Wand
SIGPLAN programming language curriculum workshop: Discussion Summaries and recommendations. ACM SIGPLAN Notices 43 (11) (2008)
Yoonsik Cheon, Antonio Cortes, Gary T. Leavens, Martine Ceberio
Integrating Random Testing with Constraints for Improved Efficiency and Diversity. SEKE (2008)
Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary T. Leavens, Peter Müller, Tobias Wrigstad
Formal Techniques for Java-Like Programs. ECOOP Workshops (2008)
Hridesh Rajan, Gary T. Leavens
Ptolemy: A Language with Quantified, Typed Events. ECOOP (2008)
Gary T. Leavens, Dimitra Giannakopoulou, Jonathan Aldrich, Michael Barnett, Natasha Sharygina
Specification and verification of component-based systems 2007. ESEC/SIGSOFT FSE (Companion) (2007)
John Boyland, Dave Clarke, Gary T. Leavens, Francesco Logozzo, Arnd Poetzsch-Heffter
Formal Techniques for Java-Like Programs. ECOOP Workshops (2007)
Gary T. Leavens, Curtis Clifton
Multiple concerns in aspect-oriented language design: a language engineering approach to balancing benefits, with examples. SPLAT (2007)
Gary T. Leavens, K. Rustan M. Leino, Peter Müller
Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19 (2) (2007)
Gary T. Leavens, Joseph R. Kiniry, Erik Poll
A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java. CAV (2007)
Gary T. Leavens
Tutorial on JML, the java modeling language. ASE (2007)
Jonathan Aldrich, Michael Barnett, Dimitra Giannakopoulou, Gary T. Leavens, Natasha Sharygina
Specification and verification of component-based systems 2007. ESEC/SIGSOFT FSE (2007)
Curtis Clifton, Gary T. Leavens, James Noble
MAO: Ownership and Effects for More Effective Reasoning About Aspects. ECOOP (2007)
Gary T. Leavens, Peter Müller
Information Hiding and Visibility in Interface Specifications. ICSE (2007)
Steve M. Shaner, Gary T. Leavens, David A. Naumann
Modular verification of higher-order methods with mandatory calls specified by model programs. OOPSLA (2007)
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
Roadmap for enhanced languages and methods to aid verification. GPCE (2006)
Gary T. Leavens
JML's Rich, Inherited Specifications for Behavioral Subtypes. ICFEM (2006)
Gary T. Leavens, Albert L. Baker, Clyde Ruby
Preliminary design of JML: a behavioral interface specification language for java. ACM SIGSOFT Softw. Eng. Notes 31 (3) (2006)
Peter Müller, Arnd Poetzsch-Heffter, Gary T. Leavens
Modular invariants for layered object structures. Sci. Comput. Program. 62 (3) (2006)
Curtis Clifton, Gary T. Leavens
MiniMAO: An imperative core language for studying aspect-oriented reasoning. Sci. Comput. Program. 63 (3) (2006)
Davide Ancona, Sophia Drossopoulou, Atsushi Igarashi, Gary T. Leavens, Arnd Poetzsch-Heffter, Elena Zucca
Formal Techniques for Java-Like Programs. ECOOP Workshops (2006)
Curtis Clifton, Todd D. Millstein, Gary T. Leavens, Craig Chambers
MultiJava: Design rationale, compiler implementation, and applications. ACM Trans. Program. Lang. Syst. 28 (3) (2006)
Gary T. Leavens
Not a Number of Floating Point Problems. J. Object Technol. 5 (2) (2006)
Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby
Extending JML for Modular Specification and Verification of Multi-threaded Programs. ECOOP (2005)
Yoonsik Cheon, Gary T. Leavens
A contextual interpretation of undefinedness for runtime assertion checking. AADEBUG (2005)
Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, Erik Poll
Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. FMCO (2005)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok
How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55 (1-3) (2005)
Gary T. Leavens, Curtis Clifton
Lessons from the JML Project. VSTTE (2005)
Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, Stephen H. Edwards
Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exp. 35 (6) (2005)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll
An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7 (3) (2005)
Gary T. Leavens
Invited Talk: JML framed! PASTE (2004)
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino, Erik Poll
An overview of JML tools and applications. Electron. Notes Theor. Comput. Sci. 80 (2003)
Peter Müller, Arnd Poetzsch-Heffter, Gary T. Leavens
Modular specification of frame properties in JML. Concurr. Comput. Pract. Exp. 15 (2) (2003)
Susan Eisenbach, Gary T. Leavens, Peter Müller, Arnd Poetzsch-Heffter, Erik Poll
Formal Techniques for Java-Like Programs. ECOOP Workshops (2003)
Yoonsik Cheon, Gary T. Leavens
A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. ECOOP (2002)
Sophia Drossopoulou, Susan Eisenbach, Gary T. Leavens, Arnd Poetzsch-Heffter, Erik Poll
Formal Techniques for Java-like Programs. ECOOP Workshops (2002)
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, David R. Cok
How the Design of JML Accomodates Both Runtime Assertion Checking and Formal Verification. FMCO (2002)
Gary T. Leavens, Sophia Drossopoulou, Susan Eisenbach, Arnd Poetzsch-Heffter, Erik Poll
Formal Techniques for Java Programs. ECOOP Workshops (2001)
Susan Eisenbach, Gary T. Leavens
Special issue: formal techniques for Java programs. Concurr. Comput. Pract. Exp. 13 (13) (2001)
Tim Wahls, Gary T. Leavens
Formal semantics of an algorithm for translating model-based specifications to concurrent constraint programs. SAC (2001)
Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, Bart Jacobs
JML (poster session): notations and tools supporting detailed design in Java. OOPSLA Addendum (2000)

Gary T. Leavens.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Gary T. Leavens