Search

Your search keyword '"Cok, David"' showing total 128 results
Start Over Author "Cok, David"
128 results on '"Cok, David"'

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

3. Specifying the Boundary Between Unverified and Verified Code

Author

Cok, David R., Leino, K. Rustan M., 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

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. Polymorphic Type Inference for Machine Code

Author

Noonan, Matthew, Loginov, Alexey, and Cok, David

Subjects
Computer Science - Programming Languages, Computer Science - Logic in Computer Science, F.3.2, D.2.7, D.3.3, F.4.3
Abstract

For many compiled languages, source-level types are erased very early in the compilation process. As a result, further compiler passes may convert type-safe source into type-unsafe machine code. Type-unsafe idioms in the original source and type-unsafe optimizations mean that type information in a stripped binary is essentially nonexistent. The problem of recovering high-level types by performing type inference over stripped machine code is called type reconstruction, and offers a useful capability in support of reverse engineering and decompilation. In this paper, we motivate and develop a novel type system and algorithm for machine-code type inference. The features of this type system were developed by surveying a wide collection of common source- and machine-code idioms, building a catalog of challenging cases for type reconstruction. We found that these idioms place a sophisticated set of requirements on the type system, inducing features such as recursively-constrained polymorphic types. Many of the features we identify are often seen only in expressive and powerful type systems used by high-level functional languages. Using these type-system features as a guideline, we have developed Retypd: a novel static type-inference algorithm for machine code that supports recursive types, polymorphism, and subtyping. Retypd yields more accurate inferred types than existing algorithms, while also enabling new capabilities such as reconstruction of pointer const annotations with 98% recall. Retypd can operate on weaker program representations than the current state of the art, removing the need for high-quality points-to information that may be impractical to compute., Comment: Full version with appendices, for PLDI 2016

Published
2016

9. SPEEDY: An Eclipse-based IDE for invariant inference

Author

Cok, David R. and Johnson, Scott C.

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Computer Science - Software Engineering
Abstract

SPEEDY is an Eclipse-based IDE for exploring techniques that assist users in generating correct specifications, particularly including invariant inference algorithms and tools. It integrates with several back-end tools that propose invariants and will incorporate published algorithms for inferring object and loop invariants. Though the architecture is language-neutral, current SPEEDY targets C programs. Building and using SPEEDY has confirmed earlier experience demonstrating the importance of showing and editing specifications in the IDEs that developers customarily use, automating as much of the production and checking of specifications as possible, and showing counterexample information directly in the source code editing environment. As in previous work, automation of specification checking is provided by back-end SMT solvers. However, reducing the effort demanded of software developers using formal methods also requires a GUI design that guides users in writing, reviewing, and correcting specifications and automates specification inference., Comment: In Proceedings F-IDE 2014, arXiv:1404.5785

Published
2014
Full Text
View/download PDF

10. OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse

Author

Cok, David R.

Subjects
Computer Science - Software Engineering, Computer Science - Logic in Computer Science, Computer Science - Programming Languages
Abstract

OpenJML is a tool for checking code and specifications of Java programs. We describe our experience building the tool on the foundation of JML, OpenJDK and Eclipse, as well as on many advances in specification-based software verification. The implementation demonstrates the value of integrating specification tools directly in the software development IDE and in automating as many tasks as possible. The tool, though still in progress, has now been used for several college-level courses on software specification and verification and for small-scale studies on existing Java programs., Comment: In Proceedings F-IDE 2014, arXiv:1404.5785

Published
2014
Full Text
View/download PDF

11. Practical Methods for Reasoning About Java 8’s Functional Programming Features

Author

Cok, David R., Tasiran, Serdar, 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, Piskac, Ruzica, editor, and Rümmer, Philipp, editor

Published
2018
Full Text
View/download PDF

12. Java Automated Deductive Verification in Practice: Lessons from Industrial Proof-Based Projects

Author

Cok, David R., Hutchison, David, Editorial Board Member, Kanade, Takeo, Editorial Board Member, Kittler, Josef, Editorial Board Member, Kleinberg, Jon M., Editorial Board Member, Mattern, Friedemann, Editorial Board Member, Mitchell, John C., Editorial Board Member, Naor, Moni, Editorial Board Member, Pandu Rangan, C., Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Terzopoulos, Demetri, Editorial Board Member, Tygar, Doug, Editorial Board Member, Weikum, Gerhard, Series Editor, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Margaria, Tiziana, editor

