Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics
Abstract elided by the publisher.
Related papers
- Automatic Generation of Warp-Level Primitives and Atomic Instructions for Fast and Portable Parallel Reduction on GPUs CGO 2019
- AnICA: analyzing inconsistencies in microarchitectural code analyzers OOPSLA 2022
- Inductive Predicate Synthesis Modulo Programs ECOOP 2024
- Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants TACAS 2023
- Optimizing remote accesses for offloaded kernels: application to high-level synthesis for FPGA PPoPP 2012
- Formalizing Linear Motion G-Code for Invariant Checking and Differential Testing of Fabrication Tools OOPSLA 2025
- TRANSIT: specifying protocols with concolic snippets PLDI 2013
- Latticed k-Induction with an Application to Probabilistic Programs CAV 2021