Revisiting Enumerative Instantiation
Abstract elided by the publisher.
1,553 papers · page 30 of 78
A Non-linear Arithmetic Procedure for Control-Command Software Verification
Abstract elided by the publisher.
Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis
To decide whether a set of states is reachable in a hybrid system, over-approximative symbolic successor computations can be used, where the symbolic representation of state sets as well as the successor computations have several parameters which determine the efficiency and the …
Structurally Defined Conditional Data-Flow Static Analysis
Data flow analysis (DFA) is an important verification technique that computes the effect of data values propagating over program paths. While more precise than flow-insensitive analyses, such an analysis is time-consuming.
Automating Deductive Verification for Weak-Memory Programs
Abstract elided by the publisher.
Feature-Guided Black-Box Safety Testing of Deep Neural Networks
Despite the improved accuracy of deep neural networks, the discovery of adversarial examples has raised serious safety concerns. Most existing approaches for crafting adversarial examples necessitate some knowledge (architecture, parameters, etc.) of the network at hand. In this …
Verified Model Checking of Timed Automata
We have constructed a mechanically verified prototype implementation of a model checker for timed automata, a popular formalism for modeling real-time systems. Our goal is two-fold: first, we want to provide a reference implementation that is fast enough to check other model chec…
YOGAR-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement - (Competition Contribution)
This paper presents the Y ogar - CBMC tool for verification of multi-threaded C programs. It employs a scheduling constraint based abstraction refinement method for bounded model checking of concurrent programs. To obtain effective refinement constraints, we have proposed the not…
Efficient Verification of Imperative Programs Using Auto2
Auto2 is a recently introduced prover for the proof assistant Isabelle. It is designed to be both highly customizable from within Isabelle, and also have a powerful proof search mechanism. In this paper, we apply auto2 to the verification of imperative programs. We describe the s…
Context-Bounded Analysis for POWER
We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis intitiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs supposed to be running under the …
Towards Parallel Boolean Functional Synthesis
Given a relational specification \(\varphi (X, Y)\), where X and Y are sequences of input and output variables, we wish to synthesize each output as a function of the inputs such that the specification holds. This is called the Boolean functional synthesis problem and has applica…
HiFrog: SMT-based Function Summarization for Software Verification
Abstract elided by the publisher.
Scaling Enumerative Program Synthesis via Divide and Conquer
Abstract elided by the publisher.
Combining String Abstract Domains for JavaScript Analysis: An Evaluation
Abstract elided by the publisher.
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions - (Competition Contribution)
Abstract elided by the publisher.
The Automatic Detection of Token Structures and Invariants Using SAT Checking
Abstract elided by the publisher.
Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults
Time-triggered switched networks are a deterministic communication infrastructure used by real-time distributed embedded systems. Due to the criticality of the applications running over them, developers need to ensure that end-to-end communication is dependable and predictable. T…
Maximizing the Conditional Expected Reward for Reaching the Goal
The paper addresses the problem of computing maximal conditional expected accumulated rewards until reaching a target state briefly called maximal conditional expectations in finite-state Markov decision processes where the condition is given as a reachability constraint. Conditi…
Rigorous Simulation-Based Analysis of Linear Hybrid Systems
Abstract elided by the publisher.
Congruence Closure with Free Variables
Abstract elided by the publisher.