工学部_研究紹介_2020_英語版

28/80

YasunariShidamaThehumansmakemistakes,soitisimportanttoverifythecorrectnessofmathematicaltheoremswithacomputer.InShidamaLaboratory,studentsworkonformalizationofmathematicsandcomputeraidedverification.Toverifyamathematicaltheoremwithacomputer,wewriteaproofofthetheorembytheformalizationlanguage.Thenwecanverifythecorrectnesswithacomputerlogicallyandmathematically.Thismethodcanbeappliedtotheinspectionofthedevelopmentoftheengineeringsystemanditsmovement.Acomputerprogramisadescriptionwithlogicaloperationsthatmakesoutputdatafrominputdatabyaformallanguage,thuswecanexpresstheoperationsasamathematicalproposition.Itisanincompletemethodforhumanstoinspectresultsusingdataandtoanalyzealloperations,aswemakemistakes.Weshouldverifythemathematicalcorrectnessofacomputerprogramwithacomputer.Thenwecanmakeacomputerprograminwhichnormaloperationsaremathematicallyguaranteed.Weparticipateinaninternationalinvestigationproject,thataimstomakethelibraryofformalizedtheoremsandproofsofallmathematics.Thepurposeistoapplyformalizedmathematicstocomputersoftwaredevelopment.Andwearedevelopingasystemthatcanmakeacomputerprogramthatnormaloperationsaremathematicallyguaranteed.ProfessorHe has been on the faculty in the Dept. of Computer Science and Engineering since 1990.Are interested in Formalization of Mathematics and Computer Aided Verification.Formalization of Mathematics and Computer Aided VerificationOurgraduatesareworkingascomputerscienceengineersastheyhavelogicalandmathematicalthinkingskills.After GraduationIn the FutureVerify the correctnessof a specification sheetTheinteractiveteachingmaterialsoftheissueofproofElectrical& Computer EngineeringElectrical& Computer EngineeringIn the FutureAfter GraduationMitsuhideSatoThissystemhasnocrankmechanism.Sincethecombustionenergyisconverteddirectlyintoelectricpower,themechanicallosscanbereduced.Serieshybridvehiclesusingfree-pistonenginecoupledwithlineargeneratorareexpectedforhigh-efficiencyenergyconversionsystems.Suchenginesdonothaveacrankmechanism,whichgreatlyreducesthefrictionloss.Inaddition,thepistonactioncanbecontrolledfreelybythegenerationbrakingthrustbyusinganinvertercontrol.OurLaboratoryisinterestedingeneratordesignandinverterpowergenerationcontrolforthepurposeofimprovingpowergenerationefficiency.Wearealsostudyingtheeffectofpistonmovementontheefficiencyofpowergenerationexperimentsusingsmallengines.Inrecentyears,electrificationhasgainedpopularityworldwidefortherealizationofasustainableautomotiveindustry.Thissystemwillbefundamentaltechnologiesforthefutureofautomotivesociety.Youwillworkasengineersandtechniciansinelectricalorprecisionmeasurementcompanies.AssistantprofessorPh.D.:ShinshuUniversityResearchfield:Lineargenerator/motorFree-piston Engine Linear Power Generation SystemBatteryFree-pistonInverterSpringCoilChargingSNNSNSSNSNNSNSSNSNSNSNNSSNSNSNNSLineargeneratorValveSparkplugFuelinjectorCombustionchamberSpringchamberPermanentmagnet26