LOPSTR 2023
who it's for
programming language researchers, language designers, static analysis engineers, verification engineers, compiler engineers, tool developers, formal methods engineers
topics
nominal unification with binders; verified deep neural network proof checker; machine-level amortized resource analysis; asynchronous multiparty compatibility; Java generics relational solver; rule-based abstract domain composition; Datalog templates for bidirectional synthesis; incremental interactive abstract interpretation; one-pass term matching algorithm; predicate-level anti-unification; propositional-formula simplification framework; category-based access control mining
| title | author | length |
|---|---|---|
| Unification Modulo Equational Theories in Languages with Binding Operators | Maribel Fernandez | 59m |
Presents concrete algorithms and implementations for solving equations where terms have binders plus equational axioms: uses nominal logic with permutations to… | ||
| Towards a Certified Proof Checker for Deep Neural Network Verification | Remi Desmartin, Omri Isac, Grant Passmore, Kathrin Stark, Guy Katz, Ekaterina Komandantskaya | 26m |
A formally verified proof checker for deep neural network verification is implemented in Imandra and extracts to native OCaml, using Simplex proof certificates… | ||
| A Reusable Machine-Calculus for Automated Resource Analyses | Hector Suzanne, Emmanuel Chailloux | 39m |
Claims a reusable, machine-level intermediate representation that encodes evaluation contexts as data and yields automated amortized resource bounds by… | ||
| A Logical Interpretation of Asynchronous Multiparty Compatibility | Marco Carbone, Sonia Marin, Carsten Schürmann | 25m |
Claims a syntactic, logical criterion that exactly captures asynchronous multiparty compatibility by encoding session types as linear propositions, using… | ||
| Relational Solver for Java Generics Type System | Petr Lozov, Dmitry Kosarev, Dmitry Ivanov, Dmitri Boulytchev | 22m |
Relational conversion of a Java subtyping verifier into a solver produces a tool that enumerates all substitutions for free type variables by combining a… | ||
| A Rule-Based Approach for Designing and Composing Abstract Domains | Daniel Jurjo Rivas, José Morales, Pedro López-García, Manuel Hermenegildo | 26m |
A rule-based language lets users specify how lattice elements from multiple abstract domains rewrite and combine, so the system generates projection, extent… | ||
| Design Datalog Templates for Synthesizing Bidirectional Programs from Tabular E... | Bach Nguyen Trong, Kanae Tsushima, Zhenjiang Hu | 31m |
Designs Datalog templates that let ProIn plus Z3 synthesize paired get/put programs from one tabular example and a supplied schema with functional… | ||
| On-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi... | Manuel Hermenegildo | 01h 06m |
An analyzer implementation (CiaoPP) performs top‑down, context‑ and path‑sensitive abstract interpretation with incremental, modular fixpoint reuse via… | ||
| A Term Matching Algorithm and Substitution Generality | Marija Kulaš | 29m |
Presents a decision procedure that reduces substitution-generality to term matching and implements a deterministic, one-pass matcher adapted from a textbook… | ||
| Predicate Anti-unification in (Constraint) Logic Programming | Gonzague Yernaux, Wim Vanhoof | 37m |
Defines predicate-level most-specific generalization (MSG) for logic programs, formalizes argument/ clause mapping and a τ quality function (term-size norm) to… | ||
| A Novel EGs-Based Framework for Systematic Propositional-Formula Simplification | Jordina Francès de Mas, Juliana Bowles | 30m |
A framework implements existential graphs plus binary implication graph analysis as a directed cyclic hypergraph to simplify arbitrary propositional formulas… | ||
| From Static to Dynamic Access Control Policies via Attribute-Based Category Min... | Anna Bamberger, Maribel Fernandez | 19m |
A miner synthesizes category-based access-control policies from logs and matrices, producing logical category formulas, allowed actions and a proof of… | ||
| Constrained Horn Clauses Satisfiability via Catamorphic Abstractions | Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti | 38m |
A terminating unfolding/folding transformation removes algebraic-data-type arguments from Constrained Horn Clauses by encoding user-specified… | ||
| Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation | John P. Gallagher, Manuel Hermenegildo, José Morales, Pedro López-García | 24m |
Transforms big-step semantics into small-step rules by writing the big-step rules as Horn clauses and encoding an interpreter specialization that executes… | ||
| nothing matches | ||