Naoki Kobayashi
where else to find them
no profile links on file
what they talk about
all 5 in the filters
where they keep going back
all 8 in the filters
on a stage with
all 22 in the filters
who talks about the same things
- Ryosuke Sato10 talks
- Takeshi Tsukada16 talks
- Hiroshi Unno18 talks
- Hiroyuki Katsura5 talks
- Tachio Terauchi4 talks
- Sharon Shoham13 talks
| title | conference | date |
|---|---|---|
| Solvable Tuple Patterns and Their Applications to Program Verification | PLDI 2026 | 2026-06-15 |
Introduces solvable tuple patterns (STPs) and conjunctive STPs as a representation for relations among sequences that are learnable from only positive samples… | ||
| Automated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…) | SAS 2025 | 2025-10-13 |
A procedure automatically abstracts CHCs over algebraic data types to integer CHCs by synthesizing catamorphisms (generalized folds) via a CEGAR-style loop… | ||
| On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus | POPL 2025 | 2025-01-19 |
Gives simple proofs that the reachability problem becomes undecidable for four undecidable extensions of finitary PCF and then isolates a decidable fragment… | ||
| Productivity Verification for Functional Programs by Reduction to Termination Ve... | PEPM 2024 | 2024-01-16 |
Method translates coinductive values into functions that take a path (integer list) and returns the element, turning productivity into reduction to termination… | ||
| Ownership Types for Verification of Programs with Pointer Arithmetic | PEPM 2024 | 2024-01-16 |
Extends Toman et al.’s refinement-plus-ownership type system to handle pointer arithmetic, proves soundness, and implements a prototype tool that verifies… | ||
| Borrowable Fractional Ownership Types for Verification | VMCAI 2024 | 2024-01-15 |
Combines ConSORT’s fractional ownership and RustHorn’s borrowable (lifetime) ownership into borrowable fractional ownership types, a flow‑sensitive type system… | ||
| Higher-Order Property-Directed Reachability | ICFP 2023 | 2023-09-04 |
Formalizes a higher-order extension of PDR that extends PDR to nu-HFL(Z) so transition systems can be described by higher-order recursive functions, implements… | ||
| HFL(Z) Validity Checking for Automated Program Verification | POPL 2023 | 2023-01-15 |
Proposes an automated validity checker for HFL(Z) formulas that encodes higher-order program verification (termination, nontermination, fair variants… | ||
| A New Refinement Type System for Automated nu-HFLZ Validity Checkin | SPLASH 2022 | 2022-12-05 |
A refinement type system targets validity checking for a fragment of vHFLZ (no least fixpoints) and produces template-based constraints that are solved to… | ||
| Termination Analysis for the pi-Calculus by Reduction to Sequential Program Termination | SPLASH 2022 | 2022-12-05 |
Proposes an automated reduction that translates pi-calculus processes into sequential C programs so termination of the C program implies termination of the… | ||
| On Type-Based Techniques for Program Manipulation | PEPM 2022 | 2022-01-17 |
Type-directed transformations formalize program rewrites as typing judgments and prove soundness by preservation under reduction plus soundness for values. Two… | ||
| Symbolic Automatic Relations and Their Applications to SMT and CHC Solving | SAS 2021 | 2021-10-17 |
Defines symbolic automatic relations that combine symbolic automata and automatic relations and proves they are closed under Boolean ops; shows satisfiability… | ||
| Termination Analysis for the \$\pi\$-Calculus by Reduction to Sequential Program Termination | APLAS 2021 | 2021-10-17 |
Proposes an automated reduction that translates π-calculus to C so termination of the sequential program implies termination of the original process, and… | ||
| Toward Neural-Network-Guided Program Synthesis and Verification | SAS 2021 | 2021-10-17 |
Proposes NeuGuS, a gray-box method that trains neural nets (four-layer; sometimes three-layer) then extracts inequalities from weights/biases to build Boolean… | ||
| Coq to C Translation with Partial Evaluation + Counterexample Generation | PEPM 2021 | 2021-01-18 |
Builds a verified Coq-to-C code generator that uses a custom codogen plugin and a partial-evaluation pipeline to monomorphize polymorphic/dependent functions… | ||
| Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking | SAS 2020 | 2020-11-18 |
Proposes an algorithm that combines νHFL(ℤ) predicate abstraction with predicate abstraction and CEGAR to decide higher‑order CHC/νHFL(ℤ) validity, implements… | ||
| nothing matches | ||