塚田 武志

Optimal CHC Solving via Termination Proofs. 

Proc. ACM Program. Lang. 7(POPL) 604-631 2023年1月  査読有り

HFL(Z) Validity Checking for Automated Program Verification. 

Proc. ACM Program. Lang. 7(POPL) 154-184 2023年1月  査読有り

Software model-checking as cyclic-proof search 

Proceedings of the ACM on Programming Languages 6(POPL) 1-29 2022年1月16日  査読有り筆頭著者

Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings 

Proceedings of 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS 2022) 60-13 2022年  査読有り筆頭著者責任著者

CPS transformation with affine types for call-by-value implicit polymorphism 

Proceedings of the ACM on Programming Languages 5(ICFP) 1-30 2021年8月22日  査読有り

Counterexample generation for program verification based on ownership refinement types 

Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation 2021年1月18日  査読有り

Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination 

Programming Languages and Systems 265-284 2021年  査読有り

Enhancing Loop-Invariant Synthesis via Reinforcement Learning. 

CoRR abs/2107.09766 2021年  

Output Without Delay: A π-Calculus Compatible with Categorical Semantics. 

Proc. of 6TH INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION 32-22 2021年  査読有り

A Cyclic Proof System for HFL_ℕ. 

29th EACSL Annual Conference on Computer Science Logic(CSL) 29-22 2021年  査読有り

Signature restriction for polymorphic algebraic effects 

Proceedings of the ACM on Programming Languages 4(ICFP) 1-30 2020年8月2日  査読有り

On Computability of Logical Approaches to Branching-Time Property Verification of Programs 

Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science 2020年7月8日  査読有り筆頭著者責任著者

Predicate Abstraction and CEGAR for $$\nu \mathrm {HFL}_\mathbb {Z}$$ Validity Checking 

Static Analysis 134-155 2020年  査読有り

On Average-Case Hardness of Higher-Order Model Checking. 

FSCD 2020 21-23 2020年  査読有り

A Probabilistic Higher-Order Fixpoint Logic 

FSCD 2020 19-22 2020年  査読有り

RustHorn: CHC-Based Verification for Rust Programs 

Programming Languages and Systems 484-514 2020年  査読有り

A New Refinement Type System for Automated $$\nu \text {HFL}_\mathbb {Z}$$ Validity Checking 

Programming Languages and Systems 86-104 2020年  査読有り

A Categorical Model of an i/o-typed pi-calculus 

Programming Languages and Systems 640-667 2019年  査読有り最終著者