Folgen
Yutaka Nagashima
Yutaka Nagashima
Institute of Computer Science, the Czech Academy of Sciences
Bestätigte E-Mail-Adresse bei cs.cas.cz - Startseite
Titel
Zitiert von
Zitiert von
Jahr
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
1352016
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
592016
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
312016
PaMpeR: proof method recommendation system for Isabelle/HOL
Y Nagashima, Y He
ASE 2018 Proceedings of the 33rd ACM/IEEE International Conference on …, 2018
302018
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
292017
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
192016
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Y Nagashima
The 17th Asian Symposium on Programming Languages and Systems (APLAS2019), 2019
152019
Goal-oriented conjecturing for Isabelle/HOL
Y Nagashima, J Parsert
Intelligent Computer Mathematics: 11th International Conference, CICM 2018 …, 2018
152018
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
62021
Simple dataset for proof method recommendation in isabelle/hol
Y Nagashima
International Conference on Intelligent Computer Mathematics, 297-302, 2020
62020
SeLFiE: Modular semantic reasoning for induction in Isabelle/HOL
Y Nagashima
CoRR, abs/2010.10296, 2020
32020
Template-Based Conjecturing for Automated Induction in Isabelle/HOL
Y Nagashima, Z Xu, N Wang, DS Goc, J Bang
International Conference on Fundamentals of Software Engineering, 112-125, 2023
22023
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
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
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20