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
642016
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
312016
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
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
112016
A proof strategy language and proof script generation for Isabelle/HOL
Y Nagashima, R Kumar
International Conference on Automated Deduction, 528-545, 2017
102017
PaMpeR: proof method recommendation system for Isabelle/HOL
Y Nagashima, Y He
ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on …, 2018
72018
Goal-oriented conjecturing for Isabelle/HOL
Y Nagashima, J Parsert
International Conference on Intelligent Computer Mathematics, 225-231, 2018
52018
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Y Nagashima
The 17th Asian Symposium on Programming Languages and Systems (APLAS2019), 2019
22019
Towards Evolutionary Theorem Proving for Isabelle/HOL
Y Nagashima
GECCO2019 Companion (The Genetic and Evolutionary Computation Conference …, 2019
12019
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
arXiv preprint arXiv:1606.02941, 2016
12016
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
Designing Game of Theorems
Y Nagashima
Conference on Artificial Intelligence and Theorem Proving (AITP2018) (arXiv …, 2019
2019
Towards Machine Learning Induction
Y Nagashima
AITP2019; LiVe2019; arXiv preprint arXiv:1812.04088, 2018
2018
Designing Games of Theorem Proving
Y Nagashima
AITP 2018, 2018
2018
Towards Smart Proof Search for Isabelle
Y Nagashima
AITP2017; arXiv preprint arXiv:1701.03037, 2017
2017
The Diameter of Binary Multithreaded Programs
A Malkis, Y Nagashima, S Borgwardt, C Eckert
2013
The Diameter of Multithreaded Programs: Preliminary Findings
S Borgwardt, A Malkis, Y Nagashima
The system can't perform the operation now. Try again later.
Articles 1–20