Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

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.

This Replicating Computational Report (RCR) describes (a) our datAFLow fuzzer and (b) how to replicate the results in "datAFLow: Toward a Data-Flow-Guided Fuzzer." Our primary artifact is the datAFLow fuzzer. Unlike traditional coverage-guided greybox fuzz ...

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

Automated fact-checking is a needed technology to curtail the spread of online misinformation. One current framework for such solutions proposes to verify claims by retrieving supporting or refuting evidence from related textual sources. However, the reali ...

In the last decade, Ultra High Performance Fibre Reinforced cement-based Composites (UHPFRC) have been increasingly implemented for rehabilitation and strengthening purposes, rendering outstanding results. The ease of application, along with their superior ...

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

Coverage-based fuzz testing and dynamic symbolic execution are both popular program testing techniques. However, on their own, both techniques suffer from scalability problems when considering the complexity of modern software. Hybrid testing methods attem ...

This paper presents a framework to derive instantiation-based decision procedures for satisfiability of quantified formulas in first-order theories, including its correctness, implementation, and evaluation. Using this framework we derive decision procedur ...

Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages ...

Coverage criteria aim at satisfying test requirements and compute metrics values that quantify the adequacy of test suites at revealing defects in programs. Typically, a test requirement is a structural program element, and the coverage metric value repres ...

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

Manual software testing is laborious and prone to human error. Yet, among practitioners, it is the most popular method for quality assurance. Automating the test case generation promises better effectiveness, especially for exposing corner-case bugs. Symbo ...

Concurrency bugs are at the heart of some of the worst bugs that plague software. Concurrency bugs slow down software development because it can take weeks or even months before developers can identify and fix them. In-production detection, root cause ...

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 which requires their computer ...

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

Reo is a coordination language that can be used to model different systems. We propose a technique for symbolic execution of Reo circuits using the symbolic representation of data constraints in Constraint Automata. This technique enables us to obtain the ...

This paper presents a publicly available toolkit and a benchmark suite for rigorous verification of Integer Numerical Transition Systems (INTS), which can be viewed as control-flow graphs whose edges are annotated by Presburger arithmetic formulas. We pres ...

This thesis explores the use of specifications for the construction of correct programs. We go beyond their standard use as run-time assertions, and present algorithms, techniques and implementations for the tasks of 1) program verification, 2) declarative ...

We present Counterexample-Guided Accelerated Abstraction Refinement (CEGAAR), a new algorithm for verifying infinite-state transition systems. CEGAAR combines interpolation-based predicate discovery in counterexample guided predicate abstraction with accel ...

Although they are helpful in many cases, state-of-the-art bug reporting systems may impose excessive overhead on users, leak private information, or provide little help to the developer in locating the problem. In this paper, we explore a new approach to b ...

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the ...

Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

Chat with Graph Search

DatAFLow: Toward a Data-flow-guided Fuzzer

Automated Verification of Network Function Binaries

Synthetic Disinformation Attacks on Automated Fact Verification Systems

Towards the use of UHPFRC in railway bridges: the rehabilitation of Buna Bridge

Scaling Functional Synthesis and Repair

Discover deeper bugs with dynamic symbolic execution and coverage-based fuzz testing

Solving quantified linear arithmetic by counterexample-guided instantiation

Decrypting Local Type Inference

PBCOV: a property-based coverage criterion

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

Improving Scalability of Symbolic Execution for Software with Complex Environment Interfaces

Techniques for Detection, Root Cause Diagnosis, and Classification of In-Production Concurrency Bugs

Representation of Medical Guidelines with a Computer Interpretable Model

Alternating Control Flow Reconstruction

Symbolic execution of Reo circuits using constraint automata

A Verification Toolkit for Numerical Transition Systems

Programming with Specifications

Accelerating Interpolants

Striking a New Balance Between Program Instrumentation and Debugging Time

Decision Procedures for Program Synthesis and Verification