On Multi-language Abstraction - Towards a Static Analysis of Multi-language Programs
Abstract elided by the publisher.
783 papers · page 6 of 40
Static Resource Analysis at Scale (Extended Abstract)
Abstract elided by the publisher.
Exact and Linear-Time Gas-Cost Analysis
Abstract elided by the publisher.
Termination of Polynomial Loops
Abstract elided by the publisher.
Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries
Abstract elided by the publisher.
Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking
Abstract elided by the publisher.
Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis
Abstract We present an automated procedure for synthesizing sound inductive invariants for floating-point numerical loops. Our procedure generates invariants of the form of a convex polynomial inequality that tightly bounds the values of loop variables. Such invariants are a prer…
Memory-Efficient Fixpoint Computation
Abstract elided by the publisher.
Probabilistic Lipschitz Analysis of Neural Networks
Abstract elided by the publisher.
Simple and Efficient Computation of Minimal Weak Control Closure
Abstract elided by the publisher.
Stratified Guarded First-Order Transition Systems
Abstract First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transi…
A Library Modeling Language for the Static Analysis of C Programs
Abstract elided by the publisher.
Cost Analysis of Smart Contracts Via Parametric Resource Analysis
. The very nature of smart contracts and blockchain platforms, where program execution and storage are replicated across a large number of nodes, makes resource consumption analysis highly relevant. This has led to the development of analyzers for specific platforms and languages.…
Formal Framework for Reasoning About the Precision of Dynamic Analysis
Abstract elided by the publisher.
Abstract Neural Networks
Deep Neural Networks (DNNs) are rapidly being applied to safety-critical domains such as drone and airplane control, motivating techniques for verifying the safety of their behavior. Unfortunately, DNN verification is NP-hard, with current algorithms slowing exponentially with th…
Temporal Verification of Programs via First-Order Fixpoint Logic
Abstract elided by the publisher.
Revisiting Polyhedral Analysis for Hybrid Systems
Abstract elided by the publisher.
Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets
Multiphase ranking functions (M$\Phi$RFs) are tuples $\langle f_1,\ldots,f_d \rangle$ of linear functions that are often used to prove termination of loops in which the computation progresses through a number of "phases". Our work provides new insights regarding such functions fo…
Abstract Interpretation of Indexed Grammars
Abstract elided by the publisher.
Syntactic and Semantic Soundness of Structural Dataflow Analysis
Abstract elided by the publisher.