9 citations · 13 across the 7 of their papers we have counts for
9 papers
ForTress: Bringing Assurance and Determinism for LLM-Driven Fortran-to-Python Translation
Qinrun Dai, Ruitong Liu, Chien-Wei Huang +3
Modernizing mature scientific software from Fortran to Python can improve accessibility and integration with modern computing tools, but manual rewriting is expensive. Large langua…
Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots (Extended Version)
Dinghong Zhong, Alexander Bai, Mikail Khan +1
Concolic execution is a variant of symbolic execution that runs a program simultaneously with concrete and symbolic inputs. It records the symbolic constraints encountered along a…
When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-stage Programming with Let-Insertion (Extended Version)
Jun Tan, Guannan Wei
Multi-stage programming with quotations has long provided a powerful way to generate and manipulate code. By treating code as data, programmers can write multi-stage programs in wh…
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He +2
Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its "…
Graph IRs for Impure Higher-Order Languages (Technical Report)
Oliver Bračevac, Guannan Wei, Songlin Jia +4
This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the graph IR, at a level of detail beyond a r…
Modeling Reachability Types with Logical Relations
Yuyan Bao, Songlin Jia, Guannan Wei +2
Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages, with a focus on higher-order functions, parametric types,…
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Guannan Wei, Oliver Bračevac, Songlin Jia +2
Reachability types are a recent proposal that has shown promise in scaling to higher-order but monomorphic settings, tracking aliasing and separation on top of a substrate inspired…
Application-Level Validation of Accelerator Designs Using a Formal Software/Hardware Interface
Bo-Yuan Huang, Steven Lyubomirsky, Yi Li +10
Ideally, accelerator development should be as easy as software development. Several recent design languages/tools are working toward this goal, but actually testing early designs o…
Graph Neural Reasoning for 2-Quantified Boolean Formula Solvers
Zhanfu Yang, Fei Wang, Ziliang Chen +2
In this paper, we investigate the feasibility of learning GNN (Graph Neural Network) based solvers and GNN-based heuristics for specified QBF (Quantified Boolean Formula) problems.…