Published
2018
Full Text
View/download PDF

13. Runtime Assertion Checking and Static Verification: Collaborative Partners

Author

Maurica, Fonenantsoa, Cok, David R., Signoles, Julien, Hutchison, David, Editorial Board Member, Kanade, Takeo, Editorial Board Member, Kittler, Josef, Editorial Board Member, Kleinberg, Jon M., Editorial Board Member, Mattern, Friedemann, Editorial Board Member, Mitchell, John C., Editorial Board Member, Naor, Moni, Editorial Board Member, Pandu Rangan, C., Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Terzopoulos, Demetri, Editorial Board Member, Tygar, Doug, Editorial Board Member, Weikum, Gerhard, Series Editor, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, and Margaria, Tiziana, editor

Published
2018
Full Text
View/download PDF

15. OpenJML: JML for Java 7 by Extending OpenJDK

Author

Cok, David R., 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, Bobaru, Mihaela, editor, Havelund, Klaus, editor, Holzmann, Gerard J., editor, and Joshi, Rajeev, editor

Published
2011
Full Text
View/download PDF

16. jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2

Author

Cok, David R., 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, Bobaru, Mihaela, editor, Havelund, Klaus, editor, Holzmann, Gerard J., editor, and Joshi, Rajeev, editor

Published
2011
Full Text
View/download PDF

17. ESC/Java2: Uniting ESC/Java and JML : Progress and Issues in Building and Using ESC/Java2, Including a Case Study Involving the Use of the Tool to Verify Portions of an Internet Voting Tally System

Author

Cok, David R., Kiniry, Joseph R., 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, Barthe, Gilles, editor, Burdy, Lilian, editor, Huisman, Marieke, editor, Lanet, Jean-Louis, editor, and Muntean, Traian, editor

Published
2005
Full Text
View/download PDF

23. IntelliJML: a JML plugin for IntelliJ IDEA

Author

Monteiro, Steven, Sokolovas, Erikas, Wittingen, Ellen, Dijk, Tom Van, Huisman, Marieke, Cok, David R., Digital Society Institute, and Formal Methods and Tools

Subjects
Source code, Java, Computer science, IDE, media_common.quotation_subject, Maintainability, Software_PROGRAMMINGTECHNIQUES, Interactive Development Environment, computer.software_genre, Error checking, Software_SOFTWAREENGINEERING, IntelliJ IDEA, Formal specification, Plug-in, Plugin, computer.programming_language, Eclipse, media_common, Syntax (programming languages), JML, Programming language, Java Modelling Language, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, computer, Syntax highlighting
Abstract

Java code can be annotated with formal specifications using the Java Modelling Language (JML). Previous work has provided IDE plugins intended to help write JML, but mostly for the Eclipse IDE. We introduce IntelliJML, a JML plugin for IntelliJ IDEA, with a focus on ease of use and maintainability. Features such as syntax, semantic, and type checking, as well as syntax highlighting and code completion are integrated into the plugin. The plugin can also be extended in the future to add more features. The source code for the plugin can be found at https://gitlab.utwente.nl/fmt/intellijml.

Published
2021
Full Text
View/download PDF

32. Safety in Numbers

Author

Melski, David, primary, Cok, David, primary, Phillips, John, primary, Wisniewski, Scott, primary, Yong, Suan H., primary, Lloyd, Nathan, primary, Kuper, Lindsay, primary, Gopen, Denis, primary, and Loginov, Alexey, primary

Published
2010
Full Text
View/download PDF

38. The 2014 SMT Competition

Author

Weber, Tjark, Cok, David R., Deharbe, David, Weber, Tjark, Cok, David R., and Deharbe, David

Published
2016

43. The 2013 SMT Evaluation

Author

Cok, David R., Stump, Aaron, Weber, Tjark, Cok, David R., Stump, Aaron, and Weber, Tjark

Abstract

After 8 years of SMT Competitions, the SMT Steering Committee decided, for 2013, to sponsor an evaluation of the status of SMT benchmarks and solvers, rather than another competition. This report summarizes the results of the evaluation, conducted by the authors. The key observations are that (1) the competition results are quite sensitive to randomness and (2) the most significant need for the future is assessment and improvement of benchmarks in the light of SMT applications. The evaluation also measured competitiveness of solvers, general coverage of solvers, logics, and benchmarks, and degree of repeatability of measurements and competitions.

