|
Showing 1 - 5 of
5 matches in All Departments
|
Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008, Proceedings (Paperback, 2008 ed.)
Otmane Ait Mohamed, Cesar Munoz, Sofiene Tahar
|
R1,570
Discovery Miles 15 700
|
Ships in 10 - 15 working days
|
This volume constitutes the proceedings of the 21st International
Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008),
which was held during August 18-21, 2008 in Montreal, Canada.
TPHOLs covers all aspects of theorem proving in higher order logics
as well as related topics in theorem proving and veri?cation. There
were 40 papers submitted to TPHOLs 2008 in the full research c-
egory, each of which was refereed by at least four reviewers
selected by the ProgramCommittee. Of these submissions, 17
researchpapers and 1 proofpearl were accepted for presentation at
the conference and publication in this v- ume. In keeping with
longstanding tradition, TPHOLs 2008 also o?ered a venue for the
presentation of emerging trends, where researchers invited
discussion by means of a brief introductory talk and then discussed
their work at a poster session. A supplementary proceedings volume
was published as a 2008 technical report of Concordia University.
The organizersaregratefulto MichaelGordonand StevenMiller for
agreeing
togiveinvitedtalksatTPHOLs2008.Aspartofthecelebrationofthe20yearsof
TPHOLs, TPHOLs 2008 invited tool developers and expert users to
give special tool presentations of the most representative theorem
provers in higher order logics. The following speakers kindly
accepted our invitation and we aregrateful tothem: YvesBertot(Coq),
MattKaufmann(ACL2), SamOwre(PVS), Konrad Slind (HOL), and Makarius
Wenzel (Isabel
|
Theorem Proving in Higher Order Logics - 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings (Paperback, 2002 ed.)
Victor A. Carreno, Cesar A. Munoz, Sofiene Tahar
|
R1,700
Discovery Miles 17 000
|
Ships in 10 - 15 working days
|
Thisvolumecontainstheproceedingsofthe 15th International Conference
on TheoremProvinginHigherOrderLogics(TPHOLs2002)heldon20-23August
2002inHampton,Virginia,USA. Theconferenceservesasavenueforthep-
sentationofworkintheoremprovinginhigher-orderlogics,andrelatedareas
indeduction,formalspeci?cation,softwareandhardwareveri?cation,andother
applications.
Eachofthe34paperssubmittedinthefullresearchcategorywasrefereedby
atleastthreereviewersfromtheprogramcommitteeorbyareviewerappointed
bytheprogramcommittee. Ofthesesubmissions,20paperswereacceptedfor
presentationattheconferenceandpublicationinthisvolume.
Followingawell-establishedtraditioninthisconferenceseries,TPHOLs2002
alsoo?eredavenueforthepresentationofworkinprogress. Fortheworkin
progresstrack,shortintroductorytalksweregivenbyresearchers,followedby
anopenpostersessionforfurtherdiscussion.
Papersacceptedforpresentation
inthistrackhavebeenpublishedasConferenceProceedingsCPNASA-2002-
211736.
TheorganizerswouldliketothankRickyButlerandG'erardHuetforgra-
fullyacceptingourinvitationtogivetalksatTPHOLs2002. RickyButlerwas
instrumentalintheformationoftheFormalMethodsprogramattheNASA
LangleyResearchCenterandhasledthegroupsinceitsbeginnings. TheNASA
LangleyFormalMethodsgroup,underRickyButler'sguidance,hasfunded,
beeninvolvedin,orin?uencedmanyformalveri?cationprojectsintheUSover
morethantwodecades. In1998G'erardHuetreceivedtheprestigiousHerbrand
Awardforhisfundamentalcontributionstotermrewritingandtheoremproving
inhigher-orderlogic,aswellasmanyotherkeycontributionstothe?eldof-
tomatedreasoning. HeistheoriginatoroftheCoqSystem,underdevelopment
atINRIA-Rocquencourt. Dr.
Huet'scurrentmaininterestiscomputationall-
guistics,howeverhisworkcontinuestoin?uenceresearchersaroundtheworldin
awidespectrumofareasintheoreticalcomputerscience,formalmethods,and
softwareengineering.
ThevenueoftheTPHOLsconferencetraditionallychangescontinenteach
yearinordertomaximizethelikelihoodthatresearchersfromallovertheworld
willattend. Startingin1993,theproceedingsofTPHOLsanditspredecessor
workshopshavebeenpublishedinthefollowingvolumesoftheSpringer-Verlag
LectureNotesinComputerScienceseries: 1993(Canada) 780
1998(Australia)1479 1994(Malta) 859 1999(France) 1690 1995(USA) 971
2000(USA) 1869 1996(Finland)1125 2001(UK) 2152 1997(USA) 1275 VI
Preface The2002conferencewasorganizedbyateamfromNASALangleyResearch
Center,theICASEInstituteatLangleyResearchCenter,andConcordiaU-
versity. FinancialsupportcamefromIntelCorporation.
Thesupportofallthese organizationsisgratefullyacknowledged.
August2002 V'?ctorA. Carreno " C'esarA. Muno "z VII Organization
TPHOLs2002isorganizedbyNASALangleyandICASEincooperationwith
ConcordiaUniversity. Organizing Committee ConferenceChair:
V'?ctorA. Carren"o(NASALangley) ProgramChair: C'esarA. Muno
"z(ICASE,NASALaRC) So?'eneTahar(ConcordiaUniversity)
ProgramCommittee MarkAagaard(Waterloo)
MichaelKohlhase(CMU&Saarland) DavidBasin(Freiburg)
ThomasKropf(Bosch) V'?ctorCarren"o(NASALangley) TomMelham(Glasgow)
Shiu-KaiChin(Syracuse) JStrotherMoore(Texas,Austin)
PaulCurzon(Middlesex) C'esarMuno "z(ICASE,NASALaRC)
GillesDowek(INRIA) SamOwre(SRI) HaraldGanzinger(MPISaarbruc ken)
ChristinePaulin-Mohring(INRIA) GaneshGopalakrishnan(Utah)
LawrencePaulson(Cambridge) JimGrundy(Intel) FrankPfenning(CMU)
ElsaGunter(NJIT) KlausSchneider(Karlsruhe) JohnHarrison(Intel)
HennySipma(Stanford) DougHowe(Carleton) KonradSlind(Utah)
BartJacobs(Nijmegen) DonSyme(Microsoft) PaulJackson(Edinburgh) So?
'eneTahar(Concordia) SaraKalvala(Warwick) WaiWong(HongKongBaptist)
Additional Reviewers OtmaneAit-Mohamed AlfonsGeser HaraldRuess
BehzadAkbarpour HanneGottliebsen LeonvanderTorre NancyDay
MikeKishinevsky TomasUribe BenDiVito HansdeNivelle
Jean-ChristopheFilliatre AndrewPitts Invited Speakers
RickyButler(NASALangley) G'erardHuet(INRIA) VIII Preface Sponsoring
Institutions NASALangley ICASE ConcordiaUniversity INTEL Table of
Contents Invited Talks FormalMethodsatNASALangley...1 RickyButler
HigherOrderUni?cation30YearsLater...3 G' erardHuet Regular Papers
CombiningHigherOrderAbstractSyntaxwithTacticalTheoremProving
and(Co)Induction ...13 Simon J. Ambler,RoyL.
Crole,AlbertoMomigliano
E?cientReasoningaboutExecutableSpeci?cationsinCoq...31
GillesBarthe,PierreCourtieu Veri?edBytecodeModelCheckers...47
DavidBasin,StefanFriedrich,MarekGawkowski
The5ColourTheoreminIsabelle/Isar...67 GertrudBauer,TobiasNipkow
Type-TheoreticFunctionalSemantics...83
YvesBertot,VenanzioCapretta,KuntalDasBarman
AProposalforaFormalOCLSemanticsinIsabelle/HOL...99 AchimD.
Brucker,BurkhartWol?
ExplicitUniversesfortheCalculusofConstructions...115 Judica.
elCourant FormalisedCutAdmissibilityforDisplayLogic...1 31 JeremyE.
Dawson,RajeevGor'e
FormalizingtheTradingTheoremfortheClassi?cationofSurfaces...148
ChristopheDehlinger,Jean-Fran,coisDufourd
Free-StyleTheoremProving...164 DavidDelahaye
AComparisonofTwoProofCritics:Powervs. Robustness...182 LouiseA.
Dennis,AlanBundy X TableofContents
Two-LevelMeta-reasoninginCoq...198 AmyP. Felty
PuzzleTool:AnExampleofProgrammingComputationandDeduction . . 214
MichaelJ. C. Gordon AFormalApproachtoProbabilisticTermination...230
JoeHurd UsingTheoremProvingforNumericalAnalysis...246 MicaelaMayero
QuotientTypes:AModularApproach...263 AlekseyNogin
SequentSchemaforDerivedRules ...281 AlekseyNogin,JasonHickey
AlgebraicStructuresandDependentRecords ...298
VirgilePrevosto,DamienDoligez,Th' er' eseHardin
ProvingtheEquivalenceofMicrostepandMacrostepSemantics...314
KlausSchneider
WeakestPreconditionforGeneralRecursiveProgramsFormalizedinCoq .
|
Verification and Evaluation of Computer and Communication Systems - 11th International Conference, VECoS 2017, Montreal, QC, Canada, August 24-25, 2017, Proceedings (Paperback, 1st ed. 2017)
Kamel Barkaoui, Hanifa Boucheneb, Ali Mili, Sofiene Tahar
|
R1,557
Discovery Miles 15 570
|
Ships in 10 - 15 working days
|
This book constitutes the proceedings of the 11th International
Conference International Conference on Verification and Evaluation
of Computer and Communication Systems ( VECoS 2017 ), held at
Concordia University, Montreal, Canada, in August 2017. The 13 full
papers, together with 3 abstracts in this volume were carefully
reviewed and selected from 35 submissions. The aim of the VECoS
conference is to bring together researchers and practitioners in
the areas of verification, control, performance and dependability
evalu-ation in order to discuss state-of-the-art and challenges in
modern computer and communication systems in which functional and
extra-functional properties are strongly interrelated. Thus, the
main motivation for VECoS is to encourage the cross-fertilization
between various formal verification and evaluation approaches,
methods and techniques, and especially those developed for
concurrent and dis-tributed hardware/software systems.
Scientists and engineers often have to deal with systems that
exhibit random or unpredictable elements and must effectively
evaluate probabilities in each situation. Computer simulations,
while the traditional tool used to solve such problems, are limited
in the scale and complexity of the problems they can solve.
Formalized Probability Theory and Applications Using Theorem
Proving discusses some of the limitations inherent in computer
systems when applied to problems of probabilistic analysis, and
presents a novel solution to these limitations, combining
higher-order logic with computer-based theorem proving. Combining
practical application with theoretical discussion, this book is an
important reference tool for mathematicians, scientists, engineers,
and researchers in all STEM fields.
Traditionally, computer simulation techniques are used to perform
probabilistic analysis. However, they provide less accurate results
and cannot handle large-scale problems due to their enormous CPU
time requirements. Recently, a significant amount of formalization
has been done in higher-order logic that allows us to conduct
precise probabilistic analysis using theorem proving and thus
overcome the limitations of the simulation based probabilistic
analysis approach. Some major contributions include the
formalization of both discrete and continuous random variables and
the verification of corresponding probabilistic and statistical
properties. This book presents a concise description of the
infrastructures behind these capabilities and their utilization to
conduct the probabilistic analysis of real-world systems. The case
studies of the round-off error of a digital processor, the Coupon
Collector's problem and the Stop-and-Wait protocol are used to
illustrate the proposed analysis approach. Designed as an
independent research tool, the book presents a well-thought-out
treatment of a rapidly emerging multidisciplinary field across
Mathematics, Computer Science and Engineering.
|
You may like...
Loot
Nadine Gordimer
Paperback
(2)
R398
R330
Discovery Miles 3 300
Loot
Nadine Gordimer
Paperback
(2)
R398
R330
Discovery Miles 3 300
|