Search
Search Results
-
PROTON: PRObes for Termination Or Not (Competition Contribution)
PROTON is a tool to check whether a given C program has a non-terminating behaviour or not. It is built around the C Bounded Model Checker (CBMC)....
-
A verified low-level implementation and visualization of the adaptive exterior light and speed control system
In this article, we present an approach to the ABZ 2020 case study that differs from those usually presented at ABZ: Rather than using a...
-
An empirical assessment of machine learning approaches for triaging reports of static analysis tools
Despite their ability to detect critical bugs in software, static analysis tools’ high false positive rates are a key barrier to their adoption in...
-
Btor2-Cert: A Certifying Hardware-Verification Framework Using Software Analyzers
Formal verification is essential but challenging: Even the best verifiers may produce wrong verification verdicts. Certifying verifiers enhance the...
-
CoPTIC: Constraint Programming Translated Into C
Constraint programming systems allow a diverse range of problems to be modelled and solved. Most systems require the user to learn a new constraint...
-
Cutting the Cake into Crumbs: Verifying Envy-Free Cake-Cutting Protocols Using Bounded Integer Arithmetic
Fair division protocols specify how to split a continuous resource (conventionally represented by a cake) between multiple agents with different...
-
Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution)
Deagle is an SMT-based multi-threaded program verification tool. It is built on top of CBMC (front-end) and MiniSAT (back-end). The basic idea of...
-
HyperPUT: generating synthetic faulty programs to challenge bug-finding tools
As research in automatically detecting bugs grows and produces new techniques, having suitable collections of programs with known bugs becomes...
-
CBMC Path: A Symbolic Execution Retrofit of the C Bounded Model Checker
We gave CBMC the ability to explore and model check single program paths, as opposed to its default whole-program model-checking behaviour. This...
-
Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds
Software model checkers are able to exhaustively explore different bounded program executions arising from various sources of non-determinism. These...
-
Binary Level Concolic Execution on Windows with Rich Instrumentation Based Taint Analysis
Windows programs are widely used. The effective testing of Windows applications can prevent financial losses. Currently, there are only a few tools...
-
Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif
Verification of Programmable Logic Controller (PLC) programs requires reasoning about propositions qualified in terms of time. CERN’s PLCverif, an...
-
ESBMC v7.3: Model Checking C++ Programs Using Clang AST
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new Clang-based C++...
-
Ten Years of Industrial Experiments with Frama-C at Mitsubishi Electric R&D Centre Europe
Mitsubishi Electric R &D Centre Europe (MERCE), the advanced European research laboratory of Mitsubishi Electric group, has been carrying research...
-
Analysing Software
In Chaps. 3–5, we consider systems modelled at an abstract level in the form of one or more FSMs. However, if a model has been derived from an actual...
-
Automated SC-MCC test case generation using coverage-guided fuzzing
One of the main objectives of testing is to achieve adequate code coverage. Modern code coverage standards suggest MC/DC (Modified Condition/Decision...
-
VeriFuzz 1.4: Checking for (Non-)termination (Competition Contribution)
In VeriFuzz 1.4, we implemented two new techniques for checking Non-termination and Termination. VeriFuzz 1.4 won the Termination category of SV-COMP...
-
Towards Efficient Data-Flow Test Data Generation
Data-flow testing (DFT) aims to detect potential data interaction anomalies by focusing on the points at which variables receive values and the...
-
Quantifying Software Reliability via Model-Counting
Critical software should be verified. But how to handle the situation when a proof for the functional correctness could not be established? In this...
-
Verifying verified code
A recent case study from AWS by Chong et al. proposes an effective methodology for Bounded Model Checking in industry. In this paper, we report on a...
