6 Search Results for "Visser, Willem"


Document
Deep Static Modeling of invokedynamic

Authors: George Fourtounis and Yannis Smaragdakis

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, introduced in Java 8, are a very popular feature, which is, however, resistant to static analysis, since it mixes invokedynamic with dynamic code generation. These techniques invalidate static analysis assumptions: programmable linking breaks reasoning about method resolution while dynamically generated code is, by definition, not available statically. In this paper, we show that a static analysis can predictively model uses of invokedynamic while also cooperating with extra rules to handle the runtime code generation of lambdas. Our approach plugs into an existing static analysis and helps eliminate all unsoundness in the handling of lambdas (including associated features such as method references) and generic invokedynamic uses. We evaluate our technique on a benchmark suite of our own and on third-party benchmarks, uncovering all code previously unreachable due to unsoundness, highly efficiently.

Cite as

George Fourtounis and Yannis Smaragdakis. Deep Static Modeling of invokedynamic. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{fourtounis_et_al:LIPIcs.ECOOP.2019.15,
  author =	{Fourtounis, George and Smaragdakis, Yannis},
  title =	{{Deep Static Modeling of invokedynamic}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{15:1--15:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.15},
  URN =		{urn:nbn:de:0030-drops-108076},
  doi =		{10.4230/LIPIcs.ECOOP.2019.15},
  annote =	{Keywords: static analysis, invokedynamic}
}
Document
Brave New Idea Paper
Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper)

Authors: Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
Many of today’s software systems are parallel or concurrent. With the rise of Node.js and more generally event-loop architectures, many systems need to handle concurrency. However, its non-deterministic behavior makes it hard to reproduce bugs. Today’s interactive debuggers unfortunately do not support developers in debugging non-deterministic issues. They only allow us to explore a single execution path. Therefore, some bugs may never be reproduced in the debugging session, because the right conditions are not triggered. As a solution, we propose multiverse debugging, a new approach for debugging non-deterministic programs that allows developers to observe all possible execution paths of a parallel program and debug it interactively. We introduce the concepts of multiverse breakpoints and stepping, which can halt a program in different execution paths, i.e. universes. We apply multiverse debugging to AmbientTalk, an actor-based language, resulting in Voyager, a multiverse debugger implemented on top of the AmbientTalk operational semantics. We provide a proof of non-interference, i.e., we prove that observing the behavior of a program by the debugger does not affect the behavior of that program and vice versa. Multiverse debugging establishes the foundation for debugging non-deterministic programs interactively, which we believe can aid the development of parallel and concurrent systems.

Cite as

Carmen Torres Lopez, Robbert Gurdeep Singh, Stefan Marr, Elisa Gonzalez Boix, and Christophe Scholliers. Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 27:1-27:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{torreslopez_et_al:LIPIcs.ECOOP.2019.27,
  author =	{Torres Lopez, Carmen and Gurdeep Singh, Robbert and Marr, Stefan and Gonzalez Boix, Elisa and Scholliers, Christophe},
  title =	{{Multiverse Debugging: Non-Deterministic Debugging for Non-Deterministic Programs}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{27:1--27:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.27},
  URN =		{urn:nbn:de:0030-drops-108192},
  doi =		{10.4230/LIPIcs.ECOOP.2019.27},
  annote =	{Keywords: Debugging, Parallelism, Concurrency, Actors, Formal Semantics}
}
Document
FITE - Future Integrated Testing Environment

Authors: Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser, and Michael W. Whalen

Published in: Dagstuhl Seminar Proceedings, Volume 10111, Practical Software Testing : Tool Automation and Human Factors (2010)


Abstract
It is a well known fact that the later software errors are discovered during the development process, the more costly they are to repair. Recently, automatic tools based on static and dynamic analysis have become widely used in industry to detect errors, such as null pointer dereferences, array indexing errors, assertion violations, etc. However, these techniques are typically applied late in the development cycle, and thus, the errors detected by such approaches are expensive to repair. Additionally, these techniques can suffer from scalability and presentation issues due to the fact that they are applied late in the development cycle. To address these issues we suggest that code should be continuously analyzed from an early stage of development, preferably as the code is written. This will allow developers to get instant feedback to repair errors as they are introduced, rather than later when it is more expensive. This analysis should also be incremental in nature to allow better scaling. Additionally, the presentation of errors in static and dynamic analysis tools can be improved due to the small increment of code being analyzed.

Cite as

Patrice Godefroid, Leonardo Mariani, Andrea Polini, Nikolai Tillmann, Willem Visser, and Michael W. Whalen. FITE - Future Integrated Testing Environment. In Practical Software Testing : Tool Automation and Human Factors. Dagstuhl Seminar Proceedings, Volume 10111, pp. 1-7, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{godefroid_et_al:DagSemProc.10111.5,
  author =	{Godefroid, Patrice and Mariani, Leonardo and Polini, Andrea and Tillmann, Nikolai and Visser, Willem and Whalen, Michael W.},
  title =	{{FITE - Future Integrated Testing Environment}},
  booktitle =	{Practical Software Testing : Tool Automation and Human Factors},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10111},
  editor =	{Mark Harman and Henry Muccini and Wolfram Schulte and Tao Xie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10111.5},
  URN =		{urn:nbn:de:0030-drops-26191},
  doi =		{10.4230/DagSemProc.10111.5},
  annote =	{Keywords: Incremental analysis, incremental testing, human factors, static analysis, model checking}
}
Document
06172 Abstracts Collection – Directed Model Checking

Authors: Stefan Edelkamp, Stefan Leue, and Willem Visser

Published in: Dagstuhl Seminar Proceedings, Volume 6172, Directed Model Checking (2007)


Abstract
From 26.04.06 to 29.04.06, the Dagstuhl Seminar 06172 ``Directed Model Checking'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Stefan Edelkamp, Stefan Leue, and Willem Visser. 06172 Abstracts Collection – Directed Model Checking. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{edelkamp_et_al:DagSemProc.06172.1,
  author =	{Edelkamp, Stefan and Leue, Stefan and Visser, Willem},
  title =	{{06172 Abstracts Collection – Directed Model Checking}},
  booktitle =	{Directed Model Checking},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.1},
  URN =		{urn:nbn:de:0030-drops-9469},
  doi =		{10.4230/DagSemProc.06172.1},
  annote =	{Keywords: Model Checking, Artificial Intelligence, AI Plannning, Guided Traversal, State Explosion Problem}
}
Document
06172 Executive Summary – Directed Model Checking

Authors: Stefan Edelkamp, Stefan Leue, and Willem Visser

Published in: Dagstuhl Seminar Proceedings, Volume 6172, Directed Model Checking (2007)


Abstract
This is a summary of the Dagstuhl Seminar 06172 {em Directed Model Checking} that was held 26 - 29 April 2006 at Schloss Dagstuhl, Germany. Directed Model Checking is a software and hardware verification technique that performs a systematic, heuristics guided search of the state space of the model to be analyzed. It hence reconciles classical model checking technology with intelligent, heuristics driven search that has a long tradition in artificial intelligence, in particular in the area of action planning. The benefits are short or even optimally short error trails, in some instances a more efficient exploration of the state space, and the applicability of state space search in some application areas in which unintelligent search would not yield useful results. The seminar brought together researchers from the system verification and the artificial intelligence domain in order to discuss the current state of the art, and to elicit and discuss research challenges and future directions.

Cite as

Stefan Edelkamp, Stefan Leue, and Willem Visser. 06172 Executive Summary – Directed Model Checking. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{edelkamp_et_al:DagSemProc.06172.2,
  author =	{Edelkamp, Stefan and Leue, Stefan and Visser, Willem},
  title =	{{06172 Executive Summary – Directed Model Checking}},
  booktitle =	{Directed Model Checking},
  pages =	{1--8},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.2},
  URN =		{urn:nbn:de:0030-drops-9443},
  doi =		{10.4230/DagSemProc.06172.2},
  annote =	{Keywords: Model checking, heuristics, state space search, software and hardware verification}
}
Document
Efficient Software Model Checking of Data Structure Properties

Authors: Chandrasekhar Boyapati and Paul Darga

Published in: Dagstuhl Seminar Proceedings, Volume 6172, Directed Model Checking (2007)


Abstract
This talk presents novel language and analysis techniques that significantly speed up software model checking of data structure properties. Consider checking a red-black tree implementation. Traditional software model checkers systematically generate all red-black tree states (within some given bounds) and check every red-black tree operation (such as insert, delete, or lookup) on every red-black tree state. Our key idea is as follows. As our checker checks a red-black tree operation $o$ on a red-black tree state $s$, it uses program analysis techniques to identify other red-black tree states $s'_1$, $s'_2$, ..., $s'_k$ on which the operation $o$ behaves similarly. Our analyses guarantee that if $o$ executes correctly on $s$, then $o$ will execute correctly on every $s'_i$. Our checker therefore does not need to check $o$ on any $s'_i$ once it checks $o$ on $s$. It thus safely prunes those state transitions from its search space, while still achieving complete test coverage within the bounded domain. Our preliminary results show {em orders of magnitude improvement} over previous approaches. We believe our techniques can make software model checking significantly faster, and thus enable checking of much larger programs and complex program properties than currently possible.

Cite as

Chandrasekhar Boyapati and Paul Darga. Efficient Software Model Checking of Data Structure Properties. In Directed Model Checking. Dagstuhl Seminar Proceedings, Volume 6172, pp. 1-19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{boyapati_et_al:DagSemProc.06172.3,
  author =	{Boyapati, Chandrasekhar and Darga, Paul},
  title =	{{Efficient Software Model Checking of Data Structure Properties}},
  booktitle =	{Directed Model Checking},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6172},
  editor =	{Stefan Edelkamp and Stefan Leue and Willem Visser},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06172.3},
  URN =		{urn:nbn:de:0030-drops-9450},
  doi =		{10.4230/DagSemProc.06172.3},
  annote =	{Keywords: Software Model Checking, Program Analysis, Linked Data Structures}
}
  • Refine by Author
  • 3 Visser, Willem
  • 2 Edelkamp, Stefan
  • 2 Leue, Stefan
  • 1 Boyapati, Chandrasekhar
  • 1 Darga, Paul
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Concurrent programming languages
  • 1 Software and its engineering → General programming languages
  • 1 Software and its engineering → Software testing and debugging
  • 1 Theory of computation → Program analysis

  • Refine by Keyword
  • 2 static analysis
  • 1 AI Plannning
  • 1 Actors
  • 1 Artificial Intelligence
  • 1 Concurrency
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 3 2007
  • 2 2019
  • 1 2010

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