Follow
Yutaka Nagashima
Yutaka Nagashima
Verified email at huawei.com - Homepage
Title
Cited by
Cited by
Year
Cogent: Verifying high-assurance file system implementations
S Amani, A Hixon, Z Chen, C Rizkallah, P Chubb, L O'Connor, J Beeren, ...
ACM SIGARCH Computer Architecture News 44 (2), 175-188, 2016
1282016
Refinement through restraint: Bringing down the cost of verification
L O'Connor, Z Chen, C Rizkallah, S Amani, J Lim, T Murray, Y Nagashima, ...
ACM SIGPLAN Notices 51 (9), 89-102, 2016
552016
PaMpeR: proof method recommendation system for Isabelle/HOL
Y Nagashima, Y He
ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on …, 2018
282018
A proof strategy language and proof script generation for Isabelle/HOL
Y Nagashima, R Kumar
Automated Deduction–CADE 26: 26th International Conference on Automated …, 2017
282017
A Framework for the Automatic Formal Verification of Refinement from Cogent to C
C Rizkallah, J Lim, Y Nagashima, T Sewell, Z Chen, L O’Connor, T Murray, ...
International Conference on Interactive Theorem Proving, 323-340, 2016
272016
COGENT: certified compilation for a functional systems language
L O'Connor, C Rizkallah, Z Chen, S Amani, J Lim, Y Nagashima, T Sewell, ...
arXiv preprint arXiv:1601.05520, 2016
162016
Goal-oriented conjecturing for Isabelle/HOL
Y Nagashima, J Parsert
Intelligent Computer Mathematics: 11th International Conference, CICM 2018 …, 2018
152018
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Y Nagashima
The 17th Asian Symposium on Programming Languages and Systems (APLAS2019), 2019
142019
Towards Evolutionary Theorem Proving for Isabelle/HOL
Y Nagashima
GECCO2019 Companion (The Genetic and Evolutionary Computation Conference …, 2019
102019
Smart induction for Isabelle/HOL (tool paper)
Y Nagashima
# PLACEHOLDER_PARENT_METADATA_VALUE# 1, 245-254, 2020
72020
Faster Smarter Proof by Induction in Isabelle/HOL.
Y Nagashima
IJCAI, 1981-1988, 2021
42021
Simple dataset for proof method recommendation in isabelle/hol
Y Nagashima
International Conference on Intelligent Computer Mathematics, 297-302, 2020
42020
Definitional quantifiers realise semantic reasoning for proof by induction
Y Nagashima
International Conference on Tests and Proofs, 48-66, 2022
22022
Property-based conjecturing for automated induction in Isabelle/HOL
Y Nagashima, Z Xu, N Wang, DS Goc, J Bang
CoRR, abs/2212.11151, 2022
22022
SeLFiE: Modular semantic reasoning for induction in Isabelle/HOL
Y Nagashima
CoRR, abs/2010.10296, 2020
22020
Genetic Algorithm for Program Synthesis
Y Nagashima
International Conference on Fundamentals of Software Engineering, 104-111, 2023
12023
Towards united reasoning for automatic induction in Isabelle/HOL
Y Nagashima
arXiv preprint arXiv:2005.12737, 2020
12020
Simple dataset for proof method recommendation in isabelle/hol (dataset description)
Y Nagashima
arXiv preprint arXiv:2004.10667, 2020
12020
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML
Y Nagashima, L O'Connor
ML2016; arXiv preprint arXiv:1608.03350, 2016
12016
Keep failed proof attempts in memory
Y Nagashima
Isabelle Workshop, Nancy, France, 2016
12016
The system can't perform the operation now. Try again later.
Articles 1–20