Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
Abstract elided by the publisher.
642 papers · page 4 of 33
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.
Efficient Local Search for Nonlinear Real Arithmetic
Abstract elided by the publisher.
Model-Guided Synthesis for LTL over Finite Traces
Abstract elided by the publisher.
Distributing and Parallelizing Non-canonical Loops
Abstract elided by the publisher.
SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
Abstract elided by the publisher.
StaticPersist: Compiler Support for PMEM Programming
Abstract elided by the publisher.
Symbolic Abstract Heaps for Polymorphic Information-Flow Guard Inference
Abstract elided by the publisher.
Satisfiability Modulo Custom Theories in Z3
Abstract elided by the publisher.
Bayesian Parameter Estimation with Guarantees via Interval Analysis and Simulation
Abstract elided by the publisher.
A Pragmatic Approach to Stateful Partial Order Reduction
Abstract elided by the publisher.
A Generic Framework to Coarse-Grain Stochastic Reaction Networks by Abstract Interpretation
. In the last decades, logical or discrete models have emerged as a successful paradigm for capturing and predicting the behaviors of systems of molecular interactions. Intuitively, they consist in sampling the abundance of each kind of biochemical entity within finite sets of in…
Efficient Interprocedural Data-Flow Analysis Using Treedepth and Treewidth
Abstract elided by the publisher.
Maximal Robust Neural Network Specifications via Oracle-Guided Numerical Optimization
Abstract elided by the publisher.
Result Invalidation for Incremental Modular Analyses
Abstract elided by the publisher.