Search

Your search keyword '"Leavens, Gary T."' showing total 362 results
Start Over Author "Leavens, Gary T."
362 results on '"Leavens, Gary T."'

1. What Kinds of Contracts Do ML APIs Need?

Author

Khairunnesa, Samantha Syeda, Ahmed, Shibbir, Imtiaz, Sayem Mohammad, Rajan, Hridesh, and Leavens, Gary T.

Subjects
Computer Science - Software Engineering, Computer Science - Machine Learning, Computer Science - Programming Languages
Abstract

Recent work has shown that Machine Learning (ML) programs are error-prone and called for contracts for ML code. Contracts, as in the design by contract methodology, help document APIs and aid API users in writing correct code. The question is: what kinds of contracts would provide the most help to API users? We are especially interested in what kinds of contracts help API users catch errors at earlier stages in the ML pipeline. We describe an empirical study of posts on Stack Overflow of the four most often-discussed ML libraries: TensorFlow, Scikit-learn, Keras, and PyTorch. For these libraries, our study extracted 413 informal (English) API specifications. We used these specifications to understand the following questions. What are the root causes and effects behind ML contract violations? Are there common patterns of ML contract violations? When does understanding ML contracts require an advanced level of ML software expertise? Could checking contracts at the API level help detect the violations in early ML pipeline stages? Our key findings are that the most commonly needed contracts for ML APIs are either checking constraints on single arguments of an API or on the order of API calls. The software engineering community could employ existing contract mining approaches to mine these contracts to promote an increased understanding of ML APIs. We also noted a need to combine behavioral and temporal contract mining approaches. We report on categories of required ML contracts, which may help designers of contract languages., Comment: Accepted for publication at EMSE (Empirical Software Engineering) Journal, 2023

Published
2023

2. Inferring Concise Specifications of APIs

Author

Singleton, John L., Leavens, Gary T., Rajan, Hridesh, and Cok, David R.

Subjects
Computer Science - Software Engineering
Abstract

Modern software relies on libraries and uses them via application programming interfaces (APIs). Correct API usage as well as many software engineering tasks are enabled when APIs have formal specifications. In this work, we analyze the implementation of each method in an API to infer a formal postcondition. Conventional wisdom is that, if one has preconditions, then one can use the strongest postcondition predicate transformer (SP) to infer postconditions. However, SP yields postconditions that are exponentially large, which makes them difficult to use, either by humans or by tools. Our key idea is an algorithm that converts such exponentially large specifications into a form that is more concise and thus more usable. This is done by leveraging the structure of the specifications that result from the use of SP. We applied our technique to infer postconditions for over 2,300 methods in seven popular Java libraries. Our technique was able to infer specifications for 75.7% of these methods, each of which was verified using an Extended Static Checker. We also found that 84.6% of resulting specifications were less than 1/4 page (20 lines) in length. Our technique was able to reduce the length of SMT proofs needed for verifying implementations by 76.7% and reduced prover execution time by 26.7%.

Published
2019
Full Text
View/download PDF

4. Further Lessons from the JML Project

Author

Leavens, Gary T., Cok, David R., Nilizadeh, Amirfarhad, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Ahrendt, Wolfgang, editor, Beckert, Bernhard, editor, Bubel, Richard, editor, and Johnsen, Einar Broch, editor

Published
2022
Full Text
View/download PDF

5. Using a Guided Fuzzer and Preconditions to Achieve Branch Coverage with Valid Inputs

Author

Nilizadeh, Amirfarhad, Leavens, Gary T., Păsăreanu, Corina S., Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Loulergue, Frédéric, editor, and Wotawa, Franz, editor

Published
2021
Full Text
View/download PDF

9. A Layered Approach to Specification Authoring, Sharing, and Usage

Author

Singleton, John L., Leavens, Gary T., Kacprzyk, Janusz, Series editor, Pal, Nikhil R., Advisory editor, Bello Perez, Rafael, Advisory editor, Corchado, Emilio S., Advisory editor, Hagras, Hani, Advisory editor, Kóczy, László T., Advisory editor, Kreinovich, Vladik, Advisory editor, Lin, Chin-Teng, Advisory editor, Lu, Jie, Advisory editor, Melin, Patricia, Advisory editor, Nedjah, Nadia, Advisory editor, Nguyen, Ngoc Thanh, Advisory editor, Wang, Jun, Advisory editor, Rubin, Stuart H., editor, and Bouabana-Tebibel, Thouraya, editor

Published
2018
Full Text
View/download PDF

10. An Illustrated Guide to the Model Theory of Supertype Abstraction and Behavioral Subtyping

Author

Leavens, Gary T., Naumann, David A., Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Weikum, Gerhard, Series Editor, Bowen, Jonathan P., editor, Liu, Zhiming, editor, and Zhang, Zili, editor

Published
2018
Full Text
View/download PDF

16. Specifying and Verifying Advanced Control Features

Author

Leavens, Gary T., Naumann, David, Rajan, Hridesh, Aotani, Tomoyuki, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Margaria, Tiziana, editor

Published
2016
Full Text
View/download PDF

20. Separating Obligations of Subjects and Handlers for More Flexible Event Type Verification

Author

Sánchez, José, Leavens, Gary T., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Binder, Walter, editor, Bodden, Eric, editor, and Löwe, Welf, editor

Published
2013
Full Text
View/download PDF

21. The 1st Verified Software Competition: Experience Report

Author

