Publication

Software Verification by Combining Program Analyses of Adjustable Precision

Related publications (93)

Graph Chatbot

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.

Interoperation between Miniboxing and Other Generics Translations

Milos Stojanovic

Generics allow programmers to design algorithms and data structures that operate in the same way regardless of the data used by abstracting over data types. Generics are useful as they improve the programmer’s productivity by raising the level of abstracti ...

2015

Traversal Query Language For Scala.Meta

Eugene Burmako, Eric Beguet

With the rise of metaprogramming in Scala, manipulating ASTs has become a daily job. Yet the standard API provides only low-level mechanisms to transform or to collect information on those data structures. Moreover, those mechanisms often force the program ...

2015

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Simon Bliudze, Qiang Wang

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015

On Deductive Program Repair in Leon

Viktor Kuncak, Etienne Kneuss

We present an approach to program repair and its application to programs with recursive functions over unbounded data types. Our approach formulates program repair in the framework of deductive synthesis that uses existing program structure as a hint to gu ...

2015

Deductive Program Repair, Computer Aided Verification

Viktor Kuncak, Etienne Kneuss

2015

Symbolic Resource Bound Inference

Viktor Kuncak, Ravichandhran Kandhadai Madhavan

We present an approach for inferring symbolic resource bounds for purely functional programs consisting of recursive functions, algebraic data types and nonlinear arithmetic operations. In our approach, the developer specifies the desired shape of the boun ...

2014

Elephant Beer and Shinto Gates: Managing Similar Concepts in a Multilingual Database

Martin Benjamin

This paper addresses problems in equivalence among concepts, within and between languages. The Kamusi Project has begun building a massively multilingual dictionary that relates as many languages as possible for which data can be gathered. In the process, ...

2014

Mutable Checkpoint-Restart: Automating Live Update for Generic Server Programs

Calin Iorgulescu

The pressing demand to deploy software updates without stopping running programs has fostered much research on live update systems in the past decades. Prior solutions, however, either make strong assumptions on the nature of the update or require extensiv ...

ACM New York2014

Synthesis Modulo Recursive Functions

Viktor Kuncak, Etienne Kneuss, Ivan Kuraj, Philippe Paul Henri Suter

We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo recursive functions, a framework for deductive synthesis, and complete synt ...

2013

On Integrating Deductive Synthesis and Verification Systems

Viktor Kuncak, Etienne Kneuss, Ivan Kuraj, Philippe Paul Henri Suter

2013