Concept

Runtime verification

Related publications (87)

-Overify: Optimizing Programs for Fast Verification

George Candea, Volodymyr Kuznetsov, Jonas Benedict Wagner

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

2013

An Embedded Query Language in Scala

Amir Shaikhha

In this thesis we address the problem of integrating general purpose programming languages with relational databases. An approach to solving this problem is using raw strings to represent SQL statements. This approach leads to runtime errors and security v ...

2013

Secure & Lightweight Distance-Bounding

Serge Vaudenay, Aikaterini Mitrokotsa

Distance-bounding is a practical solution to be used in security-sensitive contexts, mainly to prevent relay attacks. The main challenge when designing such protocols is maintaining their inexpensive cryptographic nature, whilst being able to protect again ...

2013

On Integrating Deductive Synthesis and Verification Systems

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

Synthesis Modulo Recursive Functions

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

2013

Termination Analysis in a Higher-Order Functional Context

Nicolas Charles Yves Voirol

We start by describing how higher-order function support can be added to a (first order) functional verification framework. We cover both the higher-order construct management and framework extensions necessary for constraint specification. Next, we outlin ...

2013

Medical Guidelines Reconciling Medical Software and Electronic Devices: Imatinib Case-study

Giovanni De Micheli, Alena Simalatsar

Nowadays medical software is tightly coupled with medical devices that perform patient state monitoring and lately even some basic treatment procedures. Medical guidelines (GLs) can be seen as specification of a medical system that includes both software a ...

Ieee2012

Alternating Control Flow Reconstruction

Johannes Kinder

Unresolved indirect branch instructions are a major obstacle for statically reconstructing a control flow graph (CFG) from machine code. If static analysis cannot compute a precise set of possible targets for a branch, the necessary conservative over-appro ...

Springer2012

Certifying Solutions for Numerical Constraints

Viktor Kuncak, Eva Darulova

A large portion of software is used for numerical computation in mathematics, physics and engineering. Among the aspects that make verification in this domain difficult is the need to quantify numerical errors, such as roundoff errors and errors due to the ...

2012

On the Automatic Computation of Error Bounds for Solutions of Nonlinear Equations

Viktor Kuncak, Eva Darulova

A large portion of software is used for numerical calculations in mathematics, physics and engineering applications. Among the things that make verification in this domain difficult is the quantification of numerical errors, such as roundoff errors and err ...

2012

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.