Hiroshi Unno

Orcid: 0000-0002-4225-8195

Affiliations:
  • University of Tsukuba, Japan


According to our database1, Hiroshi Unno authored at least 34 papers between 2006 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers.
Proc. ACM Program. Lang., January, 2024

2023
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.
Proc. ACM Program. Lang., January, 2023

Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations.
Proc. ACM Program. Lang., January, 2023

Optimal CHC Solving via Termination Proofs.
Proc. ACM Program. Lang., January, 2023

2022
Software model-checking as cyclic-proof search.
Proc. ACM Program. Lang., 2022

Temporal Verification with Answer-Effect Modification.
CoRR, 2022

2021
Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
CoRR, 2021

Toward Neural-Network-Guided Program Synthesis and Verification.
Proceedings of the Static Analysis - 28th International Symposium, 2021

Constraint-Based Relational Verification.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

Decision Tree Learning in CEGIS-Based Termination Analysis.
Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020
Program Verification via Predicate Constraint Satisfiability Modulo Theories.
CoRR, 2020

Probabilistic Inference for Predicate Constraint Satisfaction.
Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence, 2020

2019
Temporal Verification of Programs via First-Order Fixpoint Logic.
Proceedings of the Static Analysis - 26th International Symposium, 2019

2018
Relatively complete refinement type system for verification of higher-order non-deterministic programs.
Proc. ACM Program. Lang., 2018

A Fixpoint Logic and Dependent Effects for Temporal Property Verification.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Propositional Dynamic Logic for Higher-Order Functional Programs.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

2017
Automating Induction for Solving Horn Clauses.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016
Automating Induction for Solving Horn Clauses.
CoRR, 2016

Temporal verification of higher-order functional programs.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

2015
Verification of tree-processing programs via higher-order mode checking.
Math. Struct. Comput. Sci., 2015

Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Refinement Type Inference via Horn Constraint Optimization.
Proceedings of the Static Analysis - 22nd International Symposium, 2015

Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement.
Proceedings of the Programming Languages and Systems, 2015

Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs.
Proceedings of the Programming Languages and Systems - 13th Asian Symposium, 2015

2014
Automatic Termination Verification for Higher-Order Functional Programs.
Proceedings of the Programming Languages and Systems, 2014

2013
Automating relatively complete verification of higher-order functional programs.
Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Towards a scalable software model checker for higher-order programs.
Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, 2013

2011
Predicate abstraction and CEGAR for higher-order model checking.
Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, 2011

2010
Higher-order multi-parameter tree transducers and recursion schemes for program verification.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

Verification of Tree-Processing Programs via Higher-Order Model Checking.
Proceedings of the Programming Languages and Systems - 8th Asian Symposium, 2010

2009
Dependent type inference with interpolants.
Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2009

2008
On-Demand Refinement of Dependent Types.
Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

2006
Combining type-based analysis and model checking for finding counterexamples against non-interference.
Proceedings of the 2006 Workshop on Programming Languages and Analysis for Security, 2006


  Loading...