SAS 2023
| title | author | length |
|---|---|---|
| Opening | Manuel Hermenegildo, José Morales | 04m |
Conference opens with a program of 20 papers and four invited talks plus a PC report and a radus session Monday afternoon. Sponsors listed are Google the ens… | ||
| Goal-Directed Abstract Interpretation and Event-Driven Frameworks | Bor-Yuh Evan Chang | 56m |
Argues for goal-directed backward analysis that models only callbacks relevant to a single error, implements abstract message histories to represent realizable… | ||
| A Product of Shape and Sequence Abstractions (Young Researcher Best... | Radhia Cousot | 26m |
Introduces a novel sequence domain that tracks length, extremal values and multiset content, and forms a reduced product with a separation-logic shape analysis… | ||
| How fitting is your abstract domain? | Roberto Giacobazzi, Isabella Mastroeni, Elia Perantoni | 25m |
Presents a sound, language- and domain-agnostic proof system that decides whether an abstract domain can produce answers strictly better than a chosen… | ||
| Domain Precision in Galois Connection-less Abstract Interpretation | Isabella Mastroeni, Michele Pasqua | 33m |
Shows that completeness of an abstract interpretation is equivalent to abstract non‑interference, letting completeness be checked as a hyperproperty of the… | ||
| A Formal Framework to Measure the Incompleteness of Abstract Interpretations | Marco Campion, Caterina Urban, Mila Dalla Preda, Roberto Giacobazzi | 22m |
Defines a weaker distance notion called pre-metric that relaxes quasi-metric axioms so distances work on pre-ordered abstract and concrete domains, shows how… | ||
| Generalized Program Sketching by Abstract Interpretation and Logical Abduction | Aleksandar S. Dimovski | 22m |
Defines a generalized sketching problem and implements a working prototype synthesizer for C that fills holes with arbitrary arithmetic or boolean expressions… | ||
| Reverse Template Processing using Abstract Interpretation | Matthieu Lemerre | 26m |
A reverse-template engine converts templates into an ambiguous parser and an abstract semantics that returns all input databases that can produce a given… | ||
| BREWasm: A General Static Binary Rewriting Framework for WebAssembly | Shangtong Cao, Ningyu He, Yao Guo, Haoyu Wang | 27m |
[SAS23] BREWasm: A General Static Binary Rewriting Framework for WebAssembly
Shangtong Cao, Ningyu He, Yao Guo, Haoyu Wang
Binary rewriting is a widely… | ||
| Quantum Constant Propagation | Yanbin Chen, Yannick Stade | 30m |
Implements quantum constant propagation (QCP) to symbolically simulate entanglement groups up to a complexity bound and remove redundant controls and gates… | ||
| Boosting Multi-Neuron Convex Relaxation for Neural Network Verification | Xuezhou Tang, Ye Zheng, Jiaxiang Liu | 30m |
A volume-approximation pipeline selects which neuron groups get true convex-hull relaxation instead of computing all 2K-dimensional hulls: FaGMR computes… | ||
| Abstract Interpretation in Industry - Experience and Lessons Learned | Daniel Kaestner | 01h 08m |
Commercialized two abstract-interpretation analyzers: aiT WCET Analyzer for worst-case execution time and Astrée for absence of runtime errors, built at absin… | ||
| Lifting On-Demand Analysis to Higher-Order Languages | Daniel Schoepe, David Seekatz, Ilina Stoilkovska, Sandro Stucki, Daniel Tattersall, Pauline Bolignano, Franco Raimondi, Bor-Yuh Evan Chang | 23m |
Claims an on-demand algorithm that bootstraps call graph construction by interleaving two on-demand data‑flow queries, formalizes the method as an… | ||
| Symbolic transformation of expressions in modular arithmetic | Jérôme Boillot, Jerome Feret | 24m |
Formal rewriting rules convert modular integer expressions into sums products or quotients of linear forms with integer coefficients and prove soundness and… | ||
| Polynomial Analysis of Modular Arithmetic | Thomas Seed, Andy King, Neil Evans, Chris Coppins | 38m |
Proposes the modular polynomial abstract domain (MPAD) whose invariants are polynomial equations modulo 2^k, implements closure via coverings, Groebner bases… | ||
| Octagons Revisited - Elegant Proofs and Simplified Algorithms | Michael Schwarz, Helmut Seidl | 27m |
Provides simplified cubic time closure algorithms for Octagon abstract relations over rationals and integers that avoid introducing auxiliary negation… | ||
| Error Invariants for Fault Localization via Abstract Interpretation | Aleksandar S. Dimovski | 27m |
Presents a concrete technique that computes error invariants by iterating backward and forward abstract-interpretation analyses to shrink an error slice and… | ||
| Error Localization for Sequential Effect Systems | Colin Gordon, Chaewon Yun | 27m |
Proposes a concrete algebraic trick that gives precise error sites for sequential (flow‑sensitive) effect systems by using a residual operator from residuated… | ||
| Scaling up Roundoff Analysis of Functional Data Structure Programs | Anastasia Isychev, Eva Darulova | 32m |
Claims a method that analyzes floating-point roundoff for loops over vectors and matrices by grouping elements by value ranges and analyzing each group once… | ||
| Building Trust and Safety in Artificial Intelligence with Abstract Interpretation | Gagandeep Singh | 58m |
Abstract interpretation is used to certify and train DNNs so they generalize to infinite unseen inputs, with specific domains like DeepPoly and zonotopes and a… | ||
| Radhia Cousot Award and PC report | Manuel Hermenegildo, José Morales | 10m |
Program committee forms in late March with roughly half returning members, 4 women and 21 men, and geographic balance across US, China, Europe and Asia. Paper… | ||
| ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses | Florian Frohn, Jürgen Giesl | 29m |
ADCL presents a calculus that learns n-parameterized accelerated clauses (transitive closures of recursive CHCs) and implements it in the tool LoAT, using four… | ||
| Unconstrained Variable Oracles for Faster Static Analyses | Vincenzo Arceri, Greta Dolcetti, Enea Zaffanella | 30m |
Proposes a lightweight pre-analysis that marks variables likely to be unconstrained and rewrites their assignments to nondeterministic havoc in the Crab IR… | ||
| Modular Optimization-Based Roundoff Error Analysis of Floating-Point Programs | Rosa Abbasi Boroujeni, Eva Darulova | 22m |
An optimization-based static analysis extends FB Taylor to handle non-recursive procedural floating-point code by computing procedure summaries as functions of… | ||
| Verifying Infinitely Many Programs at Once | Loris D'Antoni | 01h 05m |
Proposes proving unrealizability for entire program search spaces by reducing synthesis-to-verification and by designing a Hoare-like logic that reasons about… | ||
| Mutual Refinements of Context-Free Language Reachability | Shuo Ding, Qirun Zhang | 21m |
Proposes a modified CFL-reachability algorithm that traces contributing edges per grammar and iteratively removes noncontributing edges across multiple CFL… | ||
| nothing matches | ||