SPLASH 2022
2022-12-05..2022-12-10
Auckland, New Zealand
SPLASH ·
[SPLASH 2019 PLMW, SPLASH 2020, SPLASH 2020 REBASE, SPLASH 2022, SPLASH 2022 Doctoral Symposium]
| title | author | length |
|---|---|---|
| FIDDLR: streamlining reuse with concern-specific modelling languages | Maximilian Schiedermeier, Bettina Kemme, Jörg Kienzle | 29m |
FIDDLR presents a concrete framework that splits concern packaging into three clear tasks: implement the concern in GPML, define a concern-specific modelling… | ||
| Manipulating GUI Structures Declaratively | Knut Anders Stokke, Mikhail Barash, Jaakko Järvi | 28m |
A DSL called Warframe lets programmers declare incidental GUI structures as relations with test and establish methods and then auto-generates an API that… | ||
| Automatic Grammar Repair | Moeketsi Raselimo, Bernd Fischer | 59m |
Describes gfixr, a tool that automatically repairs context-free grammars by combining spectrum-based fault localization at individual rule positions with small… | ||
| A Counterexample-Guided Debugger for Non-Recursive Datalog | Van-Dang Tran, Hiroyuki Kato, Zhenjiang Hu | 24m |
Prototype debugs non-recursive Datalog by (1) a property language for pre/postconditions, (2) a counterexample generator that encodes rule evaluation… | ||
| A New Refinement Type System for Automated nu-HFLZ Validity Checkin | Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada | 25m |
A refinement type system targets validity checking for a fragment of vHFLZ (no least fixpoints) and produces template-based constraints that are solved to… | ||
| P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine | Andrea Rosà, Walter Binder | 27m |
P3 is a profiler suite for the JVM that actually instruments bytecode (using diesel bytecode instrumentation) and records concrete counts of threads, tasks… | ||
| Termination Analysis for the pi-Calculus by Reduction to Sequential Program Termination | Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada | 23m |
Proposes an automated reduction that translates pi-calculus processes into sequential C programs so termination of the C program implies termination of the… | ||
| Abstract Neural Networks | Matthew Sotoudeh, Aditya V. Thakur | 31m |
The paper introduces Abstract Neural Networks that soundly overapproximate a DNN while using far fewer nodes by replacing weight matrices with elements of an… | ||
| Reduced Products of Abstract Domains for Fairness Certification of Neural Networks | Denis Mazzucato, Caterina Urban | 28m |
Libra is an open‑source static analyzer that certifies dependency fairness for ReLU feedforward classifiers by combining a cheap forward pre‑analysis over… | ||
| Static analysis of ReLU neural networks with tropical polyhedra | Eric Goubault, Sebastien Palumby, Sylvie Putot, Louis Rustenholz, Sriram Sankaranarayanan | 28m |
Claims a concrete static-analysis method that uses tropical polyhedra to abstract ReLU feedforward nets, representing ReLU layers exactly and approximating… | ||
| Compositional Verification of Smart Contracts Through Communication Abstraction | Scott Wesley, Jorge A. Navas, Valentin Wüstholz, Maria Christakis, Arie Gurfinkel, Richard Trefler | 29m |
Claims that local bundles reduce contracts with 2^160 addresses to a sequential C model with a handful of representative users computed via static analysis… | ||
| Interprocedural Shape Analysis Using Separation Logic-Based Transformer Summaries | H. Illous, M. Lemerre, X. Rival | 31m |
Proposes using connectors from separation logic to encode abstract transformation relations as procedure summaries, then composes them top-down to avoid… | ||
| Composing and decomposing op-based CRDTs with semidirect products | Matthew Weidner, Heather Miller, Christopher S. Meiklejohn | 29m |
Presents a concrete construction that composes two op-based CRDTs into one using an explicit semidirect product action that transforms noncommuting ops (proofs… | ||
| Improving Thread-Modular Abstract Interpretation | Michael Schwarz, Simmo Saan, Helmut Seidl, Kalmer Apinis, Julian Erhard, Vesal Vojdani | 30m |
Presents a thread‑modular framework that formalizes analyses as side-effecting constraint systems with a new local trace semantics, proves soundness of… | ||
| Static Analysis of Endian Portability by Abstract Interpretation | David Delmas, Abdelraouf Ouadjaout, Antoine Miné | 35m |
A static analyzer infers whether two C variants produce identical outputs across little- and big-endian platforms by building a B-cell memory abstraction plus… | ||
| Certifying the Synthesis of Heap-Manipulating Programs | Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, Ilya Sergey | 29m |
Method translates SuSLik synthesis traces into machine-checkable Coq proofs and produces three certifiers for HTT, Iris and VST, evaluated on 15 benchmarks… | ||
| Kindly Bent to Free Us | Gabriel Radanne, Hannes Saffrich, Peter Thiemann | 30m |
Affe is an ML extension that enforces single-use and drop-able resources by inferring linear and affine kinds and lexical regions and solving constrained-kind… | ||
| Stable relations and abstract interpretation of higher-order programs | Benoît Montagu, Thomas P. Jensen | 31m |
Defines a denotational semantics where terms are stable relations (binary relations between substitutions and values) and proves it sound and complete against… | ||
| Label dependent lambda calculus and gradual typing | Weili Fu, Fabian Krause, Peter Thiemann | 29m |
Defines a minimalist label-dependent lambda calculus with first-class labels, Pi/Sigma/singleton types and subtyping, then gives a gradual extension with a… | ||
| Modular Specification and Verification of Closures in Rust | Fabian Wolff, Aurel Bílý, Christoph Matheja, Alexander J. Summers, Peter Müller | 20m |
Presents a concrete method to specify and verify Rust closures by encoding higher‑order concerns into a first-order encoding that SMT solvers (via Viper and… | ||
| Revisiting Iso-Recursive Subtyping | Yaoda Zhou, Jinxu Zhao, Bruno C. d. S. Oliveira | 24m |
Presents a new declarative finite unfolding specification that says two mu-types are subtypes iff all same-depth finite unfoldings are subtypes, proves the… | ||
| Symbolic value-flow static analysis:deep,precise,complete modeling of Ethereum smartcontracts | Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, Ilias Tsatiris | 33m |
A static analysis combines concrete values and symbolic expressions into a symvalic analysis that runs as a Datalog fixpoint while calling a theorem prover… | ||
| A Case Study in Language-Based Security: Building an I/O Library for Wyvern | Jennifer A. Fish, Darya Melicher, Jonathan Aldrich | 30m |
Builds a small standard I/O library for Wyvern that combines object capabilities, an effect system, and language extensions to reduce misuse. Demonstrates… | ||
| How (Not) To Write Java Pointer Analyses After 2020 | Manas Thakur | 29m |
This research exposes concrete pitfalls and fixes for Java pointer analyses: handling 14 language cases (nulls, exceptions, hidden this, returns, globals)… | ||
| Putting the Semantics into Semantic Versioning | Patrick Lam, Jens Dietrich, David J. Pearce | 30m |
Argues that three-number semantic versioning is unreliable and proposes semantic version calculators that combine scalable static analysis, fuzzing… | ||
| PMEvo:portable inference of port mappings for out-of-order processors by evolutionary optimiz | Fabian Ritter, Sebastian Hack | 27m |
PMEvo infers processor port mappings from timed short microbenchmarks rather than platform-specific performance counters, using an evolutionary algorithm that… | ||
| Software Model-Checking as Cyclic-Proof Search | Takeshi Tsukada, Hiroshi Unno | 31m |
Claims that many software model-checking procedures are just proof-search strategies for a cyclic proof system and gives a worked mapping: symbolic execution… | ||
| SolType: Refinement Types for Arithmetic Overflow in Solidity | Bryan Tan, Benjamin Mariano, Shuvendu K. Lahiri, Isil Dillig, Yu Feng | 21m |
SolType adds refinement types to Solidity and Solid implements it, inferring contract invariants to prove arithmetic overflow absence rather than paying… | ||
| Behavioral simulation for smart contracts | Sidi Mohamed Beillahi, Gabriela Ciocarlie, Michael Emmi, Constantin Enea | 25m |
Automated method claims to verify unannotated smart contracts by synthesizing behavioral refinement as simulation relations between a few manually annotated… | ||
| Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities | Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, Yannis Smaragdakis | 31m |
Ethainter implements Datalog taint analysis and models cross-transaction taint with sanitizers, not just single-call bugs, and runs on bytecode at blockchain… | ||
| Practical Smart Contract Sharding with Ownership and Commutativity Analysis | George Pîrlea, Amrit Kumar, Ilya Sergey | 31m |
Static analysis tool CoSplit infers per-transition ownership and commutativity summaries for Cilla smart contracts and compiles them into sharding signatures… | ||
| nothing matches | ||