Skip to content

Naoki Kobayashi

Publication record assembled from the DBLP archive of ranked conferences.

Papers indexed

150

Venues

48

Active years

1992–2026

Best venue rank

A*

Where they publish

Papers

150 indexed papers, newest first.

YearVenueTitleAuthors
2026CAVAutomatic Detection of Reference Counting Bugs in Linux Kernel Drivers.Joe Hattori, Naoki Kobayashi, Ken Sakayori
2026CONCURProphecy-Based Automated Verification of Message-Passing Programs.Takashi Nagatomi, Musashi Katsura, Naoki Kobayashi, Yusuke Matsushita, Ken Sakayori
2026ESOPRelational Hoare Logic for High-Level Synthesis of Hardware Accelerators.Izumi Tanaka, Ken Sakayori, Shinya Takamaeda-Yamazaki, Naoki Kobayashi
2026SIGGRAPHSingle-Stroke Inflatable Tubes Deforming into Freeform Planar Curves.Rin Ishiguro, Jumpei Saito, Mayuka Kuwana, Takumi Yamamoto, Naoki Kobayashi, Ko Fujino, Koya Narumi
2025ESOPOn the Relationship between Dijkstra Monads and Higher-Order Fixpoint Logic.Risa Yamada, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2025SASAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic Data Types.Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2024APLASMode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem.Hiroyuki Katsura, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2024CRiSISCard-Based Secure Evaluation of Decision Trees.Yoshifumi Manabe, Naoki Kobayashi
2024EMNLPVideo Discourse Parsing and Its Application to Multimodal Summarization: A Dataset and Baseline Approaches.Tsutomu Hirao, Naoki Kobayashi, Hidetaka Kamigaito, Manabu Okumura, Akisato Kimura
2024ESORICSCard-Based Cryptographic Protocols for Three-Input Functions with a Standard Deck of Cards Using Private Operations.Naoki Kobayashi, Yoshifumi Manabe
2024MobisysDemo: Image-based Indoor Localization using Object Detection and LSTM.Yuki Aoki, Naoki Kobayashi, Tadashi Okoshi, Jin Nakazawa
2024PEPMProductivity Verification for Functional Programs by Reduction to Termination Verification.Ren Fukaishi, Naoki Kobayashi, Ryosuke Sato
2024PEPMOwnership Types for Verification of Programs with Pointer Arithmetic.Izumi Tanaka, Ken Sakayori, Naoki Kobayashi
2024VMCAIBorrowable Fractional Ownership Types for Verification.Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato, Naoki Kobayashi
2023ACLDataset Distillation with Attention Labels for Fine-tuning BERT.Aru Maekawa, Naoki Kobayashi, Kotaro Funakoshi, Manabu Okumura
2023APLASArgument Reduction of Constrained Horn Clauses Using Equality Constraints.Ryo Ikeda, Ryosuke Sato, Naoki Kobayashi
2023ESOPGradual Tensor Shape Checking.Momoko Hattori, Naoki Kobayashi, Ryosuke Sato
2023TACASNeural Network-Guided Synthesis of Recursive List Functions.Naoki Kobayashi, Minchao Wu
2022EMNLPA Simple and Strong Baseline for End-to-End Neural RST-style Discourse Parsing.Naoki Kobayashi, Tsutomu Hirao, Hidetaka Kamigaito, Manabu Okumura, Masaaki Nagata
2022FLOPSAsynchronous Unfold/Fold Transformation for Fixpoint Logic.Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato
2022IROSIntegration of Variable-height and Hopping Strategies for Humanoid Push Recovery.Ko Yamamoto, Naoki Kobayashi, Taiki Ishigaki, Yuichi Sakemi
2022SASParameterized Recursive Refinement Types for Automated Program Verification.Ryoya Mukai, Naoki Kobayashi, Ryosuke Sato
2021APLASTermination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination.Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
2021CONCURSized Types with Usages for Parallel Complexity of Pi-Calculus Processes.Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi
2021CSLA Cyclic Proof System for HFL_ℕ.Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
2021EMNLPConsidering Nested Tree Structure in Sentence Extractive Summarization with Pre-trained Transformer.Jingun Kwon, Naoki Kobayashi, Hidetaka Kamigaito, Manabu Okumura
2021NAACLImproving Neural RST Parsing Model with Silver Agreement Subtrees.Naoki Kobayashi, Tsutomu Hirao, Hidetaka Kamigaito, Manabu Okumura, Masaaki Nagata
2021PEPMCounterexample generation for program verification based on ownership refinement types.Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada
2021RANLPMaking Your Tweets More Fancy: Emoji Insertion to Texts.Jingun Kwon, Naoki Kobayashi, Hidetaka Kamigaito, Hiroya Takamura, Manabu Okumura
2021SASToward Neural-Network-Guided Program Synthesis and Verification.Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno
2021SASSymbolic Automatic Relations and Their Applications to SMT and CHC Solving.Takumi Shimoda, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato
2020AAAITop-Down RST Parsing Utilizing Granularity Levels in Documents.Naoki Kobayashi, Tsutomu Hirao, Hidetaka Kamigaito, Manabu Okumura, Masaaki Nagata
2020APLASA New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking.Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada
2020DCCGrammar Compression with Probabilistic Context-Free Grammar.Hiroaki Naganuma, Diptarama Hendrian, Ryo Yoshinaka, Ayumi Shinohara, Naoki Kobayashi
2020ESOPRustHorn: CHC-Based Verification for Rust Programs.Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
2020ESOPConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs.John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi
2020FSCDSize-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars.Kazuyuki Asada, Naoki Kobayashi
2020FSCDA Probabilistic Higher-Order Fixpoint Logic.Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
2020FSCDOn Average-Case Hardness of Higher-Order Model Checking.Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
2020SASPredicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking.Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada
2020TACASFold/Unfold Transformations for Fixpoint Logic.Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta
2019APLASA Type-Based HFL Model Checking Algorithm.Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
2019EMNLPSplit or Merge: Which is Better for Unsupervised RST Parsing?Naoki Kobayashi, Tsutomu Hirao, Kengo Nakamura, Hidetaka Kamigaito, Manabu Okumura, Masaaki Nagata
2019ICDMMulti-scale Sequential Pattern Discovery and Alignment for Long-Duration Waveform Similarity Quantification and Interpretation.Masaharu Goto, Naoki Kobayashi, Gang Ren, Mitsunori Ogihara
2019LICSOn the Termination Problem for Probabilistic Higher-Order Recursive Programs.Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
2019PEPMCombining higher-order model checking with refinement type inference.Ryosuke Sato, Naoki Iwayama, Naoki Kobayashi
2019PEPMReduction from branching-time property verification of higher-order programs to HFL validity checking.Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi
2019PPDP10 Years of the Higher-Order Model Checking Project (Extended Abstract).Naoki Kobayashi
2019SASTemporal Verification of Programs via First-Order Fixpoint Logic.Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno
2019SASA Temporal Logic for Higher-Order Functional Programs.Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi
2018APLASHoIce: An ICE-Based Non-linear Horn Clause Solver.Adrien Champion, Naoki Kobayashi, Ryosuke Sato
2018APLASAutomated Synthesis of Functional Programs with Auxiliary Functions.Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada
2018ESOPHigher-Order Program Verification via HFL Model Checking.Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
2018TACASICE-Based Refinement Type Discovery for Higher-Order Functional Programs.Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato
2017ESOPModular Verification of Higher-Order Functional Programs.Ryosuke Sato, Naoki Kobayashi
2017FOSSACSAlmost Every Simply Typed λ-Term Has a Long β-Reduction Sequence.Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada
2017ICALPPumping Lemma for Higher-order Languages.Kazuyuki Asada, Naoki Kobayashi
2017IECONExperimental verifications of control effects for severe conditions at elevator emergency stop based on the safety standards.Keisuke Kawase, Naoki Kobayashi, Toshiko Nakagawa
2017PEPMVerification of code generators via higher-order model checking.Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi
2017POPLOn the relationship between higher-order recursion schemes and higher-order fixpoint logic.Naoki Kobayashi, tienne Lozes, Florian Bruse
2016APLASHigher-Order Model Checking in Direct Style.Taku Terao, Takeshi Tsukada, Naoki Kobayashi
2016APLASVerification of Higher-Order Concurrent Programs with Dynamic Resource Creation.Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi
2016ATVAEquivalence-Based Abstraction Refinement for \mu HORS Model Checking.Xin Li, Naoki Kobayashi
2016ICALPOn Word and Frontier Languages of Unsafe Higher-Order Grammars.Kazuyuki Asada, Naoki Kobayashi
2016ICFPCompact bit encoding schemes for simply-typed lambda-terms.Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara
2016ICFPAutomatically disproving fair termination of higher-order functional programs.Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi
2016ICISPDemosaicking Method for Multispectral Images Based on Spatial Gradient and Inter-channel Correlation.Shu Ogawa, Kazuma Shinoda, Madoka Hasegawa, Shigeo Kato, Masahiro Ishikawa, Hideki Komagata, Naoki Kobayashi
2016IPASOptimal Transparent Wavelength and Arrangement for Multispectral Filter Array.Yudai Yanagi, Kazuma Shinoda, Madoka Hasegawa, Shigeo Kato, Masahiro Ishikawa, Hideki Komagata, Naoki Kobayashi
2016POPLTemporal verification of higher-order functional programs.Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
2015APLASDecision Algorithms for Checking Definability of Order-2 Finitary PCF.Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi
2015APLASAutomata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs.Yuma Matsumoto, Naoki Kobayashi, Hiroshi Unno
2015CAVPredicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs.Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
2015LICSAutomata-Based Abstraction Refinement for HORS Model Checking.Naoki Kobayashi, Xin Li
2015MVAThree-DoF pose estimation of asteroids by appearance-based linear regression with divided parameter space.Naoki Kobayashi, Yuji Oyamada, Yoshihiko Mochizuki, Hiroshi Ishikawa
2015PEPMVerifying Relational Properties of Functional Programs by First-Order Refinement.Kazuyuki Asada, Ryosuke Sato, Naoki Kobayashi
2014APLASA ZDD-Based Efficient Higher-Order Model Checking Algorithm.Taku Terao, Naoki Kobayashi
2014COMPSACProposal and Evaluation of Safe and Efficient Log Signature Scheme for the Preservation of Evidence.Naoki Kobayashi, Ryichi Sasaki
2014CONCURDeadlock Analysis of Unbounded Process Networks.Elena Giachino, Naoki Kobayashi, Cosimo Laneve
2014CONCURPairwise Reachability Analysis for Higher Order Concurrent Programs by Higher-Order Model Checking.Kazuhide Yasukata, Naoki Kobayashi, Kazutaka Matsuda
2014DCCEfficient Algorithm and Coding for Higher-Order Compression.Kazuya Yaguchi, Naoki Kobayashi, Ayumi Shinohara
2014ESOPAutomatic Termination Verification for Higher-Order Functional Programs.Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, Naoki Kobayashi
2014FOSSACSUnsafe Order-2 Tree Languages Are Context-Sensitive.Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada
2014FOSSACSComplexity of Model-Checking Call-by-Value Programs.Takeshi Tsukada, Naoki Kobayashi
2013APLASPractical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes.Koichi Fujima, Sohei Ito, Naoki Kobayashi
2013CSLSaturation-Based Model Checking of Higher-Order Recursion Schemes.Christopher H. Broadbent, Naoki Kobayashi
2013ESOPModel-Checking Higher-Order Programs with Recursive Types.Naoki Kobayashi, Atsushi Igarashi
2013LICSPumping by Typing.Naoki Kobayashi
2013PEPMTowards a scalable software model checker for higher-order programs.Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi
2013POPLAutomating relatively complete verification of higher-order functional programs.Hiroshi Unno, Tachio Terauchi, Naoki Kobayashi
2012CPPProgram Certification by Higher-Order Model Checking.Naoki Kobayashi
2012FLOPSExact Flow Analysis by Higher-Order Model Checking.Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi
2012ISITACooperative reception scheme using multiple terminals for digital terrestrial television broadcasting One-Segment Service.Ryo Araki, Naoki Kobayashi, Akira Nakamura, Kohei Ohno, Makoto Itami
2012PEPMFunctional programs as compressed data.Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara
2011ATVAType-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols.Morten Dahl, Naoki Kobayashi, Yunde Sun, Hans Httel
2011FOSSACSA Practical Linear Time Algorithm for Trivial Automata Model Checking of Higher-Order Recursion Schemes.Naoki Kobayashi
2011FUSIONFault parameter estimation with data assimilation on infrasound variations due to big earthquakes.Hiromichi Nagao, Naoki Kobayashi, Shin'ya Nakano, Tomoyuki Higuchi
2011LICSHigher-Order Model Checking: From Theory to Practice.Naoki Kobayashi
2011PLDIPredicate abstraction and CEGAR for higher-order model checking.Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno
2010APLASVerification of Tree-Processing Programs via Higher-Order Model Checking.Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi
2010FOSSACSUntyped Recursion Schemes and Infinite Intersection Types.Takeshi Tsukada, Naoki Kobayashi
2010POPLHigher-order multi-parameter tree transducers and recursion schemes for program verification.Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno
2009APLASTypes and Recursion Schemes for Higher-Order Program Verification.Naoki Kobayashi
2009APLASFractional Ownerships for Safe Memory Deallocation.Kohei Suenaga, Naoki Kobayashi
2009ESOPType-Based Automated Verification of Authenticity in Cryptographic Protocols.Daisuke Kikuchi, Naoki Kobayashi
2009ICALPComplexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus.Naoki Kobayashi, C.-H. Luke Ong
2009LICSA Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes.Naoki Kobayashi, C.-H. Luke Ong
2009POPLTypes and higher-order recursion schemes for verification of higher-order programs.Naoki Kobayashi
2009PPDPModel-checking higher-order functions.Naoki Kobayashi
2009PPDPDependent type inference with interpolants.Hiroshi Unno, Naoki Kobayashi
2008CAVA Hybrid Type System for Lock-Freedom of Mobile Processes.Naoki Kobayashi, Davide Sangiorgi
2008ESOPLinear Declassification.Yta Kaneko, Naoki Kobayashi
2008FLOPSSubstructural Type Systems for Program Analysis.Naoki Kobayashi
2008FLOPSOn-Demand Refinement of Dependent Types.Hiroshi Unno, Naoki Kobayashi
2007APLASType-Based Verification of Correspondence Assertions for Communication Protocols.Daisuke Kikuchi, Naoki Kobayashi
2007ESOPType-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts.Kohei Suenaga, Naoki Kobayashi
2007ICALPUndecidability of 2-Label BPP Equivalences and Behavioral Type Systems for theNaoki Kobayashi, Takashi Suto
2007LICSEnvironmental Bisimulations for Higher-Order Languages.Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
2006CONCURA New Type System for Deadlock-Free Processes.Naoki Kobayashi
2006PEPMResource usage analysis for a functional language with exceptions.Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
2006PLDICombining type-based analysis and model checking for finding counterexamples against non-interference.Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
2006VMCAIResource Usage Analysis for theNaoki Kobayashi, Kohei Suenaga, Lucian Wischik
2005LOPSTRExtension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives.Kohei Suenaga, Naoki Kobayashi, Akinori Yonezawa
2004APLASTranslation of Tree-Processing Programs into Stream-Processing Programs Based on Ordered Linear Type.Koichi Kodama, Kohei Suenaga, Naoki Kobayashi
2004APLASRegion-Based Memory Management for a Dynamically-Typed Language.Akihito Nagata, Naoki Kobayashi, Akinori Yonezawa
2003APLASUseless Code Elimination and Programm Slicing for the Pi-Calculus.Naoki Kobayashi
2002APLASType-Based Information Analysis for Low-Level Languages.Naoki Kobayashi, Keita Shirane
2002ICIPPractical extension to CIELUV color space to improve uniformity.Seishi Takamura, Naoki Kobayashi
2002ICIPA nonlinear spatio-temporal diffusion and its application to prefiltering in MPEG-4 video coding.Hiroyuki Tsuji, Toru Sakatani, Yoshiyuki Yashima, Naoki Kobayashi
2002PEPMA new type system for JVM lock primitives.Futoshi Iwama, Naoki Kobayashi
2002POPLResource usage analysis.Atsushi Igarashi, Naoki Kobayashi
2001APLASResource Usage Analysis.Atsushi Igarashi, Naoki Kobayashi
2001ICIPEdge preserving pre-post filtering for low bitrate video coding.Hideaki Kimata, Yoshiyuki Yashima, Naoki Kobayashi
2001ICIPConstructing a uniform color space for visually lossless color representation and image coding.Seishi Takamura, Naoki Kobayashi
2001ICIPMPEG-2 one-pass variable bit rate control algorithm and its LSI implementation.Seishi Takamura, Naoki Kobayashi
2001POPLA generic type system for the Pi-calculus.Atsushi Igarashi, Naoki Kobayashi
2000CONCURAn Implicitly-Typed Deadlock-Free Process Calculus.Naoki Kobayashi, Shin Saito, Eijiro Sumii
2000ISCASAutomatic two-layer video object plane generation scheme and its application to MPEG-4 video coding.Kumi Jinzenji, Shigeki Okada, Hiroshi Watanabe, Naoki Kobayashi
2000PEPMType-Based Useless Variable Elimination.Naoki Kobayashi
2000PEPMOnline-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract).Eijiro Sumii, Naoki Kobayashi
1999POPLQuasi-Linear Types.Naoki Kobayashi
1997LICSA Partially Deadlock-Free Typed Process Calculus.Naoki Kobayashi
1997SASType-Based Analysis of Communication for Concurrent Programming Languages.Atsushi Igarashi, Naoki Kobayashi
1996EuroParPartial Evaluation Scheme for Concurrent Languages and Its Correctness.Haruo Hosoya, Naoki Kobayashi, Akinori Yonezawa
1996POPLLinearity and the Pi-Calculus.Naoki Kobayashi, Benjamin C. Pierce, David N. Turner
1995SASStatic Analysis of Communication for Asynchronous Concurrent Programming LanguagesNaoki Kobayashi, Motoki Nakade, Akinori Yonezawa
1994ICASSPHalftoning technique using genetic algorithm.Naoki Kobayashi, Hideo Saito
1994ICECEvolutionary Computation Approaches to Halftoning Algorithm.Hideo Saito, Naoki Kobayashi
1994OOPSLAType-Theoretic Foundations for Concurrent Object-Oriented Programming.Naoki Kobayashi, Akinori Yonezawa
1993HCIA Human Memory Model Based on Search Patterns.Tomoko Saka, Hideaki Ozawa, Naoki Kobayashi
1992PSCAsynchronous Communication Model Based on Linear Logic.Naoki Kobayashi, Akinori Yonezawa