Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning
Abstract elided by the publisher.
26,098 papers · page 448 of 1,305
Revisiting Enumerative Instantiation
Abstract elided by the publisher.
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…
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Abstract elided by the publisher.
Gradual Program Verification
Both static and dynamic program verification approaches have significant disadvantages when considered in isolation. Inspired by research on gradual typing, we propose gradual verification to seamlessly and flexibly combine static and dynamic verification. Drawing on general prin…
Automatic Verification of RMA Programs via Abstraction Extrapolation
Abstract elided by the publisher.
Scalable Approximation of Quantitative Information Flow in Programs
Abstract elided by the publisher.
Code Obfuscation Against Abstract Model Checking Attacks
Abstract elided by the publisher.
Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
Abstract elided by the publisher.
A Framework for Computer-Aided Design of Educational Domain Models
Abstract elided by the publisher.
Automatic Verification of Intermittent Systems
Abstract elided by the publisher.
On abstraction and compositionality for weak-memory linearisability
Abstract elided by the publisher.
From Shapes to Amortized Complexity
Abstract elided by the publisher.