Publications by George Candea | EPFL Graph Search

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Debugging real systems is hard, requires deep knowledge of the code, and is time-consuming. Bug reports rarely provide sufficient information, thus forcing developers to turn into detectives searching for an explanation of how the program could have arrive ...

This paper presents S2E, a platform for analyzing the properties and behavior of software systems. We demonstrate S2E's use in developing practical tools for comprehensive performance profiling, reverse engineering of proprietary software, and bug finding ...

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Fault injection-a key technique for testing the robustness of software systems-ends up rarely being used in practice, because it is labor-intensive and one needs to choose between performing random injections (which leads to poor coverage and low represent ...

A critical part of developing a reliable software system is testing its recovery code. This code is traditionally difficult to test in the lab, and, in the field, it rarely gets to run; yet, when it does run, it must execute flawlessly in order to recover ...

Developers rely on automated testing and verification tools to gain confidence in their software. The input to such tools is often generated by compilers that have been designed to generate code that runs fast, not code that can be verified easily and quic ...

We present Communix, a collaborative deadlock immunity framework for Java programs. Deadlock immunity enables applications to avoid deadlocks that they previously encountered. Dimmunix [1], our deadlock immunity system, detects deadlocks and saves their si ...

The boundary between programs and libraries is an appealing location for injecting faults during testing: the cost of doing so is low, and one can emulate a wide range of errors. Several tools exist, but using them faces the challenge of deciding exactly w ...

Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like ...

Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption t ...

One of the most energy-draining and frustrating parts of software development is playing detective with elusive bugs. In this paper we argue that automated post-mortem debugging of failures is feasible for real, in-production systems with no runtime record ...

Reliability of today's software systems hinges on developers writing test cases that exercise as much of a program as possible. Writing and running such tests is inevitably subject to a time budget. This paper addresses the question of how to maximize qual ...

This article presents S2E, a platform for analyzing the properties and behavior of software systems, along with its use in developing tools for comprehensive performance profiling, reverse engineering of proprietary software, and automated testing of kerne ...

The need for high availability and performance in data management systems has been fueling a long running interest in database replication from both academia and industry. However, academic groups often attack replication problems in isolation, overlooking ...

Data races are one of the main causes of concurrency problems in multithreaded programs. Whether all data races are bad, or some are harmful and others are harmless, is still the subject of vigorous scientific debate [Narayanasamy et al. 2007; Boehm 2012]. ...

We present ConfErr, a tool for testing and quantifying the resilience of software systems to human-induced configuration errors. ConfErr uses human error models rooted in psychology and linguistics to generate realistic configuration mistakes; it then inje ...

This paper presents NFOS, a programming model, runtime, and profiler for productively developing software network functions (NFs) that scale on multicore machines. Writing shared-state concurrent systems that are both correct and scalable is still a seriou ...

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

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant man ...

George Candea

Chat with Graph Search

Execution Synthesis: A Technique for Automated Software Debugging

S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems

A Formally Verified NAT

Fast black-box testing of system recovery code

Efficient Testing of Recovery Code Using Fault Injection

-Overify: Optimizing Programs for Fast Verification

Communix: A Framework for Collaborative Deadlock Immunity

Studying Application–Library Interaction and Behavior with LibTrac

High System-Code Security with Low Overhead

A Conjecture Regarding SMT Instability

Automated Debugging for Arbitrarily Long Executions

PathScore-Relevance: A Metric for Improving Test Quality

The S2E Platform: Design, Implementation, and Applications

Middleware-based Database Replication: The Gaps Between Theory and Practice

Automated Classification of Data Races Under Both Strong and Weak Memory Models

ConfErr: A Tool for Assessing Resilience to Human Configuration Errors

Transparent Multicore Scaling of Single-threaded Network Functions

Selective Symbolic Execution

Automated Verification of Network Function Binaries

Practical Verification of System-Software Components Written in Standard C