Engineering-Research-Activity2016｜SHINSHU UNIV.

50/80

Saito LabWhat’sgoingoninourdailyenvironment?Whatinformationisneededtocreateourlivingenvironmentmoresafeandreliable?Thefirststepisbeingabletowatchsituationscarefullyandknowthefactsaboutwhatisgoingoninreal-time.Wehavebeendevelopingoptical,image,andITsensingsystemswhichcanofferlotsofinformationabouttheenvironmentinwhichwelive.Thefusionofoptics&imagingwithITisquitepowerfulinrealizingthisideaanddevelopingthesekindsofsystems.Ourresearchisopentotheworld,butcanalsobefoundintheShinshu-areasuchassky,river/lake,andplant/forest.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 EnvironmentLIFS(laser-inducedfluorescencespectrum)lidarfieldwork:Remotesensingoflivingenvironmentssuchasair-bornepollen,bio-aerosol,waterquality,plantgrowthstatus,andothersatEngineeringcampus(upper)andLakeSuwa(lower).“Realizeyourideasbytakingaction.Don’tstoptothink,butthinkasyouarerunning.Sometimesyouwillfindyourselfchallengingandbattlingdifficulttrialsagainandagain.Believeyourexperiencesthatyou’vegainedbytheaction,thenyouwillbeabletobeattheproblemsyouwillface.”StudentsinSaitolab.wholivebythismottowillnevergiveupiftheyarediscouragedbyonefailureintherealsociety.ComputerScience &EngineeringAfter GraduationIn the FutureShidamaLabThehumansmakemistakes,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.ComputerScience &EngineeringAfter GraduationIn the FutureVerify the correctnessof a specification sheetTheinteractiveteachingmaterialsoftheissueofproof48

※このページを正しく表示するにはFlashPlayer10.2以上が必要です