Local Reasoning About Probabilistic Behaviour for Classical-Quantum Programs
Abstract elided by the publisher.
26,098 papers · page 145 of 1,305
AGNES: Abstraction-Guided Framework for Deep Neural Networks Security
Deep Neural Networks (DNNs) are becoming widespread, particularly in safety-critical areas. One prominent application is image recognition in autonomous driving, where the correct classification of objects, such as traffic signs, is essential for safe driving. Unfortunately, DNNs…
Resilience and Home-Space for WSTS
Abstract elided by the publisher.
Interpolation and Quantifiers in Ortholattices
We study quantifiers and interpolation properties in \emph{orthologic}, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based proof system for qua…
Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Abstract elided by the publisher.
TP-DejaVu: Combining Operational and Declarative Runtime Verification
Abstract elided by the publisher.
Formal Runtime Error Detection During Development in the Automotive Industry
Abstract elided by the publisher.
Petrification: Software Model Checking for Programs with Dynamic Thread Management
Abstract elided by the publisher.
A Navigation Logic for Recursive Programs with Dynamic Thread Creation
Abstract elided by the publisher.
Generation of Violation Witnesses by Under-Approximating Abstract Interpretation
Abstract elided by the publisher.
Borrowable Fractional Ownership Types for Verification
Abstract elided by the publisher.
Abstract Interpretation-Based Feature Importance for Support Vector Machines
,
Sound Abstract Nonexploitability Analysis
Abstract elided by the publisher.
Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
Abstract elided by the publisher.
Verification of Neural Networks' Local Differential Classification Privacy
Abstract elided by the publisher.
Correctness Witness Validation by Abstract Interpretation
Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Give…
Solving Two-Player Games Under Progress Assumptions
This paper considers the problem of solving infinite two-player games over finite graphs under various classes of progress assumptions motivated by applications in cyber-physical system (CPS) design. Formally, we consider a game graph G, a temporal specification $\Phi$ and a temp…
Deductive Verification of Parameterized Embedded Systems Modeled in SystemC
Abstract elided by the publisher.
Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
The intrinsic complexity of deep neural networks (DNNs) makes it challenging to verify not only the networks themselves but also the hosting DNN-controlled systems. Reachability analysis of these systems faces the same challenge. Existing approaches rely on over-approximating DNN…
Function Synthesis for Maximizing Model Counting
Abstract elided by the publisher.