APLAS 2024
18 papers
- A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution
- Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language
- Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories
- Effective Search Space Pruning for Testing Deep Neural Networks
- Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses
- Explaining Explanations in Probabilistic Logic Programming
- Extending the Quantitative Pattern-Matching Paradigm
- Generic Reasoning of the Locally Nameless Representation
- Hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions
- Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem
- Non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures
- OBRA: Oracle-Based, Relational, Algorithmic Type Verification
- On Computational Indistinguishability and Logical Relations
- Quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers
- Quantum Programming Without the Quantum Physics
- Random-Access Lists, from EE to FP
- Relative Completeness of Incorrectness Separation Logic
- Type-Based Verification of Connectivity Constraints in Lattice Surgery