Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第六届国际游戏、自动机、逻辑和形式化验证研讨会(GandALF 2015)的会议记录。研讨会于2015年9月21日和22日在意大利热那亚举行。专题讨论会的会议记录载有三次应邀演讲的摘要和13篇论文,这些论文是经过仔细评估后被接受在会议上介绍的。被接受的论文的主题包括算法博弈论,自动机理论,形式化验证,模态和时序逻辑。
2015-09-23 cs.FL cs.LO
Pre-proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018)
本卷构成了第28届基于逻辑的程序合成和转换国际研讨会的预录(LOPSTR 2018),于2018年9月4日至6日在美因河畔法兰克福举行,德国,并与第20届声明式编程原则和实践国际研讨会同地举行(PPDP 2018)和第26届函数和逻辑编程国际研讨会(WFLP 2018)。
2018-09-11 cs.LO
Proceedings Tenth Symposium on Working Formal Methods
本文介绍了第十届工作形式方法研讨会(FROM 2026)的举办信息,包括时间地点、组织方、同期会议及收录的14篇论文。
2026-09-28 cs.LO cs.SC cs.SE
Proceedings of Second International Symposium on Games, Automata, Logics and Formal Verification
本卷包含了第二届游戏、自动机、语言和形式化验证国际研讨会(GandALF 2011)的论文集。会议于2011年6月15日至17日在意大利阿马尔菲海岸的米诺里举行。Gandalf研讨会的目的是为来自不同领域和不同背景的研究人员提供一个论坛,这些研究人员在博弈论,数理逻辑,自动机理论及其在复杂系统的规范,设计和验证中的应用方面有着共同的兴趣。本论文集包含三个特邀演讲和十九篇定期论文的摘要,这些论文是根据原创性、质量和与研讨会主题的相关性通过严格的审查过程选出的。
2011-06-04 cs.LO
Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第七届国际游戏、自动机、逻辑和形式化验证研讨会(GandALF 2016)的会议记录。研讨会于2016年9月14日至16日在意大利卡塔尼亚举行。研讨会的会议记录包括3个特邀演讲的摘要和21篇论文全文,这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题涵盖算法博弈论,自动机理论,综合,形式化验证,动态,模态和时态逻辑。
2016-09-13 cs.FL cs.GT cs.LO
Proceedings Eighth Symposium on Working Formal Methods
本文介绍了实用形式化方法研讨会(FROM)系列会议,其旨在汇聚形式化方法领域的研究者与从业者,推动理论成果创新及相关软件工具的开发与应用。
2024-10-30 cs.LO
Proceedings Fifth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第五届国际游戏、自动机、逻辑和形式化验证研讨会(GandALF 2014)的会议记录。研讨会于2014年9月10日至12日在意大利维罗纳举行。专题讨论会的会议记录载有三次应邀演讲的摘要和19篇论文,这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广,包括算法和行为博弈论,博弈语义学,形式语言和自动机理论,模态和时序逻辑,软件验证,混合系统。
2014-08-24 cs.FL cs.GT cs.LO
Proceedings Third Symposium on Working Formal Methods
本卷包含了2019年9月3日至5日在罗马尼亚蒂米什瓦拉举行的第三届正式工作方法研讨会的会议记录。从旨在汇集研究人员和从业者谁工作的正式方法,通过贡献新的理论成果,方法,技术和框架,和/或使正式方法的工作,通过创建或使用软件工具,应用理论的贡献。
2019-09-02 cs.LO cs.SC
Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第四届国际游戏、自动机、逻辑和形式化验证研讨会(GandALF 2013)的会议记录。研讨会于2013年8月29日至31日在意大利Borca di Cadore举行。专题讨论会的会议记录载有三次应邀演讲的摘要和17篇论文,这些论文是经过仔细评估后被接受在会议上发表的。被接受的论文的主题范围很广,包括算法和行为博弈论,博弈语义学,形式语言和自动机理论,模态和时序逻辑,软件验证,混合系统。
2013-07-16 cs.FL cs.GT cs.LO
Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第12届国际游戏,自动机,逻辑和形式化验证研讨会(GandALF 2021)的会议记录。Gandalf 2021研讨会的目的是汇集来自学术界和工业界的研究人员,他们积极参与游戏,自动机,逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题,并促进相互交流。
2021-09-16 cs.FL cs.GT cs.LO
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第13届国际游戏,自动机,逻辑和形式化验证研讨会(GandALF 2022)的会议记录。Gandalf 2022研讨会的目的是汇集来自学术界和工业界的研究人员,他们积极参与游戏,自动机,逻辑和形式化验证领域的工作。其想法是涵盖从理论到应用的广泛主题,并促进相互交流。
2022-09-19 cs.FL cs.GT cs.LO
Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第九届游戏,自动机,逻辑和形式化验证国际研讨会(GandALF 2018)的会议记录。研讨会于2018年9月26日至28日在德国萨尔布吕肯举行。Gandalf研讨会是由一群意大利计算机科学家建立的,他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛,让来自不同地区,可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神,这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2018-09-07 cs.FL cs.LO
Proceedings of the Fourteenth International Symposium on Games, Automata, Logics, and Formal Verification
该论文集汇集GandALF 2023关于博弈、自动机、逻辑与形式验证的研究,旨在连接学界与业界并推动理论及应用的交叉融合。
2023-09-29 cs.CC cs.FL cs.LO
Proceedings Seventeenth International Symposium on Games, Automata, Logics, and Formal Verification
本文是关于GandALF 2026研讨会论文集的介绍,该会议于2026年在丹麦奥尔堡举行,旨在汇集博弈、自动机、逻辑与形式化验证领域的研究者,促进理论与应用的交叉融合。
2026-10-08 cs.FL cs.LO
Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第11届游戏,自动机,逻辑和形式化验证国际研讨会(GandALF 2020)的会议记录。研讨会于2020年9月21日至22日以完全在线的方式举行。Gandalf研讨会是由一群意大利计算机科学家建立的,他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛,让来自不同地区,可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神,这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2020-09-20 cs.FL cs.GT cs.LO
Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷包含第十届游戏,自动机,逻辑和形式化验证国际研讨会(GandALF 2019)的会议记录。研讨会于2010年9月2日至3日在法国波尔多举行。Gandalf研讨会是由一群意大利计算机科学家建立的,他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛,让来自不同地区,可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神,这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2019-09-12 cs.FL cs.GT cs.LO
Proceedings Third International Symposium on Games, Automata, Logics and Formal Verification
本卷包含了2012年9月6日至8日在那不勒斯(意大利)举行的第三届游戏、自动机、逻辑和形式化验证国际研讨会(GandALF)的会议记录。Gandalf是由一些意大利计算机科学家创立的,他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛,让来自不同地区,可能有不同背景的人可以进行富有成效的互动。尽管专题讨论会的想法是在意大利研究界提出的,但正如会议委员会的组成和方案所证明的那样,这次活动具有真正的国际性质。
2012-10-07 cs.GT cs.LO
Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification
本卷包含第八届游戏、自动机、逻辑和形式化验证国际研讨会(GandALF 2017)的会议记录。研讨会于2017年9月20日至22日在意大利罗马举行。Gandalf研讨会是由一群意大利计算机科学家建立的,他们对数学逻辑、自动机理论、博弈论及其在复杂系统规范、设计和验证中的应用感兴趣。它的目的是提供一个论坛,让来自不同地区,可能有不同背景的人可以进行富有成效的互动。Gandalf具有真正的国际精神,这一点可以从项目和指导委员会的组成以及提交论文的国家分布中得到证明。
2017-09-06 cs.FL cs.GT cs.LO
Proceedings 21st International Symposium on Logical and Semantic Frameworks with Applications
第21届逻辑与语义框架及其应用研讨会会议录发布,旨在推广从传统到前沿的相关技术成果,从实践角度提供整合、实现和使用这些方法及成果的反馈。
2026-07-20 cs.LO
Proceedings of the Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷为 GandALF 2025(第十六届国际游戏、自动机、逻辑与形式化验证研讨会)论文集,旨在汇聚相关领域产学研人员,推动从理论到应用的广泛主题交流与交叉融合。
2025-09-16 cs.LO
Proceedings Fifteenth International Symposium on Games, Automata, Logics, and Formal Verification
本卷是2024年6月在冰岛雷克雅未克举办的第十五届GandALF研讨会论文集,该会汇聚游戏、自动机等领域产学研研究者,覆盖理论到应用主题以促进跨领域融合。
2024-10-29 cs.CC cs.FL cs.LO
Proceedings First Symposium on Games, Automata, Logic, and Formal Verification
本卷包含了第一次研讨会上的“游戏,自动机,逻辑,和形式化验证(GandALF)",在米诺里(阿马尔菲海岸),意大利,2010年6月17日至18日举行的会议记录。研讨会由一些对博弈论、数理逻辑、自动机理论及其在复杂系统的规范、设计和验证中的应用感兴趣的意大利计算机科学家推动。它涵盖了大量的研究课题,从理论方面到具体应用。它的目的是提供一个论坛,让来自不同地区的人,可能有不同的背景,可以成功地互动。该活动的高水平国际形象由节目委员会的组成和最终节目见证。
2010-06-09 cs.FL cs.GT cs.LO
Proceedings Twentieth International Symposium on Logical and Semantic Frameworks with Applications
本文介绍在巴西利亚举行的LSFA 2025会议论文集,说明其旨在连接逻辑与语义框架领域的理论研究与实践反馈。
2025-09-28 cs.LO
Proceedings Sixth Workshop on Intersection Types and Related Systems
本卷包含第六届交叉口类型和相关系统研讨会(ITRS 2012)的会议记录。该研讨会于2012年6月29日在杜布罗夫尼克(克罗地亚)举行,隶属于第二十七届年度ACM/IEEE计算机科学逻辑研讨会(LICS 2012)。ITRS研讨会旨在汇集研究人员,研究基于交叉口类型和相关方法的系统的理论和实际应用(例如,联合类型、细化类型、行为类型、递归类型等等)。
2013-07-30 cs.LO cs.PL
Proceedings Fourth International Symposium on Symbolic Computation in Software Science
符号计算是用符号对象(术语、公式、程序、代数对象、几何对象等)进行计算的科学。在过去的几十年中,强大的符号算法已经发展起来,并在定理证明,自动推理,软件验证,模型检验,重写,数学形式化,网络安全,Groebner基地,特征集等国际研讨会上发挥了重要作用“符号计算在软件科学”是SCSS研讨会系列的第四个。SCSS 2008和2010在奥地利哈根贝格的符号计算研究所(RISC)举行,SCSS 2009在突尼斯的Gammarth举行。这些研讨会是由内部研讨会发展而来的,这些研讨会汇集了来自以下领域的研究人员:a)评分(符号计算研究小组),日本筑波大学,b)奥地利林茨约翰内斯开普勒大学符号计算研究所的定理小组,c)SSFG(软件科学基金会小组),以及d)突尼斯迦太基大学的Sup'Com(突尼斯通信高等学院)。
2013-07-30 cs.LO cs.SC
Proceedings Sixth Workshop on Structural Operational Semantics
本卷包含SOS 2009的会议记录,第六届结构操作语义研讨会于2009年8月31日在意大利博洛尼亚举行,作为CONCUR 2009的附属研讨会,第20届国际并发理论会议。结构操作语义(SOS)是一种为编程和规约语言定义操作语义的技术。该研讨会是研究人员,学生和从业人员感兴趣的新发展和未来的调查方向在SOS领域的论坛。研讨会的具体目标之一是为并发和程序设计语言社区提供一个聚会点。另一个目标是在全世界的研究生和年轻研究人员中传播SOS的理论和实践。
2010-02-15 cs.LO cs.PL
Proceedings of the 9th International Symposium on Symbolic Computation in Software Science
本卷包含在第九届软件科学符号计算国际研讨会(SCSS 2021)上发表的论文。符号计算是一门用符号对象(术语、公式、程序、代数对象的表示等)进行计算的科学。在过去的几十年里,在符号计算的主要子领域:计算机代数和计算逻辑中,已经开发出了强大的算法。这些算法和方法被成功地应用于各个领域,包括软件科学,它涵盖了广泛的主题,软件建设和分析。同时,人工智能方法和机器学习算法如今被广泛用于各个领域,特别是与符号计算相结合。有几种方法混合了人工智能和符号方法以及部署在大型语料库上的工具,以创建所谓的认知系统。认知计算专注于构建通过推理与人类自然交互的系统,旨在大规模学习。SCSS的目的是结合现代人工智能技术,促进软件科学中符号计算的理论和实践方面的研究。这些会议记录包括Bruno Buchberger的主旨文件和10份供稿。此外,会议计划包括三个特邀演讲,九个简短的和正在进行的论文,以及一个关于计算机代数和计算逻辑的特别会议。由于COVID-19大流行,研讨会完全在线举行。它由林茨约翰尼斯开普勒大学的符号计算研究所(RISC)于2021年9月8日至10日组织。
2021-09-06 cs.AI cs.LO cs.SC
Proceedings Sixth Workshop on Models for Formal Analysis of Real Systems
MARS 2024研讨会论文集聚焦真实系统形式化建模,旨在解决大规模案例研究匮乏与模型细节易被省略的问题,强调建模重于验证以分享建模经验。
2024-03-26 cs.LO cs.PL cs.SE
Proceedings of the Sixth International Conference on Applied Category Theory 2023
本论文集为2023年第六届应用范畴论国际会议(ACT2023)的出版物,介绍了会议的举办信息、往届沿革、活动环节、投稿赛道及本卷收录规则,投稿覆盖多学科的纯理论与应用研究。
2023-12-13 cs.LO cs.PL
Proceedings 11th International Workshop on Automated Specification and Verification of Web Systems
这些会议记录包含在2015年6月23日在挪威奥斯陆举行的第11届Web系统自动化规范和验证国际研讨会(WWV 2015)上提交的论文,作为第20届形式化方法国际研讨会(FM 2015)的卫星研讨会。WWV是一个年度跨学科论坛,研究人员来自以下领域:声明式,基于规则的编程,形式化方法,软件工程和基于Web的系统。该研讨会促进这些领域的混合方法的交叉和进步。
2015-08-14 cs.LO cs.PL cs.SE
Proceedings of the Sixth Workshop on Horn Clauses for Verification and Synthesis and Third Workshop on Program Equivalence and Relational Reasoning
本卷包含第三届程序等价和关系推理研讨会(PERR)和第六届验证与综合霍恩子句研讨会(HCVS)的联合后续会议记录,分别于4月6日和7日在捷克共和国布拉格举行,作为ETAPS的附属研讨会。
2019-07-08 cs.LO
Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice
本卷是LFMTP 2011的会议记录,第六届逻辑框架和元语言国际研讨会:理论与实践。LFMTP研讨会系列汇集了设计者,实现者和从业者,讨论逻辑框架和元语言结构的各个方面,这些方面影响了它们在逻辑和计算机科学中感兴趣的各种演绎系统的表示,实现和推理。LFMTP 2011于2011年8月26日在荷兰奈梅亨举行,作为ITP 2011的相关研讨会,第二届交互式定理证明国际会议。它的方案包括贡献和邀请的演讲,并与MLPA 11,第三次证明助手模块和库研讨会相结合。本会议录仅包含被接受在研讨会上发表的论文。这些论文中的每一篇都是根据项目委员会三名成员的审查而被接受的。随后,作者有机会根据审评员提出的评论意见和他们在研讨会上发言时获得的反馈意见修改其提交的材料。
2011-10-31 cs.LO cs.PL
Proceedings Sixth Workshop on Synthesis
SYNT研讨会旨在汇集对计算系统综合这一广泛领域感兴趣的研究人员。目标是促进计算系统自动化开发的前沿技术的发展。感兴趣的贡献包括算法,复杂性和可判定性分析,以及可重复的算法,实现的工具和实验评估。应用领域包括软件、硬件、嵌入式和网络物理系统。计算模型包括函数式、反应式、混合式和时间系统。识别,正规化,并在特定的应用领域的综合评估是鼓励。第六次研讨会在德国海德堡举行。它与第29届计算机辅助核查国际会议设在同一地点。研讨会包括四个贡献的演讲,四个邀请演讲,以及关于句法指导合成竞赛(SyGuS)和反应合成竞赛(SYNTCOMP)的报告。
2017-11-28 cs.FL cs.LO cs.SE
Proceedings Sixth International Workshop on Formal Methods for Autonomous Systems
本卷收录第六届自主系统形式化方法国际研讨会(FMAS 2024)的论文,该会于2024年11月11日至13日与iFM'24在曼彻斯特大学联合举办。
2024-11-20 cs.AI cs.LO cs.RO
Proceedings Sixth Workshop on Proof eXchange for Theorem Proving
本卷EPTCS包含了2019年8月26日在巴西纳塔尔举行的第六届定理证明证据交换研讨会(PxTP 2019)的会议记录,作为CADE-27会议的一部分。PxTP研讨会系列汇集了研究人员,他们致力于推理系统和形式主义之间的通信,集成和合作的各个方面,特别关注证明。在过去几十年中,计算机辅助推理(包括自动化和交互式推理)取得了进展,使人们有可能建立越来越适用于更广泛问题的推理工具,并能够逐步更快地解决更大的问题。近年来,在较大的系统中,这些工具之间的合作已经证明了减少人工干预的潜力。推理系统之间的合作依赖于理论形式主义和实用工具的可用性,以交换问题,证明和模型。PxTP系列研讨会致力于鼓励这种合作,邀请各方就推理工具之间合作的各个方面做出贡献,无论是自动的还是交互式的。
2019-08-23 cs.LO
Proceedings of the 6th Workshop on Formal Integrated Development Environment
本卷包含F-IDE 2021的会议记录,这是第六届正式集成开发环境国际研讨会,于2021年5月24日至25日在线举行,作为NFM'21的一部分,第13届NASA正式方法研讨会。高级别的安全、保密和隐私标准要求使用正式的方法来指定和开发兼容的软件(子)系统。任何标准都有一个评估过程,这需要一个完整的应用程序文档,以便简化设计选择的合理性以及代码和证明的审查。因此,需要工具来处理规范、程序构造和验证工件。F-IDE研讨会的目的是提供一个论坛,介绍和讨论研究工作以及设计,开发和使用正式IDE的经验回报,旨在使正式方法更容易为专家和非专家。
2021-08-05 cs.LO cs.PL cs.SE
Proceedings 6th Workshop on Mathematically Structured Functional Programming
第六次数学结构化函数式编程研讨会致力于从结构中推导功能。这是庆祝理论计算机科学对我们今天编写程序的直接影响。现代程序设计语言,特别是函数式语言,支持数学结构的直接表达,为程序员提供了强大而抽象的工具。如果没有monads,Haskell会在哪里?没有箭头的函数式反应编程?按推值调用而不进行预处理?这个研讨会是一个为那些寻求在数据和控制中反映数学现象的研究人员提供的论坛。第六届数学结构函数编程研讨会于2016年4月8日在荷兰埃因霍温举行,作为ETAPS 2016的一部分。有五个贡献的谈话和一个邀请谈话。
2016-04-01 cs.LO cs.PL
Proceedings First Workshop on Quantitative Formal Methods: Theory and Applications
本卷包含了在第一次研讨会上提出的论文定量形式化方法:理论和应用,这是在埃因霍温举行的2009年11月3日作为国际研讨会的一部分形式化方法2009年。这一卷载有所有已接受在讲习班上提出的材料的最后文本。
2009-12-10 cs.LO cs.PF
Proceedings Sixth Workshop on Developments in Computational Models: Causality, Computation, and Physics
DCM 2010提供了一个关于新计算方法和模型的论坛,2010年特别强调与物理学和生物学相关的计算和因果模型。我们相信,在一个具有FLoC强大基础背景的社区中,将不同的方法结合在一起,会产生鼓舞人心的跨境交流和创新的进一步研究。第二天的这个前FLoC 2010研讨会是给了物理和量子相关的计算。第一天的内容更典型的是以前的DCM研讨会-涵盖了与开发新的计算模型或传统计算模型的新功能相关的全方位主题。DCM 2010旨在促进互动,并为提出新想法和正在进行的工作提供一个论坛。它还旨在使新来者能够了解这一领域的最新研究。
2010-07-23 cs.LO quant-ph
Proceedings Sixth International Workshop on Classical Logic and Computation
研讨会系列旨在涵盖研究经典逻辑和数学的计算方面的研究。它的重点是解开逻辑原理的计算内容和基于这些原理的数学证明,旨在将两个领域的研究人员聚集在一起并交流思想。经典逻辑与计算(CL&C)2016是该系列研讨会的第六届,作为FSCD 2016的卫星于2016年6月23日在葡萄牙波尔图举行。在第六版中,我们收到了11份简短和完整的论文。其中八(8)被选中在波尔图会议上提出,五(5)全文最初被接受出现在EPTCS特别卷,其中一个后来被其作者撤回。一个邀请演讲是由马克Bezem(美国)。《逻辑学》(Coherent Logic):一种逻辑。今年提交的其他主题包括:使用非标准分析的证明的计算内容,证明的Herbrand内容的结构化语法为基础的方法,语义的Muda-mu演算,经典自然演绎证明的规范化,凸优化和代数中的无效证明的证明挖掘功能解释。我想感谢项目委员会的成员,感谢他们出色的工作:斯蒂芬·范·巴克尔(伦敦)、斯特凡诺·贝拉尔迪(都灵)、费尔南多·费雷拉(里斯本)、雨果·德·利古罗(都灵)、亚历山大·米克尔(蒙得维的亚)。Ulrich Kohlenbach(达姆施塔特,PC主席)
2016-06-19 cs.LO
Proceedings 2nd Workshop on Formal Methods in the Development of Software
本卷包含第二届软件开发中的形式化方法研讨会(WS-FMDS 2012)的会议记录。该研讨会于2012年8月30日在法国巴黎举行,作为第18届形式方法国际研讨会(FM-2012)的卫星活动。WS-FMDS 2012的目的是为那些对使用软件方法论开发的系统上的形式化方法的应用感兴趣的研究人员提供一个论坛。特别是,该讲习班旨在汇集活跃在正式方法领域并有兴趣交流这些方法的工业应用经验的科学家和从业人员。该研讨会还致力于促进研究和开发,以改进工业应用的正式方法和工具。
2012-07-08 cs.LO cs.SE
Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications
本卷包含第二届法国新加坡正式方法和应用研讨会(FSFMA'14)的会议记录。该研讨会于2014年5月13日在新加坡举行,作为第19届形式方法国际研讨会(FM'14)的卫星活动。FSFMA旨在分享研究兴趣,并在正式方法及其应用领域开展合作。研讨会的科学主题涵盖(但不限于)形式规范、模型检验、验证、程序分析/转换、软件工程以及计算机科学主要领域(包括航空航天)的应用等领域。该研讨会汇集了来自法国,新加坡和其他国家的研究人员和行业研发专家,交流他们的知识,讨论他们的研究成果,并探索潜在的合作。本卷包含八个贡献:四个邀请会谈和四个定期文件。
2014-07-08 cs.LO cs.SE
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation
本卷包含MARS 2018的联合会议记录,第三次真实系统形式分析模型研讨会,以及VPT 2018,第六次验证和程序转换国际研讨会,于2018年4月20日在希腊塞萨洛尼基举行,作为ETAPS 2018的一部分,欧洲软件理论与实践联合会议。MARS强调建模而非验证。它的目的是讨论从制定正式的方法来验证和分析现实的系统中吸取的教训。例如:(1)选择哪种形式主义,为什么?(2)必须进行哪些抽象,为什么?(3)系统的重要特征是如何建模的?(4)在对系统建模时是否有任何并发症?(5)采取了哪些措施来保证模型的准确性?我们邀请了论文,提出了真实系统的完整模型,这可能会为未来的比较和分析奠定基础。研讨会的目的之一是介绍不同的建模方法,并讨论每种方法的利弊。在这次研讨会上提出的系统的替代正式描述是鼓励,这应该促进改进规范形式主义的发展。VPT旨在提供一个论坛,来自程序转换和程序验证领域的人们可以卓有成效地交换意见,并对这两个领域之间的相互作用有更深入的了解。这些互动在两个方面都是有益的。一方面,在程序转换领域开发的方法和工具,如部分演绎,部分求值,折叠/展开变换和超级编译,成功地应用于验证,特别是无限状态和参数化系统的验证。另一方面,在程序验证中开发的方法,如模型检验,抽象解释,SAT和SMT求解,自动定理证明,用于增强程序转换技术,从而使这些技术在实践中更强大和有用的。
2018-03-23 cs.FL cs.LO cs.PL
Proceedings Quantities in Formal Methods
本卷包含2012年8月28日在法国巴黎举行的QFM 2012正式方法研讨会的会议记录。该研讨会隶属于第18届形式方法研讨会,FM 2012。研讨会的重点是建模、验证和综合中的数量。形式化方法的现代应用需要对时间、资源或概率等量进行形式化推理。标准的形式化方法和工具已经非常擅长建模(和验证)定性属性:某些事件是否会发生。在过去的几年中,这些方法和工具已经扩展到也覆盖定量方面,特别是导致工具,例如UPPAAL(用于实时系统),PRISM(用于概率系统)和PHAVer(用于混合系统)。然而,在这些工具可以用于它们所针对的工业应用之前,还有很多工作要做。
2012-12-14 cs.FL cs.LG cs.LO
Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications
本卷包含第六届逻辑和语义框架与应用研讨会(LSFA 2011)的会议记录。研讨会将于2011年8月27日在贝洛奥里藏特举行。逻辑和语义框架是用于表示逻辑、语言和系统的形式语言。这些框架为系统和程序设计语言的正式规范提供了基础,支持工具开发和推理。这个为期一天的研讨会的目的是将理论家和实践者聚集在一起,从理论方面推广新技术和成果,并从实践方面对这些技术和成果的实施和使用进行反馈。
2012-03-24 cs.CC cs.LO cs.PL
Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
本卷包含LFMTP 2019年6月22日在加拿大温哥华举行的第14届逻辑框架和元语言国际研讨会:理论与实践(LFMTP)上发表的论文选集。该研讨会隶属于第34届年度ACM/IEEE计算机科学逻辑研讨会(LICS)。逻辑框架和元语言形成了一个共同的基础,用于表示、实现和推理逻辑和计算机科学中感兴趣的各种演绎系统。它们的设计,实现和它们在推理任务中的使用,从软件的正确性到形式系统的属性,一直是过去二十年来大量研究的焦点。该研讨会将汇集设计师,实施者和从业人员,讨论影响逻辑框架结构和实用性的各个方面,包括变量绑定,归纳和共归纳推理技术的处理以及推理过程的表达性和清晰度。
2019-10-19 cs.LO
Proceedings Third International Workshop on Linearity
本卷包含2014年7月13日在奥地利维也纳举行的第三届线性国际研讨会LINEARITY 2014上发表的论文。该研讨会是为期一天的FLoC 2014卫星活动,第六届联邦逻辑会议。它是2014年维也纳逻辑之夏的一部分。该研讨会的目的是汇集正在探索线性微积分理论和应用的研究人员,促进他们的互动,并为提出新想法和正在进行的工作提供一个论坛,并使新来者能够了解该领域的当前活动。令人感兴趣的是新的结果,使线性的中心使用,从基础工作到任何领域的应用。这包括:次线性逻辑、线性项演算、线性类型系统、线性证明理论、线性程序设计语言、并发应用、基于交互的系统、线性系统的验证、计算的量子模型以及计算的生物和化学模型。
2015-02-16 cs.LO