Demonstration venue · read-only. Every page can be browsed; the buttons that would change it are switched off. Create an account to run TaxoReview on your own data. A simulation from public publication records: the people listed were not invited and did not agree to review.

Adam Kiezun

dblp:85/6735 · DBLP profile ↗
← Back
19ranked-venue papers
5as first author
0since 2021 · last 2020
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 16 · 5 first-authorApplied, interdisciplinary, general and emerging computing · 2Databases, data management, data science and information retrieval · 1Human-computer interaction and ubiquitous computing · 1Theory of computation · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Software engineering, system software, and programming languages
14 papers
Program analysis · 42% Software testing · 33% Programming languages and type systems · 12%
Theoretical computer science
2 papers
Automated reasoning and model checking · 100%
Network and information security
3 papers
Web and mobile security · 73% Systems and software security · 27%
Interdisciplinary, comprehensive, and emerging computing
1 paper
Bioinformatics and computational biology · 100%

Topics — the 30 heaviest of 34, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Program analysis › constraint solving
string constraint solving
0.742019
Theory and practice of string solvers (invited talk abstract) · ISSTA 2019
HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars · ACM Trans. Softw. Eng. Methodol. 2012
HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection · CAV 2011
Program analysis
constraint solving
0.632019
Theory and practice of string solvers (invited talk abstract) · ISSTA 2019
HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars · ACM Trans. Softw. Eng. Methodol. 2012
HAMPI: a solver for string constraints · ISSTA 2009
Automated reasoning and model checking › constraint solving
string constraint solving
0.412019
Theory and practice of string solvers (invited talk abstract) · ISSTA 2019
Software testing › test generation
dynamic test generation
0.332010
Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking · IEEE Trans. Software Eng. 2010
Grammar-based whitebox fuzzing · PLDI 2008
Finding bugs in dynamic web applications · ISSTA 2008
Software testing
test generation
0.332010
Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking · IEEE Trans. Software Eng. 2010
Grammar-based whitebox fuzzing · PLDI 2008
Finding bugs in dynamic web applications · ISSTA 2008
Software maintenance and evolution
refactoring
0.342011
Refactoring using type constraints · ACM Trans. Program. Lang. Syst. 2011
Refactoring for Parameterizing Java Classes · ICSE 2007
Refactoring for generalization using type constraints · OOPSLA 2003
Program analysis
dynamic analysis
0.222010
Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking · IEEE Trans. Software Eng. 2010
Combined static and dynamic mutability analysis · ASE 2007
Programming languages and type systems › type systems
type constraints
0.222011
Refactoring using type constraints · ACM Trans. Program. Lang. Syst. 2011
Refactoring for generalization using type constraints · OOPSLA 2003
Bioinformatics and computational biology
proteomics
0.112012
Network-based inference from complex proteomic mixtures using SNIPE · Bioinform. 2012
Software testing
automated testing
0.112012
HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars · ACM Trans. Softw. Eng. Methodol. 2012
Software testing › test input generation
concolic testing
0.112012
HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars · ACM Trans. Softw. Eng. Methodol. 2012
Programming languages and type systems › type systems › subtyping
subtype constraints
0.112011
Refactoring using type constraints · ACM Trans. Program. Lang. Syst. 2011
Software testing
test input generation
0.112011
HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection · CAV 2011
Web and mobile security
web application vulnerability
0.122009
Automatic creation of SQL Injection and cross-site scripting attacks · ICSE 2009
Finding bugs in dynamic web applications · ISSTA 2008
Program verification › model checking
explicit-state model checking
0.112010
Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking · IEEE Trans. Software Eng. 2010
Program verification
model checking
0.112010
Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking · IEEE Trans. Software Eng. 2010
Web and mobile security › web security
cross-site scripting
0.112009
Automatic creation of SQL Injection and cross-site scripting attacks · ICSE 2009
Systems and software security › exploitation › injection attacks
SQL injection
0.112009
Automatic creation of SQL Injection and cross-site scripting attacks · ICSE 2009
Automated reasoning and model checking
satisfiability
0.112009
HAMPI: a solver for string constraints · ISSTA 2009
Program analysis › static analysis
bug detection
0.112008
Finding bugs in dynamic web applications · ISSTA 2008
Software testing › fault detection
crash detection
0.112008
Finding bugs in dynamic web applications · ISSTA 2008
Software testing › test generation
grammar-based test generation
0.112008
Grammar-based whitebox fuzzing · PLDI 2008
Software testing
web application testing
0.112008
Finding bugs in dynamic web applications · ISSTA 2008
Software testing › fuzzing
whitebox fuzzing
0.112008
Grammar-based whitebox fuzzing · PLDI 2008
Program analysis
static analysis
0.112007
Combined static and dynamic mutability analysis · ASE 2007
Programming languages and type systems
type systems
0.112007
Object and reference immutability using java generics · ESEC/SIGSOFT FSE 2007
Programming languages and type systems › type systems › polymorphism
generics
0.122007
Converting java programs to use generic libraries · OOPSLA 2004
Object and reference immutability using java generics · ESEC/SIGSOFT FSE 2007
Software maintenance and evolution › software reengineering › software modernization › software migration
legacy system migration
0.012004
Converting java programs to use generic libraries · OOPSLA 2004
Programming languages and type systems › type systems › polymorphism
parametric polymorphism
0.012004
Converting java programs to use generic libraries · OOPSLA 2004
Bioinformatics and computational biology › proteomics
shotgun proteomics
0.012012
Network-based inference from complex proteomic mixtures using SNIPE · Bioinform. 2012

