Search Results

Documents authored by Sen, Koushik

Document
DOI: 10.4230/LIPIcs.ECOOP.2016.1
Trace Typing: An Approach for Evaluating Retrofitted Type Systems

Authors: Esben Andreasen, Colin S. Gordon, Satish Chandra, Manu Sridharan, Frank Tip, and Koushik Sen

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
Recent years have seen growing interest in the retrofitting of type systems onto dynamically-typed programming languages, in order to improve type safety, programmer productivity, or performance. In such cases, type system developers must strike a delicate balance between disallowing certain coding patterns to keep the type system simple, or including them at the expense of additional complexity and effort. Thus far, the process for designing retrofitted type systems has been largely ad hoc, because evaluating multiple variations of a type system on large bodies of existing code is a significant undertaking. We present trace typing: a framework for automatically and quantitatively evaluating variations of a retrofitted type system on large code bases. The trace typing approach involves gathering traces of program executions, inferring types for instances of variables and expressions occurring in a trace, and merging types according to merge strategies that reflect specific (combinations of) choices in the source-level type system design space. We evaluated trace typing through several experiments. We compared several variations of type systems retrofitted onto JavaScript, measuring the number of program locations with type errors in each case on a suite of over fifty thousand lines of JavaScript code. We also used trace typing to validate and guide the design of a new retrofitted type system that enforces fixed object layout for JavaScript objects. Finally, we leveraged the types computed by trace typing to automatically identify tag tests --- dynamic checks that refine a type --- and examined the variety of tests identified.
Cite as

Esben Andreasen, Colin S. Gordon, Satish Chandra, Manu Sridharan, Frank Tip, and Koushik Sen. Trace Typing: An Approach for Evaluating Retrofitted Type Systems. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 1:1-1:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{andreasen_et_al:LIPIcs.ECOOP.2016.1,
  author =	{Andreasen, Esben and Gordon, Colin S. and Chandra, Satish and Sridharan, Manu and Tip, Frank and Sen, Koushik},
  title =	{{Trace Typing: An Approach for Evaluating Retrofitted Type Systems}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{1:1--1:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.1},
  URN =		{urn:nbn:de:0030-drops-60952},
  doi =		{10.4230/LIPIcs.ECOOP.2016.1},
  annote =	{Keywords: Retrofitted type systems, Type system design, trace typing}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.519
The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript

Authors: Michael Pradel and Koushik Sen

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
Most popular programming languages support situations where a value of one type is converted into a value of another type without any explicit cast. Such implicit type conversions, or type coercions, are a highly controversial language feature. Proponents argue that type coercions enable writing concise code. Opponents argue that type coercions are error-prone and that they reduce the understandability of programs. This paper studies the use of type coercions in JavaScript, a language notorious for its widespread use of coercions. We dynamically analyze hundreds of programs, including real-world web applications and popular benchmark programs. We find that coercions are widely used (in 80.42% of all function executions) and that most coercions are likely to be harmless (98.85%). Furthermore, we identify a set of rarely occurring and potentially harmful coercions that safer subsets of JavaScript or future language designs may want to disallow. Our results suggest that type coercions are significantly less evil than commonly assumed and that analyses targeted at real-world JavaScript programs must consider coercions.
Cite as

Michael Pradel and Koushik Sen. The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 519-541, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{pradel_et_al:LIPIcs.ECOOP.2015.519,
  author =	{Pradel, Michael and Sen, Koushik},
  title =	{{The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{519--541},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.519},
  URN =		{urn:nbn:de:0030-drops-52367},
  doi =		{10.4230/LIPIcs.ECOOP.2015.519},
  annote =	{Keywords: Types, Type coercions, JavaScript, Dynamically typed languages}
}
Document
DOI: 10.4230/DagRep.4.10.98
Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442)

Authors: Christian Cadar, Vijay Ganesh, Raimondas Sasnauskas, and Koushik Sen

Published in: Dagstuhl Reports, Volume 4, Issue 10 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14442 "Symbolic Execution and Constraint Solving", whose main goals were to bring together leading researchers in the fields of symbolic execution and constraint solving, foster greater communication between these two communities and exchange ideas about new research directions in these fields. There has been a veritable revolution over the last decade in the symbiotic fields of constraint solving and symbolic execution. Even though key ideas behind symbolic execution were introduced more than three decades ago, it was only recently that these techniques became practical as a result of significant advances in constraint satisfiability and scalable combinations of concrete and symbolic execution. Thanks to these advances, testing and analysis techniques based on symbolic execution are having a major impact on many sub-fields of software engineering, computer systems, security, and others. New applications such as program and document repair are being enabled, while older applications such as model checking are being super-charged. Additionally, significant and fast-paced advances are being made in research at the intersection of traditional program analysis, symbolic execution and constraint solving. Therefore, this seminar brought together researchers in these varied fields in order to further facilitate collaborations that take advantage of this unique and fruitful confluence of ideas from the fields of symbolic execution and constraint solving.
Cite as

Christian Cadar, Vijay Ganesh, Raimondas Sasnauskas, and Koushik Sen. Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442). In Dagstuhl Reports, Volume 4, Issue 10, pp. 98-114, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{cadar_et_al:DagRep.4.10.98,
  author =	{Cadar, Christian and Ganesh, Vijay and Sasnauskas, Raimondas and Sen, Koushik},
  title =	{{Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442)}},
  pages =	{98--114},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{10},
  editor =	{Cadar, Christian and Ganesh, Vijay and Sasnauskas, Raimondas and Sen, Koushik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.10.98},
  URN =		{urn:nbn:de:0030-drops-48940},
  doi =		{10.4230/DagRep.4.10.98},
  annote =	{Keywords: Symbolic Execution, Software Testing, Automated Program Analysis, Constraint Solvers}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact