Publication

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis

Publications associées (49)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Querypoint Debugging

Claude Petitpierre, Salman Mirghasemi

To fix a bug, software developers have to examine the bug-gy execution to locate defects. They employ different ap-proaches (e.g., setting breakpoints, inserting printing statements in the code) to navigate over buggy execution and inspect program state at ...

2010

Proving Memory Safety of Floating-Point Computations by Combining Static and Dynamic Program Analysis

Johannes Kinder

Whitebox fuzzing is a novel form of security testing based on runtime symbolic execution and constraint solving. Over the last couple of years, whitebox fuzzers have found dozens of new security vulnerabilities (buffer overflows) in Windows and Linux appli ...

Microsoft Research2009

Programming language abstractions for mobile code

Stéphane Micheloud

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and suppor ...

EPFL2009

Robust Dynamically Deployed Static Analysis for Java

Sebastian Gfeller

Guaranteeing the absence of errors in a program is a great challenge and many static analysis techniques have been developed to see whether a program is correct before we run it. There is, however, a whole class of programs that are especially difficult to ...

2009

Selective Symbolic Execution

George Candea, Cristian Zamfir, Vitaly Chipounov

Symbolic execution is a powerful technique for analyzing program behavior, finding bugs, and generating tests, but suffers from severely limited scalability: the largest programs that can be symbolically executed today are on the order of thousands of line ...

2009

LFI: A Practical and General Library-Level Fault Injector

George Candea, Paul Dan Marinescu

Fault injection, a critical aspect of testing robust systems, is often overlooked in the development of general-purpose software. We believe this is due to the absence of easy-to-use tools and to the extensive manual labor required to perform fault injecti ...

2009

Runtime Checking for Separation Logic

Viktor Kuncak

Separation logic is a popular approach for specifying properties of recursive mutable data structures. Several existing systems verify a subclass of separation logic specifications using static analysis techniques. Checking data structure specifications du ...

Springer2008

Program Analysis with Dynamic Precision Adjustment

Dirk Thilo Beyer, Grégory Théoduloz

We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a ...

IEEE2008

Proving non-termination

Andrey Rybalchenko, Ashutosh Kumar Gupta

The search for proof and the search for counterexamples (bugs) are complementary activities that need to be pursued concurrently in order to maximize the practical success rate of verification tools. While this is well-understood in safety verification, th ...

2008

Runtime Checking for Separation Logic

Viktor Kuncak

2007