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

32/84

Saito LabWhat’sgoingoninourdailyenvironment?Whatinformationisneededtocreateourlivingenvironmentmoresafeandreliable?Thefirststepisbeingabletowatchsituationscarefullyandknowthefactsaboutwhatisgoingoninreal-time.WehavebeendevelopingLIDARusingadvancedoptical,image,andITsensingtechnologieswhichcanofferlotsofinformationabouttheenvironmentinwhichwelive.Ourresearchisopentotheworld,butcanalsobefoundintheShinshu-areasuchassky,river/lake,plant/forest,mountain/earthandothersrelatingtonaturalenvironmentandhumanlivingsphere.Humanshavecreatedrichandcomfortablelivingenvironmentsbyusingtheenergyof“light”fromtheSunverywell.Let’simaginethefutureworldfullofbrightsun-light.Thechancesandplacesforopticaltechnology,whichisagiftfromnature,willbefoundanywhere.EspeciallytogetherwithIT,itwillbemoreactiveineveryregionoftheworld.IT-basedopticaltechnologywillsurelyopeninnovativeworldsforhumanlivingwithbettersecurityandsafetythanever.YasunoriSaito,Professorsince 2004.Always curious to know what happens in the relationship of humans and nature. Field Informatics, Optical & Spectroscopic Sensing, Imaging Technology, and their applications to Environmental Sensing.Optical, Image, and IT Sensing Technologies Creating a Safe and Reliable EnvironmentConceptofopticalremotesensing(LIDAR)forearth/livingenvironment(Upper),andLIFS(laser-inducedfluorescencespectrum)lidarfieldworkofwaterqualitysensingatLakeSuwa(lower).“Realizeyourideasbytakingaction.Don’tstoptothink,butthinkasyouarerunning.Sometimesyouwillfindyourselfchallengingandbattlingdifficulttrialsagainandagain.Believeyourexperiencesthatyou’vegainedbytheaction,thenyouwillbeabletobeattheproblemsyouwillface.”StudentsinSaitolab.wholivebythismottowillnevergiveupiftheyarediscouragedbyonefailureintherealsociety.After GraduationIn the FutureElectrical& Computer EngineeringShidamaLabThehumansmakemistakes,soitisimportanttoverifythecorrectnessofmathematicaltheoremswithacomputer.InShidamaLaboratory,studentsworkonformalizationofmathematicsandcomputeraidedverification.Toverifyamathematicaltheoremwithacomputer,wewriteaproofofthetheorembytheformalizationlanguage.Thenwecanverifythecorrectnesswithacomputerlogicallyandmathematically.Thismethodcanbeappliedtotheinspectionofthedevelopmentoftheengineeringsystemanditsmovement.Acomputerprogramisadescriptionwithlogicaloperationsthatmakesoutputdatafrominputdatabyaformallanguage,thuswecanexpresstheoperationsasamathematicalproposition.Itisanincompletemethodforhumanstoinspectresultsusingdataandtoanalyzealloperations,aswemakemistakes.Weshouldverifythemathematicalcorrectnessofacomputerprogramwithacomputer.Thenwecanmakeacomputerprograminwhichnormaloperationsaremathematicallyguaranteed.Weparticipateinaninternationalinvestigationproject,thataimstomakethelibraryofformalizedtheoremsandproofsofallmathematics.Thepurposeistoapplyformalizedmathematicstocomputersoftwaredevelopment.Andwearedevelopingasystemthatcanmakeacomputerprogramthatnormaloperationsaremathematicallyguaranteed.YasunariShidamaProfessorHas 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 Engineering30