Methods — techniques the papers use, named apart from their topics

constraint solving · 1.2word equations · 0.3context-free grammar · 0.3concolic execution · 0.3type inference · 0.2HTML validation · 0.2regular expressions · 0.1regular expression · 0.1permutation test · 0.1network propagation · 0.1string constraint solving · 0.1explicit-state model checking · 0.1symbolic execution · 0.1
YearPublicationVenuePosition
2020 Subjective Search Intent Predictions using Customer Reviews
abstract
Query intent prediction is a component of information retrieval which improves result relevance through an understanding of latent user intents in addition to explicit query keywords. We target context-of-use intents, such as the activity for which a product is used and the target audience for a product, which are subjective and not usually indexed as product attributes in the catalog. We describe a method to predict latent query intents: we extract intents from product reviews on amazon.com and, using behavioral purchase signals that associate queries with the reviewed products, train query classifiers that label queries with the intents extracted from reviews. For example, we predict the activity "running" for the query "adidas mens pants." We show that our method can predict latent intents not indexed directly in the product catalog.
Adrian Boteanu, Emily Dutile, Adam Kiezun, Shay Artzi
CHIIR3
2019 Theory and practice of string solvers (invited talk abstract)
abstract
The paper titled "Hampi: A Solver for String Constraints" was published in the proceedings of the International Symposium on Software Testing and Analysis (ISSTA) 2009, and has been selected to receive the ISSTA 2019 Impact Paper Award. The paper describes HAMPI, one of the first practical solver aimed at solving the satisfiability problem for a theory of string (word) equations, operations over strings, predicates over regular expressions and context-free grammars. HAMPI has been used widely to solve many software engineering and security problems, and has inspired considerable research on string solving algorithms and their applications.
Adam Kiezun, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst, Vijay Ganesh 0001
ISSTA1
2012 Network-based inference from complex proteomic mixtures using SNIPE
abstract
MOTIVATION: Proteomics presents the opportunity to provide novel insights about the global biochemical state of a tissue. However, a significant problem with current methods is that shotgun proteomics has limited success at detecting many low abundance proteins, such as transcription factors from complex mixtures of cells and tissues. The ability to assay for these proteins in the context of the entire proteome would be useful in many areas of experimental biology. RESULTS: We used network-based inference in an approach named SNIPE (Software for Network Inference of Proteomics Experiments) that selectively highlights proteins that are more likely to be active but are otherwise undetectable in a shotgun proteomic sample. SNIPE integrates spectral counts from paired case-control samples over a network neighbourhood and assesses the statistical likelihood of enrichment by a permutation test. As an initial application, SNIPE was able to select several proteins required for early murine tooth development. Multiple lines of additional experimental evidence confirm that SNIPE can uncover previously unreported transcription factors in this system. We conclude that SNIPE can enhance the utility of shotgun proteomics data to facilitate the study of poorly detected proteins in complex mixtures. AVAILABILITY AND IMPLEMENTATION: An implementation for the R statistical computing environment named snipeR has been made freely available at http://genetics.bwh.harvard.edu/snipe/. CONTACT: [email protected] SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.
David P. Nusinow, Adam Kiezun, Daniel J. O'Connell, Joel M. Chick, Yingzi Yue, Richard L. Maas, Steven Gygi, Shamil R. Sunyaev
Bioinform.2
2012 HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars
abstract
Many automatic testing, analysis, and verification techniques for programs can be effectively reduced to a constraint-generation phase followed by a constraint-solving phase. This separation of concerns often leads to more effective and maintainable software reliability tools. The increasing efficiency of off-the-shelf constraint solvers makes this approach even more compelling. However, there are few effective and sufficiently expressive off-the-shelf solvers for string constraints generated by analysis of string-manipulating programs, so researchers end up implementing their own ad-hoc solvers. To fulfill this need, we designed and implemented Hampi, a solver for string constraints over bounded string variables. Users of Hampi specify constraints using regular expressions, context-free grammars, equality between string terms, and typical string operations such as concatenation and substring extraction. Hampi then finds a string that satisfies all the constraints or reports that the constraints are unsatisfiable. We demonstrate Hampi's expressiveness and efficiency by applying it to program analysis and automated testing. We used Hampi in static and dynamic analyses for finding SQL injection vulnerabilities in Web applications with hundreds of thousands of lines of code. We also used Hampi in the context of automated bug finding in C programs using dynamic systematic testing (also known as concolic testing). We then compared Hampi with another string solver, CFGAnalyzer, and show that Hampi is several times faster. Hampi's source code, documentation, and experimental data are available at http://people.csail.mit.edu/akiezun/hampi 1
Adam Kiezun, Vijay Ganesh 0001, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst
ACM Trans. Softw. Eng. Methodol.1
2011 HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection
Vijay Ganesh 0001, Adam Kiezun, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst
CAV2
2011 Refactoring using type constraints
abstract
Type constraints express subtype relationships between the types of program expressions, for example, those relationships that are required for type correctness. Type constraints were originally proposed as a convenient framework for solving type checking and type inference problems. This paper shows how type constraints can be used as the basis for practical refactoring tools. In our approach, a set of type constraints is derived from a type-correct program P . The main insight behind our work is the fact that P constitutes just one solution to this constraint system, and that alternative solutions may exist that correspond to refactored versions of P . We show how a number of refactorings for manipulating types and class hierarchies can be expressed naturally using type constraints. Several refactorings in the standard distribution of Eclipse are based on our work.
Frank Tip, Robert M. Fuhrer, Adam Kiezun, Michael D. Ernst, Ittai Balaban, Bjorn De Sutter
ACM Trans. Program. Lang. Syst.3
2010 Finding Bugs in Web Applications Using Dynamic Test Generation and Explicit-State Model Checking
abstract
Web script crashes and malformed dynamically generated webpages are common errors, and they seriously impact the usability of Web applications. Current tools for webpage validation cannot handle the dynamically generated pages that are ubiquitous on today's Internet. We present a dynamic test generation technique for the domain of dynamic Web applications. The technique utilizes both combined concrete and symbolic execution and explicit-state model checking. The technique generates tests automatically, runs the tests capturing logical constraints on inputs, and minimizes the conditions on the inputs to failing tests so that the resulting bug reports are small and useful in finding and fixing the underlying faults. Our tool Apollo implements the technique for the PHP programming language. Apollo generates test inputs for a Web application, monitors the application for crashes, and validates that the output conforms to the HTML specification. This paper presents Apollo's algorithms and implementation, and an experimental evaluation that revealed 673 faults in six PHP Web applications.
Shay Artzi, Adam Kiezun, Julian Dolby, Frank Tip, Danny Dig, Amit M. Paradkar, Michael D. Ernst
IEEE Trans. Software Eng.2
2009 Automatic creation of SQL Injection and cross-site scripting attacks
abstract
We present a technique for finding security vulnerabilities in Web applications. SQL Injection (SQLI) and cross-site scripting (XSS) attacks are widespread forms of attack in which the attacker crafts the input to the application to access or modify user data and execute malicious code. In the most serious attacks (called second-order, or persistent, XSS), an attacker can corrupt a database so as to cause subsequent users to execute malicious code.
Adam Kiezun, Philip J. Guo, Karthick Jayaraman, Michael D. Ernst
ICSE1
2009 HAMPI: a solver for string constraints
abstract
Many automatic testing, analysis, and verification techniques for programs can be effectively reduced to a constraint generation phase followed by a constraint-solving phase. This separation of concerns often leads to more effective and maintainable tools. The increasing efficiency of off-the-shelf constraint solvers makes this approach even more compelling. However, there are few effective and sufficiently expressive off-the-shelf solvers for string constraints generated by analysis techniques for string-manipulating programs.
Adam Kiezun, Vijay Ganesh 0001, Philip J. Guo, Pieter Hooimeijer, Michael D. Ernst
ISSTA1
2009 Parameter reference immutability: formal definition, inference tool, and comparison
Shay Artzi, Adam Kiezun, Jaime Quinonez, Michael D. Ernst
Autom. Softw. Eng.2
2008 Finding bugs in dynamic web applications
abstract
Web script crashes and malformed dynamically-generated Web pages are common errors, and they seriously impact usability of Web applications. Current tools for Web-page validation cannot handle the dynamically-generated pages that are ubiquitous on today's Internet. In this work, we apply a dynamic test generation technique, based on combined concrete and symbolic execution, to the domain of dynamic Web applications. The technique generates tests automatically, uses the tests to detect failures, and minimizes the conditions on the inputs exposing each failure, so that the resulting bug reports are small and useful in finding and fixing the underlying faults. Our tool Apollo implements the technique for PHP. Apollo generates test inputs for the Web application, monitors the application for crashes, and validates that the output conforms to the HTML specification. This paper presents Apollo's algorithms and implementation, and an experimental evaluation that revealed 214 faults in 4 PHP Web applications.
Shay Artzi, Adam Kiezun, Julian Dolby, Frank Tip, Danny Dig, Amit M. Paradkar, Michael D. Ernst
ISSTA2
2008 Grammar-based whitebox fuzzing
abstract
Whitebox fuzzing is a form of automatic dynamic test generation, based on symbolic execution and constraint solving, designed for security testing of large applications. Unfortunately, the current effectiveness of whitebox fuzzing is limited when testing applications with highly-structured inputs, such as compilers and interpreters. These applications process their inputs in stages, such as lexing, parsing and evaluation. Due to the enormous number of control paths in early processing stages, whitebox fuzzing rarely reaches parts of the application beyond those first stages.
Patrice Godefroid, Adam Kiezun, Michael Y. Levin
PLDI2
2008 miRNAminer: A tool for homologous microRNA gene search
abstract
BACKGROUND: MicroRNAs (miRNAs), present in most metazoans, are small non-coding RNAs that control gene expression by negatively regulating translation through binding to the 3'UTR of mRNA transcripts. Previously, experimental and computational methods were used to construct miRNA gene repositories agreeing with careful submission guidelines. RESULTS: An algorithm we developed - miRNAminer - is used for homologous conserved miRNA gene search in several animal species. Given a search query, candidate homologs from different species are tested for their known miRNA properties, such as secondary structure, energy and alignment and conservation, in order to asses their fidelity. When applying miRNAminer on seven mammalian species we identified several hundreds of high-confidence homologous miRNAs increasing the total collection of (miRbase) miRNAs, in these species, by more than 50%. miRNAminer uses stringent criteria and exhibits high sensitivity and specificity. CONCLUSION: We present - miRNAminer - the first web-server for homologous miRNA gene search in animals. miRNAminer can be used to identify conserved homolog miRNA genes and can also be used prior to depositing miRNAs in public databases. miRNAminer is available at http://pag.csail.mit.edu/mirnaminer.
Shay Artzi, Adam Kiezun, Noam Shomron
BMC Bioinform.2
2007 Refactoring for Parameterizing Java Classes
abstract
Type safety and expressiveness of many existing Java libraries and their client applications would improve, if the libraries were upgraded to define generic classes. Efficient and accurate tools exist to assist client applications to use generic libraries, but so far the libraries themselves must be parameterized manually, which is a tedious, time-consuming, and error-prone task. We present a type- constraint-based algorithm for converting non-generic libraries to add type parameters. The algorithm handles the full Java language and preserves backward compatibility, thus making it safe for existing clients. Among other features, it is capable of inferring wildcard types and introducing type parameters for mutually-dependent classes. We have implemented the algorithm as a fully automatic refactoring in Eclipse. We evaluated our work in two ways. First, our tool parameterized code that was lacking type parameters. We contacted the developers of several of these applications, and in all cases they confirmed that the resulting parameterizations were correct and useful. Second, to better quantify its effectiveness, our tool parameterized classes from already-generic libraries, and we compared the results to those that were created by the libraries' authors. Our tool performed the refactoring accurately-in 87% of cases the results were as good as those created manually by a human expert, in 9% of cases the tool results were better, and in 4% of cases the tool results were worse.
Adam Kiezun, Michael D. Ernst, Frank Tip, Robert M. Fuhrer
ICSE1
2007 Combined static and dynamic mutability analysis
abstract
Knowing which method parameters may be mutated during a method's executionis useful for many software engineering tasks. We present an approach todiscovering parameter reference immutability, in which several lightweight, scalable analyses are combined in stages, with each stage refining the overall result. The resulting analysis is scalable and combines the strengths of its component analyses. As one of the component analyses, we present a novel, dynamic mutability analysis and show how its results can be improved by random input generation. Experimental results on programs of up to 185 kLOC show that, compared to previous approaches, our approach increases both scalability and overall accuracy
Shay Artzi, Adam Kiezun, David Glasser, Michael D. Ernst
ASE2
2007 Object and reference immutability using java generics
abstract
A compiler-checked immutability guarantee provides useful documentation, facilitates reasoning, and enables optimizations. This paper presents Immutability Generic Java (IGJ), a novel language extension that expresses immutability without changing Java's syntax by building upon Java's generics and annotation mechanisms. In IGJ, each class has one additional type parameter that is Immutable, Mutable, or ReadOnly. IGJ guarantees both reference immutability (only mutable references can mutate an object) and object immutability (an immutable reference points to an immutable object). IGJ is the first proposal for enforcing object immutability within Java's syntax and type system, and its reference immutability is more expressive than previous work. IGJ also permits covariant changes of type parameters in a type-safe manner, e.g., a readonly list of integers is a subtype of a readonly list of numbers. IGJ extends Java's type system with a few simple rules. We formalize this type system and prove it sound. Our IGJ compiler works by type-erasure and generates byte-code that can be executed on any JVM without runtime penalty.
Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kiezun, Michael D. Ernst
ESEC/SIGSOFT FSE5
2005 Efficiently Refactoring Java Applications to Use Generic Libraries
Robert M. Fuhrer, Frank Tip, Adam Kiezun, Julian Dolby, Markus Keller
ECOOP3
2004 Converting java programs to use generic libraries
abstract
Java 1.5 will include a type system (called JSR-14) that supports parametric polymorphism, or generic classes. This will bring many benefits to Java programmers, not least because current Java practice makes heavy use of logically-generic classes, including container classes.
Alan Donovan, Adam Kiezun, Matthew S. Tschantz, Michael D. Ernst
OOPSLA2
2003 Refactoring for generalization using type constraints
abstract
Refactoring is the process of applying behavior-preserving transformations (called "refactorings") in order to improve a program's design. Associated with a refactoring is a set of preconditions that must be satisfied to guarantee that program behavior is preserved, and a set of source code modifications. An important category of refactorings is concerned with generalization (e.g., Extract Interface for re-routing the access to a class via a newly created interface, and Pull Up Members for moving members into a superclass). For these refactorings, both the preconditions and the set of allowable source code modifications depend on interprocedural relationships between types of variables. We present an approach in which type constraints are used to verify the preconditions and to determine the allowable source code modifications for a number of generalization-related refactorings. This work is implemented in the standard distribution of Eclipse (see www.eclipse.org).
Frank Tip, Adam Kiezun, Dirk Bäumer
OOPSLA2