Klebanov, Vladimir, Müller, Peter, Shankar, Natarajan, Leavens, Gary T., Wüstholz, Valentin, Alkassar, Eyad, Arthan, Rob, Bronish, Derek, Chapman, Rod, Cohen, Ernie, Hillebrand, Mark, Jacobs, Bart, Leino, K. Rustan M., Monahan, Rosemary, Piessens, Frank, Polikarpova, Nadia, Ridge, Tom, Smans, Jan, Tobies, Stephan, Tuerk, Thomas, Ulbrich, Mattias, Weiß, Benjamin, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Butler, Michael, editor, and Schulte, Wolfram, editor

Published
2011
Full Text
View/download PDF

22. Formal Techniques for Java-Like Programs : Report on the 10th Workshop FTfJP at ECOOP 2008

Author

Albert, Elvira, Banerjee, Anindya, Drossopoulou, Sophia, Huisman, Marieke, Igarashi, Atsushi, Leavens, Gary T., Müller, Peter, Wrigstad, Tobias, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Eugster, Patrick, editor

Published
2009
Full Text
View/download PDF

23. Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services

Author

Rajan, Hridesh, Tao, Jia, Shaner, Steve, Leavens, Gary T., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Castagna, Giuseppe, editor

Published
2009
Full Text
View/download PDF

24. Ptolemy: A Language with Quantified, Typed Events

Author

Rajan, Hridesh, Leavens, Gary T., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Vitek, Jan, editor

Published
2008
Full Text
View/download PDF

25. Lessons from the JML Project

Author

Leavens, Gary T., Clifton, Curtis, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Meyer, Bertrand, editor, and Woodcock, Jim, editor

Published
2008
Full Text
View/download PDF

27. MAO: Ownership and Effects for More Effective Reasoning About Aspects

Author

Clifton, Curtis, Leavens, Gary T., Noble, James, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Ernst, Erik, editor

Published
2007
Full Text
View/download PDF

28. Formal Techniques for Java-Like Programs : Report on the WS FTfJP at ECOOP’06

Author

Ancona, Davide, Drossopoulou, Sophia, Igarashi, Atsushi, Leavens, Gary T., Poetzsch-Heffter, Arnd, Zucca, Elena, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Rangan, C. Pandu, editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Südholt, Mario, editor, and Consel, Charles, editor

Published
2007
Full Text
View/download PDF

29. JML’s Rich, Inherited Specifications for Behavioral Subtypes

Author

Leavens, Gary T., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Liu, Zhiming, editor, and He, Jifeng, editor

Published
2006
Full Text
View/download PDF

30. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2

Author

Chalin, Patrice, Kiniry, Joseph R., Leavens, Gary T., Poll, Erik, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, de Boer, Frank S., editor, Bonsangue, Marcello M., editor, Graf, Susanne, editor, and de Roever, Willem-Paul, editor

Published
2006
Full Text
View/download PDF

31. Extending JML for Modular Specification and Verification of Multi-threaded Programs

Author

Rodríguez, Edwin, Dwyer, Matthew, Flanagan, Cormac, Hatcliff, John, Leavens, Gary T., Robby, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, and Black, Andrew P., editor

Published
2005
Full Text
View/download PDF

35. Formal Techniques for Java-Like Programs

Author

Eisenbach, Susan, Leavens, Gary T., Müller, Peter, Poetzsch-Heffter, Arnd, Poll, Erik, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Buschmann, Frank, editor, Buchmann, Alejandro P., editor, and Cilia, Mariano A., editor

Published
2004
Full Text
View/download PDF

38. Formal Techniques for Java Programs

Author

Leavens, Gary T., Drossopoulou, Sophia, Eisenbach, Susan, Poetzsch-Heffter, Arnd, Poll, Erik, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, and Frohner, Ákos, editor

Published
2002
Full Text
View/download PDF

39. Formal Techniques for Java-like Programs

Author

Drossopoulou, Sophia, Eisenbach, Susan, Leavens, Gary T., Poetzsch-Heffter, Arnd, Poll, Erik, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Hernández, Juan, editor, and Moreira, Ana, editor

Published
2002
Full Text
View/download PDF

40. Formal Techniques for Java Programs

Author

Drossopoulou, Sophia, Eisenbach, Susan, Jacobs, Bart, Leavens, Gary T., Müller, Peter, Poetzsch-Heffter, 1Arnd, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Malenfant, Jacques, editor, Moisan, Sabine, editor, and Moreira, Ana, editor

Published
2000
Full Text
View/download PDF

43. Formal Techniques for Java Programs

Author

Jacobs, Bart, Leavens, Gary T., Müller, Peter, Poetzsch-Heffter, Arnd, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Demeyer, Serge, and Moreira, Ana, editor

Published
1999
Full Text
View/download PDF

47. Programming Is Writing: Why Programs Must Be Carefully Evaluated.

Author

Leavens, Gary T., Baker, Albert L., and Honavar, Vasant

Abstract

Discusses the reasons for careful evaluation of students' programs by a skilled programmer. Suggests that grades for programs must be partly based on quality factors such as clarity, organization, conciseness, and maintainability. (ASK)

Published
1998

50. Aiding Self-Motivation with Readings in Introductory Computing.

Author

Leavens, Gary T.

Abstract

Advocates discussion of self-motivation and its importance with computing majors, suggests wide reading in computing as a way to encourage majors to promote their own self-motivation and interest, and offers specific reading suggestions. (10 references) (MKR)

Published
1995

Catalog

Books, media, physical & digital resources
See catalog results