Publication

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

Related publications (23)

DatAFLow: Toward a Data-flow-guided Fuzzer

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

2023

Automated Verification of Network Function Binaries

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki

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

USENIX Association2022

Synthetic Disinformation Attacks on Automated Fact Verification Systems

Antoine Bosselut

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

ASSOC ADVANCEMENT ARTIFICIAL INTELLIGENCE2022

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

Eugen Brühwiler, Dragan Damjanovic

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

CRC PRESS-TAYLOR & FRANCIS GROUP2019

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

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

EPFL2019

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

George Candea, Vitaly Chipounov, Bin Zhang, Chao Feng

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

INST ENGINEERING TECHNOLOGY-IET2018

Solving quantified linear arithmetic by counterexample-guided instantiation

Viktor Kuncak, Andrew Joseph Reynolds

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

2017

Decrypting Local Type Inference

Hubert Plociniczak

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

EPFL2016

PBCOV: a property-based coverage criterion

Hamza Harkous, Kassem Fawaz

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

Springer2015

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