Scaling Language Features for Program Verification
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.
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 ...
We present a verification procedure for pure higher-order functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counter-examples. The procedure reduces the analysis of higher-orde ...
High-level languages allow programmers to express data structures and algorithms that abstract over the type of data they handle. This improves code reuse and makes it possible to develop general-purpose libraries. Yet, data abstractions slow down program ...
The Semantic Web brings a powerful set of concepts, standards and ideas that are already changing the shape of the Web. However, in order to put these notions into practice we need to translate them into code. That is why the broad notion of programming th ...
Programming systems incorporating aspects of functional programming, e.g., higher-order func- tions, are becoming increasingly popular for large-scale distributed programming. New frameworks such as Apache Spark leverage functional techniques to provide hi ...
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 ...
One of the main challenges in software verification is efficient and precise analysis of programs with procedures and loops. Interpolation methods remain among the most promising techniques for such verification. To accommodate the demands of various progr ...
Hundreds of programming languages compile to JavaScript. Yet, most of them fail, at one level or another, to provide satisfactory interoperability with JavaScript APIs. This is limiting, as interoperability is at least required to manipulate web pages thro ...
We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy eval- uation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. ...
This dissertation explores techniques that synthesize and generate program fragments and test inputs. The main goal of these techniques is to improve and support automation in program synthesis and test input generation. This is important because performin ...
