ASE 2026 – Preliminary Table of Contents |
Contents -
Abstracts -
Authors
|
| FPSieve Conference Poster: Conference poster for the paper "FPSieve: LLM-Powered Cascade for Filtering False Positives in OS Migration Testing." |
unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.
| LiteScope — ASE 2026 Presentation Slides: Presentation slides for the ASE 2026 Industry Showcase talk on "LiteScope: Revealing the Security Paradox of Android Lite Apps in Resource-Constrained Ecosystems." | |
| LiteScope — One-Page Summary Slide: A single-slide summary of the talk, intended for display during the Industry Showcase session. |
| BanditFuzz Presentation Slide: This one-slide presentation summarizes the core architecture and key findings of BanditFuzz, a synergistic differential fuzzing framework for compilers. It visually outlines the four-stage pipeline—the Bandit Scheduler, CompileFix heuristic repair, ASTMutate deterministic expansion, and the enhanced differential ... |
proc time: 17.4