Yutaka Nagashima
Yutaka Nagashima
CIIRC, Czech Technical University, University of Innsbruck
Verified email at cvut.cz - 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
782016
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
332016
A proof strategy language and proof script generation for Isabelle/HOL
Y Nagashima, R Kumar
International Conference on Automated Deduction, 528-545, 2017
162017
PaMpeR: proof method recommendation system for Isabelle/HOL
Y Nagashima, Y He
ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on …, 2018
122018
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
122016
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
112016
Goal-oriented conjecturing for Isabelle/HOL
Y Nagashima, J Parsert
International Conference on Intelligent Computer Mathematics, 225-231, 2018
102018
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Y Nagashima
The 17th Asian Symposium on Programming Languages and Systems (APLAS2019), 2019
62019
Towards Evolutionary Theorem Proving for Isabelle/HOL
Y Nagashima
GECCO2019 Companion (The Genetic and Evolutionary Computation Conference …, 2019
32019
Smart Induction for Isabelle/HOL (Tool Paper)
YN CIIRC
PROCEEDINGS OF THE 20TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED …, 2020
22020
Simple dataset for proof method recommendation in isabelle/hol
Y Nagashima
International Conference on Intelligent Computer Mathematics, 297-302, 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
A proof strategy language and proof script generation for isabelle
Y Nagashima, R Kumar
CoRR, abs/1606.02941, 2016
12016
SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL
Y Nagashima
arXiv preprint arXiv:2010.10296, 2020
2020
Faster Smarter Induction in Isabelle/HOL with SeLFiE
Y Nagashima
arXiv preprint arXiv:2009.09215, 2020
2020
Towards United Reasoning for Automatic Induction in Isabelle/HOL
Y Nagashima
arXiv preprint arXiv:2005.12737, 2020
2020
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description)
Y Nagashima
arXiv preprint arXiv:2004.10667, 2020
2020
Smart Induction for Isabelle/HOL (System Description)
Y Nagashima
arXiv preprint arXiv:2001.10834, 2020
2020
Domain-Specific Language to Encode Induction Heuristics
Y Nagashima
ICFP 2019 Student Research Competition (arXiv preprint arXiv:1907.02594), 2019
2019
The system can't perform the operation now. Try again later.
Articles 1–20