Published
2014

46. Lean and Efficient Software: Whole-Program Optimization of Executables

Author

GRAMMATECH INC ITHACA NY, Cok, David, Loginov, Alexey, Johnson, Tom, Alliet, Brian, Yong, Suan, Ciarletta, David, Lim, Junghee, GRAMMATECH INC ITHACA NY, Cok, David, Loginov, Alexey, Johnson, Tom, Alliet, Brian, Yong, Suan, Ciarletta, David, and Lim, Junghee

Abstract

Modern software is typically produced using home-grown or third-party libraries and pre-existing components. Consequently, a finished executable often contains unneeded code, duplicate defensive checks, and extra layers of procedure calls. Such bloat contributes to excess memory footprint, slower performance, and security vulnerabilities (by hosting more return-oriented-programming gadgets an attacker can hijack). The Layer Collapsing project is devising and prototyping techniques to substantially improve the performance, size, and robustness of binary executables. We are using static and dynamic binary program analysis techniques to perform whole-program optimization directly on compiled programs: specializing library subroutines, removing redundant argument checking and interface layers, eliminating dead code, and improving computational efficiency. A tool that successfully implements this goal will dramatically improve the way software is developed and deployed, providing new optimizations available late in the development process or even by the end user., The original document contains color images.

Published
2013

47. Active Learning and Effort Estimation: Finding the Essential Content of Software Effort Estimation Data

Author

Naval Postgraduate School (U.S.), Kocaguneli, Ekrem, Menzies, Tim, Keung, Jacky, Cok, David, Madachy, Ray, Naval Postgraduate School (U.S.), Kocaguneli, Ekrem, Menzies, Tim, Keung, Jacky, Cok, David, and Madachy, Ray

Abstract

Background: Do we always need complex methods for software effort estimation (SEE)? Aim: To characterize the essential content of SEE data, i.e., the least number of features and instances required to capture the information within SEE data. If the essential content is very small, then 1) the contained information must be very brief and 2) the value added of complex learning schemes must be minimal. Method: Our QUICK method computes the euclidean distance between rows (instances) and columns (features) of SEE data, then prunes synonyms (similar features) and outliers (distant instances), then assesses the reduced data by comparing predictions from 1) a simple learner using the reduced data and 2) a state-of-the-art learner (CART) using all data. Performance is measured using hold-out experiments and expressed in terms of mean and median MRE, MAR, PRED(25), MBRE, MIBRE, or MMER. Results: For 18 datasets, QUICK pruned 69 to 96 percent of the training data (median = 89 percent). K ¼ 1 nearest neighbor predictions (in the reduced data) performed as well as CART’s predictions (using all data). Conclusion: The essential content of some SEE datasets is very small. Complex estimation methods may be overelaborate for such datasets and can be simplified. We offer QUICK as an example of such a simpler SEE method.

Published
2013

48. Safety in Numbers

Author

GRAMMATECH INC ITHACA NY, Melski, David, Cok, David, Phillips, John, Wisniewski, Scott, Yong, Suan H., Lloyd, Nathan, Kuper, Lindsay, Gopen, Denis, Loginov, Alexey, GRAMMATECH INC ITHACA NY, Melski, David, Cok, David, Phillips, John, Wisniewski, Scott, Yong, Suan H., Lloyd, Nathan, Kuper, Lindsay, Gopen, Denis, and Loginov, Alexey

Abstract

Using large-scale distributed resources can help find vulnerabilities and malicious code. This project studied the feasibility of distributing two kinds of static analyses of machine code across large-scale donated computational cycles: conventional static analyses for finding bugs and vulnerabilities, and concolic execution to find test cases that trigger rare, possibly maliciously hidden, code paths. We demonstrated that concolic execution is particularly suited to large-scale distributed execution since its core computational loop is very parallelizable and communication costs are small. We assessed a large number of possible parallel architectures and experimented in depth with three. In the process of expanding and scaling our concolic engine for this application, we also devised a means to "fuzz" its semantic representation of machine code and so were able to demonstrate a general technique for validating abstract representations of machine code semantics., The original document contains color images.

Published
2010

Catalog

Books, media, physical & digital resources
See catalog results